Mathlib.Logic.Function.Conjugate

Function.Semiconj definition

(f : α → β) (ga : α → α) (gb : β → β) : Prop

Full source

/--
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`.
-/
def Semiconj (f : α → β) (ga : α → α) (gb : β → β) : Prop :=
  ∀ x, f (ga x) = gb (f x)

Semiconjugate functions

Informal description

A function $f : \alpha \to \beta$ is said to semiconjugate functions $g_a : \alpha \to \alpha$ and $g_b : \beta \to \beta$ if for all $x \in \alpha$, the equality $f(g_a(x)) = g_b(f(x))$ holds. This is equivalent to the composition condition $f \circ g_a = g_b \circ f$.

Function.semiconj_iff_comp_eq theorem

: Semiconj f ga gb ↔ f ∘ ga = gb ∘ f

Full source

/-- Definition of `Function.Semiconj` in terms of functional equality. -/
lemma _root_.Function.semiconj_iff_comp_eq : SemiconjSemiconj f ga gb ↔ f ∘ ga = gb ∘ f := funext_iff.symm

Semiconjugacy Condition via Function Composition

Informal description

A function $f : \alpha \to \beta$ semiconjugates $g_a : \alpha \to \alpha$ to $g_b : \beta \to \beta$ if and only if the composition $f \circ g_a$ is equal to $g_b \circ f$.

Function.Semiconj.eq theorem

(h : Semiconj f ga gb) (x : α) : f (ga x) = gb (f x)

Full source

protected theorem eq (h : Semiconj f ga gb) (x : α) : f (ga x) = gb (f x) :=
  h x

Semiconjugate Functions Satisfy Pointwise Equality

Informal description

Given a semiconjugate relation between functions $f : \alpha \to \beta$, $g_a : \alpha \to \alpha$, and $g_b : \beta \to \beta$, for any $x \in \alpha$, we have $f(g_a(x)) = g_b(f(x))$.

Function.Semiconj.comp_right theorem

(h : Semiconj f ga gb) (h' : Semiconj f ga' gb') : Semiconj f (ga ∘ ga') (gb ∘ gb')

Full source

/-- If `f` semiconjugates `ga` to `gb` and `ga'` to `gb'`,
then it semiconjugates `ga ∘ ga'` to `gb ∘ gb'`. -/
theorem comp_right (h : Semiconj f ga gb) (h' : Semiconj f ga' gb') :
    Semiconj f (ga ∘ ga') (gb ∘ gb') := fun x ↦ by
  simp only [comp_apply, h.eq, h'.eq]

Composition of Semiconjugate Functions Preserves Semiconjugacy

Informal description

Let $f : \alpha \to \beta$ be a function that semiconjugates $g_a$ to $g_b$ (i.e., $f \circ g_a = g_b \circ f$) and also semiconjugates $g_a'$ to $g_b'$. Then $f$ semiconjugates the composition $g_a \circ g_a'$ to $g_b \circ g_b'$, meaning that $f \circ (g_a \circ g_a') = (g_b \circ g_b') \circ f$.

Function.Semiconj.trans theorem

(hab : Semiconj fab ga gb) (hbc : Semiconj fbc gb gc) : Semiconj (fbc ∘ fab) ga gc

Full source

/-- 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. -/
protected theorem trans (hab : Semiconj fab ga gb) (hbc : Semiconj fbc gb gc) :
    Semiconj (fbc ∘ fab) ga gc := fun x ↦ by
  simp only [comp_apply, hab.eq, hbc.eq]

Transitivity of Semiconjugate Functions: $f_{bc} \circ f_{ab}$ Semiconjugates $g_a$ to $g_c$

Informal description

Let $f_{ab} : \alpha \to \beta$ be a function that semiconjugates $g_a : \alpha \to \alpha$ to $g_b : \beta \to \beta$ (i.e., $f_{ab} \circ g_a = g_b \circ f_{ab}$), and let $f_{bc} : \beta \to \gamma$ be a function that semiconjugates $g_b$ to $g_c : \gamma \to \gamma$. Then the composition $f_{bc} \circ f_{ab}$ semiconjugates $g_a$ to $g_c$, meaning that $(f_{bc} \circ f_{ab}) \circ g_a = g_c \circ (f_{bc} \circ f_{ab})$.

Function.Semiconj.comp_left theorem

(hbc : Semiconj fbc gb gc) (hab : Semiconj fab ga gb) : Semiconj (fbc ∘ fab) ga gc

Full source

/-- 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. -/
theorem comp_left (hbc : Semiconj fbc gb gc) (hab : Semiconj fab ga gb) :
    Semiconj (fbc ∘ fab) ga gc :=
  hab.trans hbc

Composition of Semiconjugate Functions: $f_{bc} \circ f_{ab}$ Semiconjugates $g_a$ to $g_c$

Informal description

Let $f_{ab} : \alpha \to \beta$ be a function that semiconjugates $g_a : \alpha \to \alpha$ to $g_b : \beta \to \beta$ (i.e., $f_{ab} \circ g_a = g_b \circ f_{ab}$), and let $f_{bc} : \beta \to \gamma$ be a function that semiconjugates $g_b$ to $g_c : \gamma \to \gamma$. Then the composition $f_{bc} \circ f_{ab}$ semiconjugates $g_a$ to $g_c$, meaning that $(f_{bc} \circ f_{ab}) \circ g_a = g_c \circ (f_{bc} \circ f_{ab})$.

Function.Semiconj.id_right theorem

: Semiconj f id id

Full source

/-- Any function semiconjugates the identity function to the identity function. -/
theorem id_right : Semiconj f id id := fun _ ↦ rfl

Identity Functions are Semiconjugate via Any Function

Informal description

For any function $f : \alpha \to \beta$, the identity function $\mathrm{id} : \alpha \to \alpha$ is semiconjugate to the identity function $\mathrm{id} : \beta \to \beta$ via $f$. In other words, $f \circ \mathrm{id} = \mathrm{id} \circ f$.

Function.Semiconj.id_left theorem

: Semiconj id ga ga

Full source

/-- The identity function semiconjugates any function to itself. -/
theorem id_left : Semiconj id ga ga := fun _ ↦ rfl

Identity Function Semiconjugates Any Function to Itself

Informal description

The identity function $\mathrm{id} : \alpha \to \alpha$ semiconjugates any function $g_a : \alpha \to \alpha$ to itself, i.e., $\mathrm{id} \circ g_a = g_a \circ \mathrm{id}$.

Function.Semiconj.inverses_right theorem

(h : Semiconj f ga gb) (ha : RightInverse ga' ga) (hb : LeftInverse gb' gb) : Semiconj f ga' gb'

Full source

/-- 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. -/
theorem inverses_right (h : Semiconj f ga gb) (ha : RightInverse ga' ga) (hb : LeftInverse gb' gb) :
    Semiconj f ga' gb' := fun x ↦ by
  rw [← hb (f (ga' x)), ← h.eq, ha x]

Semiconjugacy of Inverses under Semiconjugate Functions

Informal description

Let $f : \alpha \to \beta$ be a function that semiconjugates $g_a : \alpha \to \alpha$ to $g_b : \beta \to \beta$, i.e., $f \circ g_a = g_b \circ f$. If $g_a'$ is a right inverse of $g_a$ and $g_b'$ is a left inverse of $g_b$, then $f$ also semiconjugates $g_a'$ to $g_b'$.

Function.Semiconj.inverse_left theorem

{f' : β → α} (h : Semiconj f ga gb) (hf₁ : LeftInverse f' f) (hf₂ : RightInverse f' f) : Semiconj f' gb ga

Full source

/-- If `f` semiconjugates `ga` to `gb` and `f'` is both a left and a right inverse of `f`,
then `f'` semiconjugates `gb` to `ga`. -/
lemma inverse_left {f' : β → α} (h : Semiconj f ga gb)
    (hf₁ : LeftInverse f' f) (hf₂ : RightInverse f' f) : Semiconj f' gb ga := fun x ↦ by
  rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]

