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
assertsMonoidHom.CompTriple φ ψ (ψ.comp φ)
MonoidHom.CompTriple.id_comp
assertsMonoidHom.CompTriple φ ψ ψ
in the presence ofMonoidHom.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 ?
theorem
MonoidHom.CompTriple.IsId.eq_id
{M : Type u_2}
:
∀ {inst : Monoid M} {σ : M →* M} [self : MonoidHom.CompTriple.IsId σ], σ = MonoidHom.id M
Equations
- ⋯ = ⋯
instance
MonoidHom.CompTriple.instIsIdOfIsIdCoe
{M : Type u_2}
[Monoid M]
{σ : M →* M}
[h : 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 ψ χ
@[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 φ₃ φ₁₂₃