isLimitFan — Mathlib

English

There is a well-defined lifting operation that takes a compatible family of morphisms from T' to each T_j and produces a morphism from T' to the product-triangle.

Русский

Существует корректная операция подъема, которая принимает совместимую семью морфизмов и порождает морфизм из T' в произведение треугольников.

LaTeX

$$lift_T' φ : T' ⟶ productTriangle T$$

Lean4

/-- The triangle `productTriangle T` satisfies the universal property of the categorical
product of the triangles `T`. -/
def isLimitFan : IsLimit (productTriangle.fan T) :=
  mkFanLimit _ (fun s => productTriangle.lift T s.proj) (fun s j => by cat_disch)
    (by
      intro s m hm
      ext1
      all_goals exact Pi.hom_ext _ _ (fun j => (by simp [← hm])))

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