prodIsoPullback_hom_snd — Mathlib

English

The pullback-to-product isomorphism also identifies the second projection with prod.snd.

Русский

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

LaTeX

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

Lean4

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

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