doc-next-gen

Mathlib.Algebra.Group.Hom.CompTypeclasses

Module docstring

{"# Propositional typeclasses on several monoid homs

This file contains typeclasses used in the definition of equivariant maps, in the spirit what was initially developed by Frédéric Dupuis and Heather Macbeth for linear maps. However, we do not expect that all maps should be guessed automatically, as it happens for linear maps.

If φ, ψ… are monoid homs and M, N… are monoids, we add two instances: * MonoidHom.CompTriple φ ψ χ, which expresses that ψ.comp φ = χ * MonoidHom.IsId φ, which expresses that φ = id

Some basic lemmas are proved: * MonoidHom.CompTriple.comp asserts MonoidHom.CompTriple φ ψ (ψ.comp φ) * MonoidHom.CompTriple.id_comp asserts MonoidHom.CompTriple φ ψ ψ in the presence of MonoidHom.IsId φ * its variant MonoidHom.CompTriple.comp_id

TODO : * align with RingHomCompTriple * probably rename MonoidHom.CompTriple as MonoidHomCompTriple (or, on the opposite, rename RingHomCompTriple as RingHom.CompTriple) * does one need AddHom.CompTriple ?

"}

MonoidHom.CompTriple structure
{M N P : Type*} [Monoid M] [Monoid N] [Monoid P] (φ : M →* N) (ψ : N →* P) (χ : outParam (M →* P))
Full source 
/-- Class of composing triples -/
class CompTriple {M N P : Type*} [Monoid M] [Monoid N] [Monoid P]
    (φ : M →* N) (ψ : N →* P) (χ : outParam (M →* P)) : Prop where
  /-- The maps form a commuting triangle -/
  comp_eq : ψ.comp φ = χ
Composition Triple of Monoid Homomorphisms
Informal description
The structure `MonoidHom.CompTriple` represents a triple of monoid homomorphisms $(φ, ψ, χ)$ between monoids $M$, $N$, and $P$ such that the composition $ψ \circ φ$ equals $χ$. In other words, for all $x \in M$, we have $ψ(φ(x)) = χ(x)$.
MonoidHom.CompTriple.IsId structure
(σ : M →* M)
Full source 
/-- Class of Id maps -/
class IsId (σ : M →* M) : Prop where
  eq_id : σ = MonoidHom.id M
Identity monoid homomorphism property
Informal description
The structure `MonoidHom.CompTriple.IsId` represents the property that a monoid homomorphism $\sigma: M \to M$ is equal to the identity homomorphism on $M$.
MonoidHom.CompTriple.instIsId instance
{M : Type*} [Monoid M] : IsId (MonoidHom.id M)
Full source 
instance instIsId {M : Type*} [Monoid M] : IsId (MonoidHom.id M) where
  eq_id := rfl
Identity Monoid Homomorphism is Identity
Informal description
For any monoid $M$, the identity monoid homomorphism $\text{id}_M: M \to M$ satisfies the identity property.
MonoidHom.CompTriple.instIsIdOfIsIdCoe instance
{σ : M →* M} [h : _root_.CompTriple.IsId σ] : IsId σ
Full source 
instance {σ : M →* M} [h : _root_.CompTriple.IsId σ] : IsId σ  where
  eq_id := by ext; exact congr_fun h.eq_id _
Identity Function Implies Identity Monoid Homomorphism
Informal description
For any monoid homomorphism $\sigma: M \to M$, if $\sigma$ is equal to the identity function (as witnessed by `CompTriple.IsId`), then $\sigma$ is also equal to the identity monoid homomorphism.
MonoidHom.CompTriple.instComp_id instance
{N P : Type*} [Monoid N] [Monoid P] {φ : N →* N} [IsId φ] {ψ : N →* P} : CompTriple φ ψ ψ
Full source 
instance instComp_id {N P : Type*} [Monoid N] [Monoid P]
    {φ : N →* N} [IsId φ] {ψ : N →* P} :
    CompTriple φ ψ ψ where
  comp_eq := by simp only [IsId.eq_id, MonoidHom.comp_id]
Composition with Identity Monoid Homomorphism Preserves the Homomorphism
Informal description
For any monoids $N$ and $P$, if $\phi: N \to N$ is the identity monoid homomorphism and $\psi: N \to P$ is any monoid homomorphism, then the composition $\psi \circ \phi$ equals $\psi$.
MonoidHom.CompTriple.instId_comp instance
{M N : Type*} [Monoid M] [Monoid N] {φ : M →* N} {ψ : N →* N} [IsId ψ] : CompTriple φ ψ φ
Full source 
instance instId_comp {M N : Type*} [Monoid M] [Monoid N]
    {φ : M →* N} {ψ : N →* N} [IsId ψ] :
    CompTriple φ ψ φ where
  comp_eq := by simp only [IsId.eq_id, MonoidHom.id_comp]
Composition with Identity Monoid Homomorphism Preserves the Homomorphism
Informal description
For any monoids $M$ and $N$, if $\psi: N \to N$ is the identity monoid homomorphism and $\phi: M \to N$ is any monoid homomorphism, then the composition $\psi \circ \phi$ equals $\phi$.
MonoidHom.CompTriple.comp_inv theorem
{φ : M →* N} {ψ : N →* M} (h : Function.RightInverse φ ψ) {χ : M →* M} [IsId χ] : CompTriple φ ψ χ
Full source 
lemma comp_inv {φ : M →* N} {ψ : N →* M} (h : Function.RightInverse φ ψ)
    {χ : M →* M} [IsId χ] :
    CompTriple φ ψ χ where
  comp_eq := by simp only [IsId.eq_id, ← DFunLike.coe_fn_eq, coe_comp, h.id, coe_id]
Composition Triple for Right Inverse Monoid Homomorphisms with Identity
Informal description
Let $M$ and $N$ be monoids, and let $\phi \colon M \to N$ and $\psi \colon N \to M$ be monoid homomorphisms such that $\psi$ is a right inverse of $\phi$ (i.e., $\phi \circ \psi = \text{id}_N$). If $\chi \colon M \to M$ is the identity homomorphism, then the triple $(\phi, \psi, \chi)$ forms a composition triple, meaning that $\psi(\phi(x)) = \chi(x) = x$ for all $x \in M$.
MonoidHom.CompTriple.instRootCompTriple instance
{φ : M →* N} {ψ : N →* P} {χ : M →* P} [κ : CompTriple φ ψ χ] : _root_.CompTriple φ ψ χ
Full source 
instance instRootCompTriple {φ : M →* N} {ψ : N →* P} {χ : M →* P} [κ : CompTriple φ ψ χ] :
    _root_.CompTriple φ ψ χ where
  comp_eq := by rw [← MonoidHom.coe_comp, κ.comp_eq]
Root Composition Triple from Monoid Homomorphism Composition Triple
Informal description
For any monoid homomorphisms $\phi \colon M \to N$, $\psi \colon N \to P$, and $\chi \colon M \to P$ such that $\psi \circ \phi = \chi$ (as formalized by the `CompTriple` structure), the triple $(\phi, \psi, \chi)$ also forms a composition triple in the root namespace.
MonoidHom.CompTriple.comp theorem
{φ : M →* N} {ψ : N →* P} : CompTriple φ ψ (ψ.comp φ)
Full source 
/-- `φ`, `ψ` and `ψ.comp φ` form a `MonoidHom.CompTriple`

  (to be used with care, because no simplification is done) -/
theorem comp {φ : M →* N} {ψ : N →* P} :
    CompTriple φ ψ (ψ.comp φ) where
  comp_eq := rfl
Composition Triple of Monoid Homomorphisms
Informal description
For any monoid homomorphisms $\phi \colon M \to N$ and $\psi \colon N \to P$, the triple $(\phi, \psi, \psi \circ \phi)$ forms a composition triple, meaning that $\psi(\phi(x)) = (\psi \circ \phi)(x)$ for all $x \in M$.
MonoidHom.CompTriple.comp_apply theorem
{φ : M →* N} {ψ : N →* P} {χ : M →* P} (h : CompTriple φ ψ χ) (x : M) : ψ (φ x) = χ x
Full source 
lemma comp_apply
    {φ : M →* N} {ψ : N →* P} {χ : M →* P} (h : CompTriple φ ψ χ) (x : M) :
    ψ (φ x) = χ x := by
  rw [← h.comp_eq, MonoidHom.comp_apply]
Composition Triple Evaluation: $\psi(\phi(x)) = \chi(x)$
Informal description
For monoid homomorphisms $\phi \colon M \to N$, $\psi \colon N \to P$, and $\chi \colon M \to P$ forming a composition triple (i.e., $\psi \circ \phi = \chi$), and for any element $x \in M$, we have $\psi(\phi(x)) = \chi(x)$.
MonoidHom.CompTriple.comp_assoc theorem
{Q : Type*} [Monoid Q] {φ₁ : M →* N} {φ₂ : N →* P} {φ₁₂ : M →* P} (κ : CompTriple φ₁ φ₂ φ₁₂) {φ₃ : P →* Q} {φ₂₃ : N →* Q} (κ' : CompTriple φ₂ φ₃ φ₂₃) {φ₁₂₃ : M →* Q} : CompTriple φ₁ φ₂₃ φ₁₂₃ ↔ CompTriple φ₁₂ φ₃ φ₁₂₃
Full source 
theorem comp_assoc {Q : Type*} [Monoid Q]
    {φ₁ : M →* N} {φ₂ : N →* P} {φ₁₂ : M →* P}
    (κ : CompTriple φ₁ φ₂ φ₁₂)
    {φ₃ : P →* Q} {φ₂₃ : N →* Q} (κ' : CompTriple φ₂ φ₃ φ₂₃)
    {φ₁₂₃ : M →* Q} :
    CompTripleCompTriple φ₁ φ₂₃ φ₁₂₃ ↔ CompTriple φ₁₂ φ₃ φ₁₂₃ := by
  constructor <;>
  · rintro ⟨h⟩
    exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩
Associativity of Composition Triples for Monoid Homomorphisms
Informal description
Let $M$, $N$, $P$, and $Q$ be monoids, and let $\phi_1 \colon M \to N$, $\phi_2 \colon N \to P$, and $\phi_3 \colon P \to Q$ be monoid homomorphisms. Suppose we have composition triples $(\phi_1, \phi_2, \phi_{12})$ and $(\phi_2, \phi_3, \phi_{23})$. Then, the composition triple $(\phi_1, \phi_{23}, \phi_{123})$ holds if and only if the composition triple $(\phi_{12}, \phi_3, \phi_{123})$ holds. In other words, the associativity of composition triples is equivalent to the associativity of the underlying monoid homomorphisms.