rightUnitor_inv_left_fst — Mathlib

English

The inverse of the right unitor composed with fst recovers the left projection to the base object.

Русский

Обратный правый унитор в сочетании с fst восстанавливает левую проекцию базового объекта.

LaTeX

$$$ (\\rho_Y)^{\\mathrm{inv}}_{\\mathrm{left}} \\circ \\mathrm{fst}(Y.hom, \\mathrm{id}_X) = \\mathrm{id}_{Y.left} $$$

Lean4

@[reassoc (attr := simp)]
theorem rightUnitor_inv_left_fst (Y : Over X) : (ρ_ Y).inv.left ≫ pullback.fst _ (𝟙 X) = 𝟙 _ :=
  limit.lift_π _ _

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