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 equivalentlysemiconj f g g.
We say that f : α → β semiconjugates ga : α → α to gb : β → β if f ∘ ga = gb ∘ f.
Equations
- function.semiconj f ga gb = ∀ (x : α), f (ga x) = gb (f x)
theorem
function.semiconj.comp_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α}
{gb : β → β} :
function.semiconj f ga gb → f ∘ ga = gb ∘ f
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' : β → β} :
function.semiconj f ga gb → 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 : γ → γ} :
function.semiconj fab ga gb → 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' : β → β} :
function.semiconj f ga gb → function.right_inverse ga' ga → function.left_inverse gb' gb → function.semiconj f ga' gb'
Two maps f g : α → α commute if f ∘ g = g ∘ f.
Equations
- function.commute f g = function.semiconj f g g
theorem
function.semiconj.commute
{α : Type u_1}
{f g : α → α} :
function.semiconj f g g → function.commute f g
theorem
function.commute.symm
{α : Type u_1}
{f g : α → α} :
function.commute f g → function.commute g f
theorem
function.commute.comp_right
{α : Type u_1}
{f g g' : α → α} :
function.commute f g → function.commute f g' → function.commute f (g ∘ g')
theorem
function.commute.comp_left
{α : Type u_1}
{f f' g : α → α} :
function.commute f g → function.commute f' g → function.commute (f ∘ f') g
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)
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)
theorem
function.semiconj₂.comp_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ga : α → α → α}
{gb : β → β → β} :
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 : γ → γ → γ} :
function.semiconj₂ f' gb gc → function.semiconj₂ f ga gb → function.semiconj₂ (f' ∘ f) ga gc