Mathlib.Logic.Function.CompTypeclasses

Module docstring

{"# 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

CompTriple structure

{M N P : Type*} (φ : M → N) (ψ : N → P) (χ : outParam (M → P))

Full source

/-- Class of composing triples -/
class CompTriple {M N P : Type*} (φ : M → N) (ψ : N → P) (χ : outParam (M → P)) : Prop where
  /-- The maps form a commuting triangle -/
  comp_eq : ψ.comp φ = χ

Composition Triple of Functions

Informal description

The structure `CompTriple φ ψ χ` represents a composition triple of functions, where `φ : M → N`, `ψ : N → P`, and `χ : M → P`, such that the composition `ψ ∘ φ` equals `χ`. This is used to formalize the notion of equivariant maps in a categorical setting.

CompTriple.IsId structure

{M : Type*} (σ : M → M)

Full source

/-- Class of Id maps -/
class IsId {M : Type*} (σ : M → M) : Prop where
  eq_id : σ = id

Identity Function Class

Informal description

The structure `IsId` is a class that asserts a function `σ : M → M` is equal to the identity function on `M$.

CompTriple.instIsIdId instance

{M : Type*} : IsId (@id M)

Full source

instance {M : Type*} : IsId (@id M) where
  eq_id := rfl

Identity Function Satisfies IsId Property

Informal description

The identity function $\text{id} : M \to M$ satisfies the `IsId` property, meaning it is equal to itself.

CompTriple.instComp_id instance

{N P : Type*} {φ : N → N} [IsId φ] {ψ : N → P} : CompTriple φ ψ ψ

Full source

instance instComp_id {N P : Type*} {φ : N → N} [IsId φ] {ψ : N → P} :
    CompTriple φ ψ ψ where
  comp_eq := by simp only [IsId.eq_id, Function.comp_id]

Composition with Identity Preserves Function

Informal description

For any function $\psi : N \to P$ and any function $\varphi : N \to N$ that is equal to the identity function on $N$, the composition triple $\text{CompTriple}(\varphi, \psi, \psi)$ holds, meaning $\psi \circ \varphi = \psi$.

CompTriple.instId_comp instance

{M N : Type*} {φ : M → N} {ψ : N → N} [IsId ψ] : CompTriple φ ψ φ

Full source

instance instId_comp {M N : Type*} {φ : M → N} {ψ : N → N} [IsId ψ] :
    CompTriple φ ψ φ where
  comp_eq := by simp only [IsId.eq_id, Function.id_comp]

Composition with Identity Preserves the Function

Informal description

For any function $\varphi : M \to N$ and any function $\psi : N \to N$ that is equal to the identity function on $N$, the composition triple $\text{CompTriple}(\varphi, \psi, \varphi)$ holds, meaning $\psi \circ \varphi = \varphi$.

CompTriple.comp theorem

{M N P : Type*} {φ : M → N} {ψ : N → P} : CompTriple φ ψ (ψ.comp φ)

Full source

/-- `φ`, `ψ` and `ψ ∘ φ` for` a `CompTriple` -/
theorem comp {M N P : Type*}
    {φ : M → N} {ψ : N → P} :
    CompTriple φ ψ  (ψ.comp φ) where
  comp_eq := rfl

Composition Triple of $\psi \circ \phi$

Informal description

For any types $M$, $N$, $P$ and functions $\phi: M \to N$, $\psi: N \to P$, the composition triple $\text{CompTriple}(\phi, \psi, \psi \circ \phi)$ holds, meaning that $\psi \circ \phi$ is equal to the composition of $\psi$ and $\phi$.

CompTriple.comp_inv theorem

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

Full source

lemma comp_inv {M N : Type*} {φ : M → N} {ψ : N → M}
    (h : Function.RightInverse φ ψ) {χ : M → M} [IsId χ] :
    CompTriple φ ψ χ where
  comp_eq := by simp only [IsId.eq_id, h.id]

Composition Triple with Right Inverse Yields Identity

Informal description

Let $M$ and $N$ be types, and let $\phi: M \to N$ and $\psi: N \to M$ be functions such that $\phi$ is a right inverse of $\psi$ (i.e., $\phi \circ \psi = \text{id}_N$). If $\chi: M \to M$ is the identity function, then the composition triple $\text{CompTriple}\, \phi\, \psi\, \chi$ holds, meaning $\psi \circ \phi = \chi$.

CompTriple.comp_apply theorem

{M N P : Type*} {φ : M → N} {ψ : N → P} {χ : M → P} (h : CompTriple φ ψ χ) (x : M) : ψ (φ x) = χ x

Full source

lemma comp_apply {M N P : Type*}
    {φ : M → N} {ψ : N → P} {χ : M → P} (h : CompTriple φ ψ χ) (x : M) :
    ψ (φ x) = χ x := by
  rw [← h.comp_eq, Function.comp_apply]

Function Application in Composition Triple

Informal description

For any types $M$, $N$, $P$ and functions $\phi: M \to N$, $\psi: N \to P$, $\chi: M \to P$, if $\text{CompTriple}\, \phi\, \psi\, \chi$ holds (i.e., $\psi \circ \phi = \chi$), then for any $x \in M$, we have $\psi(\phi(x)) = \chi(x)$.