pullbackP1Iso_hom_fst — Mathlib

English

For each i, the hom component of the isomorphism P1Iso interacts with the first projection as the second coordinate of the pullback, i.e., the hom part composed with the first projection yields the second projection.

Русский

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

LaTeX

$$$$ (pullbackP1Iso \ 𝒰 f g i).hom \; \circ \; \mathrm{fst} = \mathrm{snd} $$$$

Lean4

@[simp, reassoc]
theorem pullbackP1Iso_hom_fst (i : 𝒰.I₀) : (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.fst _ _ = pullback.snd _ _ := by
  simp_rw [pullbackP1Iso, pullback.lift_fst]

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