limitCone — Mathlib

English

The limit of F can be realized as a cone with vertex Shrink(F.sections) and projection maps defined via an equivalence with F.sections.

Русский

Предел диаграммы F реализуется как конус с вершиной Shrink(F.sections) и проекциями, заданными через эквивалентность с F.sections.

LaTeX

$$$\\text{limitCone}(F)\\;:\\;\\mathrm{Cone}(F)\\text{ with } \\mathrm{pt}=\\mathrm{Shrink}(F.\\mathrmsections),\\;\\pi_j(u)=((\\mathrm{equivShrink } F.\\mathrmsections).symm\\, u).val_j$$$

Lean4

/-- (internal implementation) the limit cone of a functor,
implemented as flat sections of a pi type
-/
@[simps]
noncomputable def limitCone : Cone F where
  pt := Shrink F.sections
  π :=
    { app := fun j u => ((equivShrink F.sections).symm u).val j
      naturality := fun j j' f => by
        funext x
        simp }

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