of_is_product — Mathlib

English

Variant: from a limit cone on WalkingCospan, obtain an IsPullback structure.

Русский

Из предельного конуса на WalkingCospan вы получаете структуру IsPullback.

LaTeX

$$IsPullback (c.π.app left) (c.π.app right) (D.map WalkingCospan.Hom.inl) (D.map WalkingCospan.Hom.inr)$$

Lean4

/-- If `c` is a limiting binary product cone, and we have a terminal object,
then we have `IsPullback c.fst c.snd 0 0`
(where each `0` is the unique morphism to the terminal object). -/
theorem of_is_product {c : BinaryFan X Y} (h : Limits.IsLimit c) (t : IsTerminal Z) :
    IsPullback c.fst c.snd (t.from _) (t.from _) :=
  of_isLimit
    (isPullbackOfIsTerminalIsProduct _ _ _ _ t
      (IsLimit.ofIsoLimit h (Limits.Cones.ext (Iso.refl c.pt) (by rintro ⟨⟨⟩⟩ <;> simp))))

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