inv_fst — Mathlib

English

The inverse of the diagonal map interacts with fst in a way expressible by a composition involving fst and the diagonal map, reflecting the compatibility of the diagonal with the pullback data.

Русский

Обратное диагонального отображения взаимодействует с fst так, что выражается композицией, включающей fst и диагональную карту, отражая совместимость диагонали с данными предела.

LaTeX

$$$$ (pullbackDiagonalMapIdIso\ f\ g\ i)^{−1} \circ fst = fst \circ f $$$$

Lean4

@[reassoc (attr := simp)]
theorem inv_fst :
    (pullbackDiagonalMapIso f i i₁ i₂).inv ≫ pullback.fst _ _ = pullback.fst _ _ ≫ i₁ ≫ pullback.fst _ _ :=
  by
  delta pullbackDiagonalMapIso
  simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

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