# 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 ?

source
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

Instances

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

Class of Id maps

- eq_id : σ = id M

Instances

source
instance MonoidHom.CompTriple.instIsId {M : Type u_4} [Monoid M] :
IsId (id M)
source
instance MonoidHom.CompTriple.instIsIdOfIsIdCoe {M : Type u_1} [Monoid M] {σ : M →* M} [h : _root_.CompTriple.IsId ⇑σ] :
IsId σ
source
instance MonoidHom.CompTriple.instComp_id {N : Type u_4} {P : Type u_5} [Monoid N] [Monoid P] {φ : N →* N} [IsId φ] {ψ : N →* P} :
φ.CompTriple ψ ψ
source
instance MonoidHom.CompTriple.instId_comp {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {φ : M →* N} {ψ : N →* N} [IsId ψ] :
φ.CompTriple ψ φ
source
theorem MonoidHom.CompTriple.comp_inv {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {φ : M →* N} {ψ : N →* M} (h : Function.RightInverse ⇑φ ⇑ψ) {χ : M →* M} [IsId χ] :
φ.CompTriple ψ χ
source
instance MonoidHom.CompTriple.instRootCompTriple {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} [κ : φ.CompTriple ψ χ] :
_root_.CompTriple ⇑φ ⇑ψ ⇑χ
source
theorem MonoidHom.CompTriple.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [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)

source
theorem MonoidHom.CompTriple.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} (h : φ.CompTriple ψ χ) (x : M) :
ψ (φ x) = χ x
source
theorem MonoidHom.CompTriple.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] {Q : Type u_4} [Monoid Q] {φ₁ : M →* N} {φ₂ : N →* P} {φ₁₂ : M →* P} (κ : φ₁.CompTriple φ₂ φ₁₂) {φ₃ : P →* Q} {φ₂₃ : N →* Q} (κ' : φ₂.CompTriple φ₃ φ₂₃) {φ₁₂₃ : M →* Q} :
φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