Documentation

Mathlib.Logic.Function.CompTypeclasses

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.

TODO :

class CompTriple {M : Type u_1} {N : Type u_2} {P : Type u_3} (φ : MN) (ψ : NP) (χ : outParam (MP)) :

Class of composing triples

  • comp_eq : ψ φ = χ

    The maps form a commuting triangle

Instances
class CompTriple.IsId {M : Type u_1} (σ : MM) :

Class of Id maps

  • eq_id : σ = id
Instances
instance CompTriple.instComp_id {N : Type u_1} {P : Type u_2} {φ : NN} [IsId φ] {ψ : NP} :
CompTriple φ ψ ψ
instance CompTriple.instId_comp {M : Type u_1} {N : Type u_2} {φ : MN} {ψ : NN} [IsId ψ] :
CompTriple φ ψ φ
theorem CompTriple.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : MN} {ψ : NP} :
CompTriple φ ψ (ψ φ)

φ, ψ and ψ ∘ φ foraCompTriple`

theorem CompTriple.comp_inv {M : Type u_1} {N : Type u_2} {φ : MN} {ψ : NM} (h : Function.RightInverse φ ψ) {χ : MM} [IsId χ] :
CompTriple φ ψ χ
theorem CompTriple.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : MN} {ψ : NP} {χ : MP} (h : CompTriple φ ψ χ) (x : M) :
ψ (φ x) = χ x