limitCone — Mathlib

English

For a diagram F: J → AlgCat(R), the constructed limit cone limitCone F is a genuine limit cone for F in AlgCat(R).

Русский

Для диаграммы F: J → AlgCat(R) конструируемый предел-конус limitCone F действительно является пределом над F в AlgCat(R).

LaTeX

$$$$\text{IsLimit}(\text{limitCone}(F)).$$$$

Lean4

/-- Construction of a limit cone in `AlgCat R`.
(Internal use only; use the limits API.)
-/
def limitCone : Cone F where
  pt := AlgCat.of R (Types.Small.limitCone (F ⋙ forget _)).pt
  π :=
    { app := fun j ↦ ofHom <| limitπAlgHom F j
      naturality := fun _ _ f => by
        ext : 1
        exact AlgHom.coe_fn_injective ((Types.Small.limitCone (F ⋙ forget _)).π.naturality f) }

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