lift_fst_snd — Mathlib

English

For a pullback of f,g, the lift morphism built from fst and snd is the identity on the pullback.

Русский

Для пулибэка f,g собираемого из fst и snd, отображение лифта является тождественным на пуллбэк.

LaTeX

$$$\mathrm{lift}\ (\mathrm{fst}\ f g)\ (\mathrm{snd}\ f g)\;\mathrm{condition} = \mathrm{id}_{\mathrm{pullback} f g}$$$

Lean4

@[simp]
theorem lift_fst_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
    lift (fst f g) (snd f g) condition = 𝟙 (pullback f g) := by apply hom_ext <;> simp

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