mathlib3 documentation

logic.function.conjugate

Semiconjugate and commuting maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the following predicates:

function.semiconj: f : α → β semiconjugates ga : α → α to gb : β → β if f ∘ ga = gb ∘ f;
function.semiconj₂:f : α → βsemiconjugates a binary operationga : α → α → αtogb : β → β → βiff (ga x y) = gb (f x) (f y)`;
f : α → α commutes with g : α → α if f ∘ g = g ∘ f, or equivalently `semiconj f g g`.

def function.semiconj {α : Type u_1} {β : Type u_2} (f : α → β) (ga : α → α) (gb : β → β) :

Prop

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) :

f ∘ ga = gb ∘ f

@[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.id_right {α : Type u_1} {β : Type u_2} {f : α → β} :

function.semiconj f id id

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

function.semiconj id ga ga

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'

theorem function.semiconj.option_map {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} (h : function.semiconj f ga gb) :

function.semiconj (option.map f) (option.map ga) (option.map gb)

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

Prop

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

@[refl]

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

function.commute f f

@[symm]

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

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

function.commute f id

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

function.commute id f

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

function.commute f g → function.commute (option.map f) (option.map 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₂.id_left {α : Type u_1} (op : α → α → α) :

function.semiconj₂ id op op

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