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 : MonoidHom.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

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

Equations

• ⋯ = ⋯

instance MonoidHom.CompTriple.instIsId_1 {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} : MonoidHom.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 ψ] : MonoidHom.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 χ] : MonoidHom.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} [κ : MonoidHom.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} : MonoidHom.CompTriple φ ψ (MonoidHom.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 : MonoidHom.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} (κ : MonoidHom.CompTriple φ₁ φ₂ φ₁₂) {φ₃ : P →* Q} {φ₂₃ : N →* Q} (κ' : MonoidHom.CompTriple φ₂ φ₃ φ₂₃) {φ₁₂₃ : M →* Q} : MonoidHom.CompTriple φ₁ φ₂₃ φ₁₂₃ ↔ MonoidHom.CompTriple φ₁₂ φ₃ φ₁₂₃