Inverse Function Semiconjugacy Theorem

Informal description

Let $f : \alpha \to \beta$ be a function that semiconjugates $g_a : \alpha \to \alpha$ to $g_b : \beta \to \beta$, i.e., $f \circ g_a = g_b \circ f$. If $f' : \beta \to \alpha$ is both a left and right inverse of $f$, then $f'$ semiconjugates $g_b$ to $g_a$, i.e., $f' \circ g_b = g_a \circ f'$.

Function.Semiconj.option_map theorem

 {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) : Semiconj (Option.map f) (Option.map ga) (Option.map gb)

Full source

/-- If `f : α → β` semiconjugates `ga : α → α` to `gb : β → β`,
then `Option.map f` semiconjugates `Option.map ga` to `Option.map gb`. -/
theorem option_map {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) :
    Semiconj (Option.map f) (Option.map ga) (Option.map gb)
  | none => rfl
  | some _ => congr_arg some <| h _

Lifting Semiconjugacy to Option Maps

Informal description

Let $f : \alpha \to \beta$ be a function that semiconjugates $g_a : \alpha \to \alpha$ to $g_b : \beta \to \beta$, meaning that $f \circ g_a = g_b \circ f$. Then the lifted function $\text{Option.map}\, f$ semiconjugates $\text{Option.map}\, g_a$ to $\text{Option.map}\, g_b$.

