of_isLimit_binaryFan_of_isTerminal

English

From a limit of a binary fan and a terminal object, a pullback can be constructed with canonical legs.

Русский

Из предела бинарного фанона и терминального объекта конструируется пуллбак с каноническими ножками.

LaTeX

$$$ IsLimit c \\Rightarrow IsTerminal T \\Rightarrow IsPullback c.fst c.snd (T.from _) (T.from _) $$$

Lean4

theorem of_isLimit_binaryFan_of_isTerminal {X Y : C} {c : BinaryFan X Y} (hc : IsLimit c) {T : C} (hT : IsTerminal T) :
    IsPullback c.fst c.snd (hT.from _) (hT.from _) where
  isLimit' :=
    ⟨PullbackCone.IsLimit.mk _ (fun s ↦ hc.lift (BinaryFan.mk s.fst s.snd))
        (fun s ↦ hc.fac (BinaryFan.mk s.fst s.snd) ⟨.left⟩) (fun s ↦ hc.fac (BinaryFan.mk s.fst s.snd) ⟨.right⟩)
        (fun s m h₁ h₂ ↦ by
          apply BinaryFan.IsLimit.hom_ext hc
          · rw [h₁, hc.fac (BinaryFan.mk s.fst s.snd) ⟨.left⟩]
            rfl
          · rw [h₂, hc.fac (BinaryFan.mk s.fst s.snd) ⟨.right⟩]
            rfl)⟩

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