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 ?

class MonoidHom.CompTriple {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (φ : M →* N) (ψ : N →* P) (χ : outParam (M →* P)) : Prop

Class of composing triples

• comp_eq : ψ.comp φ = χ

  The maps form a commuting triangle

@[simp]

theorem MonoidHom.CompTriple.comp_eq {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : outParam (M →* P)} [self : φ.CompTriple ψ χ] : ψ.comp φ = χ

The maps form a commuting triangle

class MonoidHom.CompTriple.IsId {M : Type u_2} [Monoid M] (σ : M →* M) : Prop

Class of Id maps

• eq_id : σ = MonoidHom.id M

theorem MonoidHom.CompTriple.IsId.eq_id {M : Type u_2} [Monoid M] {σ : M →* M} [self : MonoidHom.CompTriple.IsId σ] : σ = MonoidHom.id M

instance MonoidHom.CompTriple.instIsId {M : Type u_5} [Monoid M] : MonoidHom.CompTriple.IsId (MonoidHom.id M)

Equations

• ⋯ = ⋯

instance MonoidHom.CompTriple.instIsIdOfIsIdCoe {M : Type u_2} [Monoid M] {σ : M →* M} [h : CompTriple.IsId ⇑σ] : MonoidHom.CompTriple.IsId σ

Equations

• ⋯ = ⋯

instance MonoidHom.CompTriple.instComp_id {N : Type u_5} {P : Type u_6} [Monoid N] [Monoid P] {φ : N →* N} [MonoidHom.CompTriple.IsId φ] {ψ : N →* P} : φ.CompTriple ψ ψ

Equations

• ⋯ = ⋯

instance MonoidHom.CompTriple.instId_comp {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] {φ : M →* N} {ψ : N →* N} [MonoidHom.CompTriple.IsId ψ] : φ.CompTriple ψ φ

Equations

• ⋯ = ⋯

theorem MonoidHom.CompTriple.comp_inv {M : Type u_2} {N : Type u_3} [Monoid M] [Monoid N] {φ : M →* N} {ψ : N →* M} (h : Function.RightInverse ⇑φ ⇑ψ) {χ : M →* M} [MonoidHom.CompTriple.IsId χ] : φ.CompTriple ψ χ

instance MonoidHom.CompTriple.instRootCompTriple {M : Type u_2} {N : Type u_3} {P : Type u_4} [Monoid M] [Monoid N] [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} [κ : φ.CompTriple ψ χ] : CompTriple ⇑φ ⇑ψ ⇑χ

Equations

• ⋯ = ⋯

theorem MonoidHom.CompTriple.comp {M : Type u_2} {N : Type u_3} {P : Type u_4} [Monoid M] [Monoid N] [Monoid P] {φ : M →* N} {ψ : N →* P} : φ.CompTriple ψ (ψ.comp φ)

φ, ψ and ψ.comp φ form a MonoidHom.CompTriple

(to be used with care, because no simplification is done)

theorem MonoidHom.CompTriple.comp_apply {M : Type u_2} {N : Type u_3} {P : Type u_4} [Monoid M] [Monoid N] [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} (h : φ.CompTriple ψ χ) (x : M) : ψ (φ x) = χ x

@[simp]

theorem MonoidHom.CompTriple.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} [Monoid M] [Monoid N] [Monoid P] {Q : Type u_5} [Monoid Q] {φ₁ : M →* N} {φ₂ : N →* P} {φ₁₂ : M →* P} (κ : φ₁.CompTriple φ₂ φ₁₂) {φ₃ : P →* Q} {φ₂₃ : N →* Q} (κ' : φ₂.CompTriple φ₃ φ₂₃) {φ₁₂₃ : M →* Q} : φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