Semiconjugate and commuting maps #
We define the following predicates:
function.semiconj:f : α → βsemiconjugatesga : α → αtogb : β → βiff ∘ ga = gb ∘ f;function.semiconj₂:f : α → βsemiconjugates a binary operationga : α → α → αtogb : β → β → βiff (ga x y) = gb (f x) (f y)`;f : α → αcommutes withg : α → αiff ∘ g = g ∘ f, or equivalently `semiconj f g g`.
We say that f : α → β semiconjugates ga : α → α to gb : β → β if f ∘ ga = gb ∘ f.
We use ∀ x, f (ga x) = gb (f x) as the definition, so given h : function.semiconj f ga gb and
a : α, we have h a : f (ga a) = gb (f a) and h.comp_eq : f ∘ ga = gb ∘ f.
Equations
- function.semiconj f ga gb = ∀ (x : α), f (ga x) = gb (f x)
@[protected]
theorem
function.semiconj.comp_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α}
{gb : β → β}
(h : function.semiconj f ga gb) :
@[protected]
theorem
function.semiconj.eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α}
{gb : β → β}
(h : function.semiconj f ga gb)
(x : α) :
f (ga x) = gb (f x)
theorem
function.semiconj.comp_right
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga ga' : α → α}
{gb gb' : β → β}
(h : function.semiconj f ga gb)
(h' : function.semiconj f ga' gb') :
function.semiconj f (ga ∘ ga') (gb ∘ gb')
theorem
function.semiconj.comp_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{fab : α → β}
{fbc : β → γ}
{ga : α → α}
{gb : β → β}
{gc : γ → γ}
(hab : function.semiconj fab ga gb)
(hbc : function.semiconj fbc gb gc) :
function.semiconj (fbc ∘ fab) ga gc
theorem
function.semiconj.inverses_right
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga ga' : α → α}
{gb gb' : β → β}
(h : function.semiconj f ga gb)
(ha : function.right_inverse ga' ga)
(hb : function.left_inverse gb' gb) :
function.semiconj f ga' gb'
Two maps f g : α → α commute if f (g x) = g (f x) for all x : α.
Given h : function.commute f g and a : α, we have h a : f (g a) = g (f a) and
h.comp_eq : f ∘ g = g ∘ f.
Equations
- function.commute f g = function.semiconj f g g
theorem
function.semiconj.commute
{α : Type u_1}
{f g : α → α}
(h : function.semiconj f g g) :
function.commute f g
theorem
function.commute.symm
{α : Type u_1}
{f g : α → α}
(h : function.commute f g) :
function.commute g f
theorem
function.commute.comp_right
{α : Type u_1}
{f g g' : α → α}
(h : function.commute f g)
(h' : function.commute f g') :
function.commute f (g ∘ g')
theorem
function.commute.comp_left
{α : Type u_1}
{f f' g : α → α}
(h : function.commute f g)
(h' : function.commute f' g) :
function.commute (f ∘ f') g
def
function.semiconj₂
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(ga : α → α → α)
(gb : β → β → β) :
Prop
A map f semiconjugates a binary operation ga to a binary operation gb if
for all x, y we have f (ga x y) = gb (f x) (f y). E.g., a monoid_hom
semiconjugates (*) to (*).
Equations
- function.semiconj₂ f ga gb = ∀ (x y : α), f (ga x y) = gb (f x) (f y)
@[protected]
theorem
function.semiconj₂.eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α → α}
{gb : β → β → β}
(h : function.semiconj₂ f ga gb)
(x y : α) :
f (ga x y) = gb (f x) (f y)
@[protected]
theorem
function.semiconj₂.comp_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α → α}
{gb : β → β → β}
(h : function.semiconj₂ f ga gb) :
function.bicompr f ga = function.bicompl gb f f
theorem
function.semiconj₂.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{ga : α → α → α}
{gb : β → β → β}
{f' : β → γ}
{gc : γ → γ → γ}
(hf' : function.semiconj₂ f' gb gc)
(hf : function.semiconj₂ f ga gb) :
function.semiconj₂ (f' ∘ f) ga gc
theorem
function.semiconj₂.is_associative_right
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α → α}
{gb : β → β → β}
[is_associative α ga]
(h : function.semiconj₂ f ga gb)
(h_surj : function.surjective f) :
is_associative β gb
theorem
function.semiconj₂.is_associative_left
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α → α}
{gb : β → β → β}
[is_associative β gb]
(h : function.semiconj₂ f ga gb)
(h_inj : function.injective f) :
is_associative α ga
theorem
function.semiconj₂.is_idempotent_right
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α → α}
{gb : β → β → β}
[is_idempotent α ga]
(h : function.semiconj₂ f ga gb)
(h_surj : function.surjective f) :
is_idempotent β gb
theorem
function.semiconj₂.is_idempotent_left
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α → α}
{gb : β → β → β}
[is_idempotent β gb]
(h : function.semiconj₂ f ga gb)
(h_inj : function.injective f) :
is_idempotent α ga