Function.Commute definition

(f g : α → α) : Prop

Full source

/--
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`.
-/
protected def Commute (f g : α → α) : Prop :=
  Semiconj f g g

Commuting functions

Informal description

Two functions $f, g : \alpha \to \alpha$ commute if for all $x \in \alpha$, the equality $f(g(x)) = g(f(x))$ holds. This is equivalent to the composition condition $f \circ g = g \circ f$.

Function.Semiconj.commute theorem

{f g : α → α} (h : Semiconj f g g) : Commute f g

Full source

/-- Reinterpret `Function.Semiconj f g g` as `Function.Commute f g`. These two predicates are
definitionally equal but have different dot-notation lemmas. -/
theorem Semiconj.commute {f g : α → α} (h : Semiconj f g g) : Commute f g := h

Semiconjugacy Implies Commutation of Functions

Informal description

Given two functions $f, g : \alpha \to \alpha$, if $f$ semiconjugates $g$ to itself (i.e., $f \circ g = g \circ f$), then $f$ and $g$ commute.

Function.Commute.semiconj theorem

(h : Commute f g) : Semiconj f g g

Full source

/-- Reinterpret `Function.Commute f g` as `Function.Semiconj f g g`. These two predicates are
definitionally equal but have different dot-notation lemmas. -/
theorem semiconj (h : Commute f g) : Semiconj f g g := h

Commuting Functions Imply Semiconjugation

Informal description

If two functions $f, g : \alpha \to \alpha$ commute, then $f$ semiconjugates $g$ to itself, i.e., $f \circ g = g \circ f$.

Function.Commute.refl theorem

(f : α → α) : Commute f f

Full source

@[refl]
theorem refl (f : α → α) : Commute f f := fun _ ↦ Eq.refl _

Reflexivity of Function Commutation

Informal description

For any function $f : \alpha \to \alpha$, the function $f$ commutes with itself, i.e., $f \circ f = f \circ f$.

Function.Commute.symm theorem

(h : Commute f g) : Commute g f

Full source

@[symm]
theorem symm (h : Commute f g) : Commute g f := fun x ↦ (h x).symm

Symmetry of Function Commutation

Informal description

If two functions $f, g : \alpha \to \alpha$ commute, then $g$ and $f$ also commute, i.e., $g \circ f = f \circ g$.

Function.Commute.comp_right theorem

(h : Commute f g) (h' : Commute f g') : Commute f (g ∘ g')

Full source

/-- If `f` commutes with `g` and `g'`, then it commutes with `g ∘ g'`. -/
theorem comp_right (h : Commute f g) (h' : Commute f g') : Commute f (g ∘ g') :=
  Semiconj.comp_right h h'

Composition Preserves Commutation of Functions

Informal description

If a function $f : \alpha \to \alpha$ commutes with both $g$ and $g'$, then $f$ also commutes with their composition $g \circ g'$, i.e., $f \circ (g \circ g') = (g \circ g') \circ f$.

Function.Commute.comp_left theorem

(h : Commute f g) (h' : Commute f' g) : Commute (f ∘ f') g

Full source

/-- If `f` and `f'` commute with `g`, then `f ∘ f'` commutes with `g` as well. -/
nonrec theorem comp_left (h : Commute f g) (h' : Commute f' g) : Commute (f ∘ f') g :=
  h.comp_left h'

Composition of Commuting Functions Preserves Commutation with $g$

Informal description

If two functions $f, f' : \alpha \to \alpha$ both commute with a function $g : \alpha \to \alpha$, then their composition $f \circ f'$ also commutes with $g$, i.e., $(f \circ f') \circ g = g \circ (f \circ f')$.

Function.Commute.id_right theorem

: Commute f id

Full source

/-- Any self-map commutes with the identity map. -/
theorem id_right : Commute f id := Semiconj.id_right

Right Commutation with Identity Function

Informal description

For any function $f : \alpha \to \alpha$, the identity function $\mathrm{id} : \alpha \to \alpha$ commutes with $f$, i.e., $f \circ \mathrm{id} = \mathrm{id} \circ f$.

Function.Commute.id_left theorem

: Commute id f

Full source

/-- The identity map commutes with any self-map. -/
theorem id_left : Commute id f :=
  Semiconj.id_left

Identity Function Commutes with Any Function

Informal description

The identity function $\mathrm{id} : \alpha \to \alpha$ commutes with any function $f : \alpha \to \alpha$, i.e., $\mathrm{id} \circ f = f \circ \mathrm{id}$.

Function.Commute.option_map theorem

{f g : α → α} (h : Commute f g) : Commute (Option.map f) (Option.map g)

Full source

/-- If `f` commutes with `g`, then `Option.map f` commutes with `Option.map g`. -/
nonrec theorem option_map {f g : α → α} (h : Commute f g) : Commute (Option.map f) (Option.map g) :=
  h.option_map

Commutation of Lifted Functions on Option Type

Informal description

If two functions $f, g : \alpha \to \alpha$ commute (i.e., $f \circ g = g \circ f$), then their lifted versions $\text{Option.map}\, f$ and $\text{Option.map}\, g$ also commute.

Function.Semiconj₂ definition

(f : α → β) (ga : α → α → α) (gb : β → β → β) : Prop

Full source

/--
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 `(*)`.
-/
def Semiconj₂ (f : α → β) (ga : α → α → α) (gb : β → β → β) : Prop :=
  ∀ x y, f (ga x y) = gb (f x) (f y)

Semiconjugacy of binary operations

Informal description

A function $ f : \alpha \to \beta $ semiconjugates a binary operation $ g_a : \alpha \to \alpha \to \alpha $ to a binary operation $ g_b : \beta \to \beta \to \beta $ if for all $ x, y \in \alpha $, the equation $ f(g_a(x, y)) = g_b(f(x), f(y)) $ holds. For example, a monoid homomorphism semiconjugates the multiplication operation to itself.

Function.Semiconj₂.eq theorem

(h : Semiconj₂ f ga gb) (x y : α) : f (ga x y) = gb (f x) (f y)

Full source

protected theorem eq (h : Semiconj₂ f ga gb) (x y : α) : f (ga x y) = gb (f x) (f y) :=
  h x y

Semiconjugacy Equation for Binary Operations

Informal description

Given a function $f \colon \alpha \to \beta$ that semiconjugates binary operations $g_a \colon \alpha \to \alpha \to \alpha$ and $g_b \colon \beta \to \beta \to \beta$, then for any $x, y \in \alpha$, we have $f(g_a(x, y)) = g_b(f(x), f(y))$.

Function.Semiconj₂.comp_eq theorem

(h : Semiconj₂ f ga gb) : bicompr f ga = bicompl gb f f

Full source

protected theorem comp_eq (h : Semiconj₂ f ga gb) : bicompr f ga = bicompl gb f f :=
  funext fun x ↦ funext <| h x

Composition Equality for Semiconjugate Binary Operations

Informal description

Given a function $f \colon \alpha \to \beta$ that semiconjugates a binary operation $g_a \colon \alpha \to \alpha \to \alpha$ to $g_b \colon \beta \to \beta \to \beta$, the composition of $f$ with $g_a$ equals the composition of $g_b$ with $f$ on both arguments, i.e., $f \circ g_a = g_b \circ (f \times f)$.

Function.Semiconj₂.id_left theorem

(op : α → α → α) : Semiconj₂ id op op

Full source

theorem id_left (op : α → α → α) : Semiconj₂ id op op := fun _ _ ↦ rfl

Identity Function Semiconjugates Any Binary Operation to Itself

Informal description

For any binary operation $\mathrm{op} : \alpha \to \alpha \to \alpha$, the identity function $\mathrm{id} : \alpha \to \alpha$ semiconjugates $\mathrm{op}$ to itself, i.e., $\mathrm{id}(\mathrm{op}(x, y)) = \mathrm{op}(\mathrm{id}(x), \mathrm{id}(y))$ for all $x, y \in \alpha$.

Function.Semiconj₂.comp theorem

 {f' : β → γ} {gc : γ → γ → γ} (hf' : Semiconj₂ f' gb gc) (hf : Semiconj₂ f ga gb) : Semiconj₂ (f' ∘ f) ga gc

Full source

theorem comp {f' : β → γ} {gc : γ → γ → γ} (hf' : Semiconj₂ f' gb gc) (hf : Semiconj₂ f ga gb) :
    Semiconj₂ (f' ∘ f) ga gc := fun x y ↦ by simp only [hf'.eq, hf.eq, comp_apply]

Composition of Semiconjugate Binary Operations Preserves Semiconjugacy

Informal description

Let $f \colon \alpha \to \beta$ and $f' \colon \beta \to \gamma$ be functions, and let $g_a \colon \alpha \to \alpha \to \alpha$, $g_b \colon \beta \to \beta \to \beta$, and $g_c \colon \gamma \to \gamma \to \gamma$ be binary operations. If $f$ semiconjugates $g_a$ to $g_b$ and $f'$ semiconjugates $g_b$ to $g_c$, then the composition $f' \circ f$ semiconjugates $g_a$ to $g_c$, i.e., $(f' \circ f)(g_a(x, y)) = g_c((f' \circ f)(x), (f' \circ f)(y))$ for all $x, y \in \alpha$.

Function.Semiconj₂.isAssociative_right theorem

[Std.Associative ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) : Std.Associative gb

Full source

theorem isAssociative_right [Std.Associative ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) :
    Std.Associative gb :=
  ⟨h_surj.forall₃.2 fun x₁ x₂ x₃ ↦ by simp only [← h.eq, Std.Associative.assoc (op := ga)]⟩

Surjective Semiconjugacy Preserves Associativity of Binary Operations

Informal description

Let $f \colon \alpha \to \beta$ be a surjective function that semiconjugates an associative binary operation $g_a \colon \alpha \to \alpha \to \alpha$ to a binary operation $g_b \colon \beta \to \beta \to \beta$, i.e., $f(g_a(x, y)) = g_b(f(x), f(y))$ for all $x, y \in \alpha$. Then $g_b$ is also associative.

Function.Semiconj₂.isAssociative_left theorem

[Std.Associative gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) : Std.Associative ga

Full source

theorem isAssociative_left [Std.Associative gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) :
    Std.Associative ga :=
  ⟨fun x₁ x₂ x₃ ↦ h_inj <| by simp only [h.eq, Std.Associative.assoc (op := gb)]⟩

Injective Semiconjugacy Preserves Associativity of Binary Operations

Informal description

Let $f \colon \alpha \to \beta$ be an injective function that semiconjugates a binary operation $g_a \colon \alpha \to \alpha \to \alpha$ to an associative binary operation $g_b \colon \beta \to \beta \to \beta$, i.e., $f(g_a(x, y)) = g_b(f(x), f(y))$ for all $x, y \in \alpha$. Then $g_a$ is also associative.

Function.Semiconj₂.isIdempotent_right theorem

[Std.IdempotentOp ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) : Std.IdempotentOp gb

Full source

theorem isIdempotent_right [Std.IdempotentOp ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) :
    Std.IdempotentOp gb :=
  ⟨h_surj.forall.2 fun x ↦ by simp only [← h.eq, Std.IdempotentOp.idempotent (op := ga)]⟩

Surjective Semiconjugacy Preserves Idempotence of Binary Operations

Informal description

Let $f \colon \alpha \to \beta$ be a surjective function that semiconjugates an idempotent binary operation $g_a \colon \alpha \to \alpha \to \alpha$ to a binary operation $g_b \colon \beta \to \beta \to \beta$, i.e., $f(g_a(x, y)) = g_b(f(x), f(y))$ for all $x, y \in \alpha$. Then $g_b$ is also idempotent.

Function.Semiconj₂.isIdempotent_left theorem

[Std.IdempotentOp gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) : Std.IdempotentOp ga

Full source

theorem isIdempotent_left [Std.IdempotentOp gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) :
    Std.IdempotentOp ga :=
  ⟨fun x ↦ h_inj <| by rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]⟩

Injective Semiconjugacy Preserves Idempotence of Binary Operations

Informal description

Let $f \colon \alpha \to \beta$ be a function that semiconjugates a binary operation $g_a \colon \alpha \to \alpha \to \alpha$ to a binary operation $g_b \colon \beta \to \beta \to \beta$, i.e., $f(g_a(x, y)) = g_b(f(x), f(y))$ for all $x, y \in \alpha$. If $g_b$ is idempotent and $f$ is injective, then $g_a$ is also idempotent.