mathlib documentation

logic.function.conjugate

Semiconjugate and commuting maps

We define the following predicates:

def function.semiconj {α : Type u_1} {β : Type u_2} :
(α → β)(α → α)(β → β) → Prop

We say that f : α → β semiconjugates ga : α → α to gb : β → β if f ∘ ga = gb ∘ f.

Equations
theorem function.semiconj.comp_eq {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} :
function.semiconj f ga gbf 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 gbfunction.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 gbfunction.semiconj fbc gb gcfunction.semiconj (fbc fab) ga gc

theorem function.semiconj.id_right {α : Type u_1} {β : Type u_2} {f : α → β} :

theorem function.semiconj.id_left {α : Type u_1} {ga : α → α} :

theorem function.semiconj.inverses_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga ga' : α → α} {gb gb' : β → β} :

def function.commute {α : Type u_1} :
(α → α)(α → α) → Prop

Two maps f g : α → α commute if f ∘ g = g ∘ f.

Equations
theorem function.semiconj.commute {α : Type u_1} {f g : α → α} :

theorem function.commute.refl {α : Type u_1} (f : α → α) :

theorem function.commute.symm {α : Type u_1} {f g : α → α} :

theorem function.commute.comp_right {α : Type u_1} {f g g' : α → α} :

theorem function.commute.comp_left {α : Type u_1} {f f' g : α → α} :

theorem function.commute.id_right {α : Type u_1} {f : α → α} :

theorem function.commute.id_left {α : Type u_1} {f : α → α} :

def function.semiconj₂ {α : Type u_1} {β : Type u_2} :
(α → β)(α → α → α)(β → β → β) → 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
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 : β → β → β} :

theorem function.semiconj₂.id_left {α : Type u_1} (op : α → α → α) :

theorem function.semiconj₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {ga : α → α → α} {gb : β → β → β} {f' : β → γ} {gc : γ → γ → γ} :

theorem function.semiconj₂.is_associative_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [is_associative α ga] :

theorem function.semiconj₂.is_associative_left {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [is_associative β gb] :

theorem function.semiconj₂.is_idempotent_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [is_idempotent α ga] :

theorem function.semiconj₂.is_idempotent_left {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [is_idempotent β gb] :