# Semiconjugate and commuting maps #

We define the following predicates:

- `Function.Semiconj`: `f : α → β` semiconjugates `ga : α → α` to `gb : β → β` if `f ∘ ga = gb ∘ 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`, or equivalently `Semiconj f g g`.

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

Instances For

source
theorem Function.semiconj_iff_comp_eq {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} :
Semiconj f ga gb ↔ f ∘ ga = gb ∘ f

Definition of `Function.Semiconj` in terms of functional equality.

source
theorem Function.Semiconj.comp_eq {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} :
Semiconj f ga gb → f ∘ ga = gb ∘ f

Alias of the forward direction of `Function.semiconj_iff_comp_eq`.

Definition of `Function.Semiconj` in terms of functional equality.

source
theorem Function.Semiconj.eq {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) (x : α) :
f (ga x) = gb (f x)
source
theorem Function.Semiconj.comp_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga ga' : α → α} {gb gb' : β → β} (h : Semiconj f ga gb) (h' : Semiconj f ga' gb') :
Semiconj f (ga ∘ ga') (gb ∘ gb')

If `f` semiconjugates `ga` to `gb` and `ga'` to `gb'`, then it semiconjugates `ga ∘ ga'` to `gb ∘ gb'`.

source
theorem Function.Semiconj.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {fab : α → β} {fbc : β → γ} {ga : α → α} {gb : β → β} {gc : γ → γ} (hab : Semiconj fab ga gb) (hbc : Semiconj fbc gb gc) :
Semiconj (fbc ∘ fab) ga gc

If `fab : α → β` semiconjugates `ga` to `gb` and `fbc : β → γ` semiconjugates `gb` to `gc`, then `fbc ∘ fab` semiconjugates `ga` to `gc`.

See also `Function.Semiconj.comp_left` for a version with reversed arguments.

source
theorem Function.Semiconj.comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {fab : α → β} {fbc : β → γ} {ga : α → α} {gb : β → β} {gc : γ → γ} (hbc : Semiconj fbc gb gc) (hab : Semiconj fab ga gb) :
Semiconj (fbc ∘ fab) ga gc

If `fbc : β → γ` semiconjugates `gb` to `gc` and `fab : α → β` semiconjugates `ga` to `gb`, then `fbc ∘ fab` semiconjugates `ga` to `gc`.

See also `Function.Semiconj.trans` for a version with reversed arguments.

Backward compatibility note: before 2024-01-13, this lemma used to have the same order of arguments that `Function.Semiconj.trans` has now.

source
theorem Function.Semiconj.id_right {α : Type u_1} {β : Type u_2} {f : α → β} :
Semiconj f id id

Any function semiconjugates the identity function to the identity function.

source
theorem Function.Semiconj.id_left {α : Type u_1} {ga : α → α} :
Semiconj id ga ga

The identity function semiconjugates any function to itself.

source
theorem Function.Semiconj.inverses_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga ga' : α → α} {gb gb' : β → β} (h : Semiconj f ga gb) (ha : RightInverse ga' ga) (hb : LeftInverse gb' gb) :
Semiconj f ga' gb'

If `f : α → β` semiconjugates `ga : α → α` to `gb : β → β`, `ga'` is a right inverse of `ga`, and `gb'` is a left inverse of `gb`, then `f` semiconjugates `ga'` to `gb'` as well.

source
theorem Function.Semiconj.inverse_left {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} {f' : β → α} (h : Semiconj f ga gb) (hf₁ : LeftInverse f' f) (hf₂ : RightInverse f' f) :
Semiconj f' gb ga

If `f` semiconjugates `ga` to `gb` and `f'` is both a left and a right inverse of `f`, then `f'` semiconjugates `gb` to `ga`.

source
theorem Function.Semiconj.option_map {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) :
Semiconj (Option.map f) (Option.map ga) (Option.map gb)

If `f : α → β` semiconjugates `ga : α → α` to `gb : β → β`, then `Option.map f` semiconjugates `Option.map ga` to `Option.map gb`.

source
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

Instances For

source
theorem Function.Semiconj.commute {α : Type u_1} {f g : α → α} (h : 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.

source
theorem Function.Commute.semiconj {α : Type u_1} {f g : α → α} (h : Function.Commute f g) :
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.

source
theorem Function.Commute.refl {α : Type u_1} (f : α → α) :
Function.Commute f f
source
theorem Function.Commute.symm {α : Type u_1} {f g : α → α} (h : Function.Commute f g) :
Function.Commute g f
source
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')

If `f` commutes with `g` and `g'`, then it commutes with `g ∘ g'`.

source
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

If `f` and `f'` commute with `g`, then `f ∘ f'` commutes with `g` as well.

source
theorem Function.Commute.id_right {α : Type u_1} {f : α → α} :
Function.Commute f id

Any self-map commutes with the identity map.

source
theorem Function.Commute.id_left {α : Type u_1} {f : α → α} :
Function.Commute id f

The identity map commutes with any self-map.

source
theorem Function.Commute.option_map {α : Type u_1} {f g : α → α} (h : Function.Commute f g) :
Function.Commute (Option.map f) (Option.map g)

If `f` commutes with `g`, then `Option.map f` commutes with `Option.map g`.

source
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 `MonoidHom` semiconjugates `(*)` to `(*)`.

Equations

- Function.Semiconj₂ f ga gb = ∀ (x y : α), f (ga x y) = gb (f x) (f y)

Instances For

source
theorem Function.Semiconj₂.eq {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} (h : Semiconj₂ f ga gb) (x y : α) :
f (ga x y) = gb (f x) (f y)
source
theorem Function.Semiconj₂.comp_eq {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} (h : Semiconj₂ f ga gb) :
bicompr f ga = bicompl gb f f
source
theorem Function.Semiconj₂.id_left {α : Type u_1} (op : α → α → α) :
Semiconj₂ id op op
source
theorem Function.Semiconj₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {ga : α → α → α} {gb : β → β → β} {f' : β → γ} {gc : γ → γ → γ} (hf' : Semiconj₂ f' gb gc) (hf : Semiconj₂ f ga gb) :
Semiconj₂ (f' ∘ f) ga gc
source
theorem Function.Semiconj₂.isAssociative_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [Std.Associative ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) :
Std.Associative gb
source
theorem Function.Semiconj₂.isAssociative_left {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [Std.Associative gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) :
Std.Associative ga
source
theorem Function.Semiconj₂.isIdempotent_right {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [Std.IdempotentOp ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) :
Std.IdempotentOp gb
source
theorem Function.Semiconj₂.isIdempotent_left {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [Std.IdempotentOp gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) :
Std.IdempotentOp ga