buildIsLimit — Mathlib

English

If t1,t2,i are limit cones for c1,c2,i, respectively, then buildLimit yields a limit cone for F for any i.

Русский

Если t1,t2,i являются пределами конусов для c1,c2,i, соответственно, то buildLimit дает предел конуса для F для любого i.

LaTeX

$$$(t_1,t_2,hi) \Rightarrow IsLimit\,(buildLimit\ s\ t\ hs\ ht\ i)$$$

Lean4

/-- (Implementation) Show the cone constructed in `buildLimit` is limiting, provided the cones used in
its construction are.
-/
def buildIsLimit (t₁ : IsLimit c₁) (t₂ : IsLimit c₂) (hi : IsLimit i) : IsLimit (buildLimit s t hs ht i)
    where
  lift
    q := by
    refine hi.lift (Fork.ofι ?_ ?_)
    · refine t₁.lift (Fan.mk _ fun j => ?_)
      apply q.π.app j
    · apply t₂.hom_ext
      intro ⟨j⟩
      simp [hs, ht]
  uniq q m w := hi.hom_ext (i.equalizer_ext (t₁.hom_ext fun j => by simpa using w j.1))
  fac s j := by simp

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