pullbackZeroZeroIso_hom_fst — Mathlib

English

The pullback’s hom composed with the first projection equals the pullback’s first projection.

Русский

Гомоморфизм пуллбэка, сопоставленный с первой проекцией, равен первой проекции.

LaTeX

$$$$ \bigl(\text{pullbackZeroZeroIso } X Y\bigr).\mathrm{hom} \circ \mathrm{prod.fst} = \mathrm{pullback.fst} 0 0. $$$$

Lean4

@[simp]
theorem pullbackZeroZeroIso_hom_fst (X Y : C) [HasBinaryProduct X Y] :
    (pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst 0 0 := by simp [← Iso.eq_inv_comp]

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