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
    @[simp]
    theorem CompTriple.comp_eq {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : MN} {ψ : NP} {χ : outParam (MP)} [self : CompTriple φ ψ χ] :
    ψ φ = χ

    The maps form a commuting triangle

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

    Class of Id maps

    • eq_id : σ = id
    Instances
      theorem CompTriple.IsId.eq_id {M : Type u_1} {σ : MM} [self : CompTriple.IsId σ] :
      σ = id
      Equations
      • =
      instance CompTriple.instComp_id {N : Type u_1} {P : Type u_2} {φ : NN} [CompTriple.IsId φ] {ψ : NP} :
      CompTriple φ ψ ψ
      Equations
      • =
      instance CompTriple.instId_comp {M : Type u_1} {N : Type u_2} {φ : MN} {ψ : NN} [CompTriple.IsId ψ] :
      CompTriple φ ψ φ
      Equations
      • =
      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} [CompTriple.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