prodIsoPullback_hom_fst — Mathlib

English

The pullback-to-product isomorphism respects the first projection: the hom part composed with pullback.fst equals prod.fst.

Русский

Изоморфизм между пуллбэком и произведением согласуется с первой проекцией: композиция с prodIsoPullback.hom и pullback.fst равна prod.fst.

LaTeX

$$$(\\,prodIsoPullback X Y\\,).hom \\;\\gg\\; pullback.fst = prod.fst$$$

Lean4

@[reassoc (attr := simp)]
theorem prodIsoPullback_hom_fst [HasTerminal C] [HasPullbacks C] (X Y : C) [HasBinaryProduct X Y] :
    (prodIsoPullback X Y).hom ≫ pullback.fst _ _ = prod.fst :=
  limit.isoLimitCone_hom_π (limitConeOfTerminalAndPullbacks _) ⟨.left⟩

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