mapPairComp_hom_app_right — Mathlib

English

The right component of the inverse of mapPairComp on right d is the identity on right (Gᵣ.obj(Fᵣ.obj d)).

Русский

Правая составляющая обратной карты mapPairComp на right d равна тождественному морфизму на right (Gᵣ.obj(Fᵣ.obj d)).

LaTeX

$$$ (\mathrm{mapPairComp} Fₗ Fᵣ Gₗ Gᵣ)^{-1}.\mathrm{app}(\mathrm{right}\; d) = \mathrm{id}_{(\mathrm{right}\; (Gᵣ.obj (Fᵣ.obj d)))} $$$

Lean4

@[simp]
theorem mapPairComp_hom_app_right (d : D) :
    (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (right d) = 𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) :=
  by
  dsimp [mapPairComp]
  simp

Похожие утверждения