Documentation

Mathlib.Logic.Function.Conjugate

Semiconjugate and commuting maps #

We define the following predicates:

Function.Semiconj: f : α → β→ β semiconjugates ga : α → α→ α to gb : β → β→ β if f ∘ ga = gb ∘ f∘ ga = gb ∘ f∘ f;
Function.Semiconj₂: f : α → β→ β semiconjugates a binary operation ga : α → α → α→ α → α→ α to gb : β → β → β→ β → β→ β if f (ga x y) = gb (f x) (f y);
Function.Commute: f : α → α→ α commutes with g : α → α→ α if f ∘ g = g ∘ f∘ g = g ∘ f∘ f, or equivalently Semiconj f g g.

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

We say that f : α → β→ β semiconjugates ga : α → α→ α to gb : β → β→ β if f ∘ ga = gb ∘ f∘ ga = gb ∘ f∘ f. We use ∀ x, f (ga x) = gb (f x)∀ 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∘ ga = gb ∘ f∘ 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 : β → β} (h : 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' : β → β} (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.RightInverse ga' ga) (hb : Function.LeftInverse 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 : α → α) :

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∘ g = g ∘ f∘ 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

Reinterpret Function.Semiconj f g g as Function.Commute f g. These two predicates are definitionally equal but have different dot-notation lemmas.

theorem Function.Commute.semiconj {α : Type u_1} {f : α → α} {g : α → α} (h : Function.Commute f g) :

Function.Semiconj f g g

Reinterpret Function.Commute f g as Function.Semiconj f g g. These two predicates are definitionally equal but have different dot-notation lemmas.

theorem Function.Commute.refl {α : Type u_1} (f : α → α) :

Function.Commute f f

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

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 MonoidHom 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 : β → β → β} (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_3} {β : Type u_1} {γ : Type u_2} {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₂.isAssociative_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [inst : IsAssociative α ga] (h : Function.Semiconj₂ f ga gb) (h_surj : Function.Surjective f) :

IsAssociative β gb

theorem Function.Semiconj₂.isAssociative_left {α : Type u_2} {β : Type u_1} {f : α → β} {ga : α → α → α} {gb : β → β → β} [inst : IsAssociative β gb] (h : Function.Semiconj₂ f ga gb) (h_inj : Function.Injective f) :

IsAssociative α ga

theorem Function.Semiconj₂.isIdempotent_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [inst : IsIdempotent α ga] (h : Function.Semiconj₂ f ga gb) (h_surj : Function.Surjective f) :

IsIdempotent β gb

theorem Function.Semiconj₂.isIdempotent_left {α : Type u_2} {β : Type u_1} {f : α → β} {ga : α → α → α} {gb : β → β → β} [inst : IsIdempotent β gb] (h : Function.Semiconj₂ f ga gb) (h_inj : Function.Injective f) :

IsIdempotent α ga