isBinaryProductOfIsTerminalIsPullback

English

If a span is obtained as a pullback over a terminal object, then that span is a binary product of its two legs.

Русский

Если две мономорфизмы образуют отношение через граничный объект (терминал), образующий распад-обратную схему (pullback) над терминальным объектом, то этот спан является бинарным произведением двух его сторон.

LaTeX

$$$\\forall F:\\mathrm{DiscreteWalkingPair}\\to C,\\ \\forall c:\\mathrm{Cone}\;F,\\ \\forall X:\\,C\\,\\Big(\\mathrm{IsTerminal}\\,X\\Big)\\;\\Big( f:\\,F(\\mathrm{left})\\to X,\\ g:\\,F(\\mathrm{right})\\to X \\Big)\\;\\Big( \\mathrm{IsLimit}\\big(\\mathrm{PullbackCone.mk}(c.\\pi.\\mathrm{left})(c.\\pi.\\mathrm{right})\\;|\\;hX.hom_ext(\\_\\to f)(\\_\\to g)\\big)\\;\\Rightarrow\\; \\mathrm{IsLimit}\\,c \\Big).$$

Lean4

/-- If a span is the pullback span over the terminal object, then it is a binary product. -/
def isBinaryProductOfIsTerminalIsPullback (F : Discrete WalkingPair ⥤ C) (c : Cone F) {X : C} (hX : IsTerminal X)
    (f : F.obj ⟨WalkingPair.left⟩ ⟶ X) (g : F.obj ⟨WalkingPair.right⟩ ⟶ X)
    (hc :
      IsLimit
        (PullbackCone.mk (c.π.app ⟨WalkingPair.left⟩) (c.π.app ⟨WalkingPair.right⟩ :) <| hX.hom_ext (_ ≫ f) (_ ≫ g))) :
    IsLimit c
    where
  lift s := hc.lift (PullbackCone.mk (s.π.app ⟨WalkingPair.left⟩) (s.π.app ⟨WalkingPair.right⟩) (hX.hom_ext _ _))
  fac _
    j := Discrete.casesOn j fun j => WalkingPair.casesOn j (hc.fac _ WalkingCospan.left) (hc.fac _ WalkingCospan.right)
  uniq s m
    J :=
    by
    let c' :=
      PullbackCone.mk (m ≫ c.π.app ⟨WalkingPair.left⟩) (m ≫ c.π.app ⟨WalkingPair.right⟩ :) (hX.hom_ext (_ ≫ f) (_ ≫ g))
    dsimp; rw [← J, ← J]
    apply hc.hom_ext
    rintro (_ | (_ | _)) <;> simp only [PullbackCone.mk_π_app]
    exacts [(Category.assoc _ _ _).symm.trans (hc.fac_assoc c' WalkingCospan.left f).symm,
      (hc.fac c' WalkingCospan.left).symm, (hc.fac c' WalkingCospan.right).symm]

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