pullbackObjIso_hom_comp_fst — Mathlib

English

For f: F ⟶ H and g: G ⟶ H in a pullback square, (pullbackObjIso f g d).hom ≫ pullback.fst (f.app d) (g.app d) = pullback.fst f g).app d.

Русский

В тождественном квадрате вытянутого предела композиция (pullbackObjIso f g d).hom с первой проекцией равна проекции pullback.fst f g на d-ой компоненте.

LaTeX

$$$(\\text{pullbackObjIso } f\\, g\\, d).\\mathrm{hom} \\; \\circ \\; \\text{pullback.fst} (f.app d) (g.app d) = \\text{pullback.fst} f g).\\mathrm{app} d.$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackObjIso_hom_comp_fst (f : F ⟶ H) (g : G ⟶ H) (d : D) :
    (pullbackObjIso f g d).hom ≫ pullback.fst (f.app d) (g.app d) = (pullback.fst f g).app d := by simp [pullbackObjIso]

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