Propositional typeclasses on several maps

This file contains typeclasses that are 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.

• CompTriple φ ψ χ, which expresses that ψ.comp φ = χ
• CompTriple.IsId φ, which expresses that φ = id

TODO :

• align with RingHomCompTriple

class CompTriple {M : Type u_1} {N : Type u_2} {P : Type u_3} (φ : M → N) (ψ : N → P) (χ : outParam (M → P)) : Prop

Class of composing triples

• comp_eq : ψ ∘ φ = χ

  The maps form a commuting triangle

@[simp]

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

The maps form a commuting triangle

class CompTriple.IsId {M : Type u_1} (σ : M → M) : Prop

Class of Id maps

• eq_id : σ = id

theorem CompTriple.IsId.eq_id {M : Type u_1} {σ : M → M} [self : CompTriple.IsId σ] : σ = id

instance CompTriple.instIsIdId {M : Type u_1} : CompTriple.IsId id

Equations

• ⋯ = ⋯

instance CompTriple.instComp_id {N : Type u_1} {P : Type u_2} {φ : N → N} [CompTriple.IsId φ] {ψ : N → P} : CompTriple φ ψ ψ

Equations

• ⋯ = ⋯

instance CompTriple.instId_comp {M : Type u_1} {N : Type u_2} {φ : M → N} {ψ : N → N} [CompTriple.IsId ψ] : CompTriple φ ψ φ

Equations

• ⋯ = ⋯

theorem CompTriple.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : M → N} {ψ : N → P} : CompTriple φ ψ (ψ ∘ φ)

φ, ψ and ψ ∘ φ foraCompTriple`

theorem CompTriple.comp_inv {M : Type u_1} {N : Type u_2} {φ : M → N} {ψ : N → M} (h : Function.RightInverse φ ψ) {χ : M → M} [CompTriple.IsId χ] : CompTriple φ ψ χ

theorem CompTriple.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : M → N} {ψ : N → P} {χ : M → P} (h : CompTriple φ ψ χ) (x : M) : ψ (φ x) = χ x