coneOfSectionCompYoneda — Mathlib

English

A cocone c is a colimit if and only if for every X in Cᵒᵖ, the cone obtained by mapping c along yoneda.obj X is a limit.

Русский

Кокон является колимитом тогда и только тогда, когда для каждого X в Cᵒᵖ образованный через yoneda.obj X конус является пределом.

LaTeX

$$$\\mathrm{IsColimit}(c) \\;\\Longleftrightarrow\\; \\forall X:\\!C^{op},\\; \\mathrm{IsLimit}((\\mathrm{yoneda.obj} X).mapCone c^{op})$$$

Lean4

/-- The cone of `F` corresponding to an element in `(F ⋙ yoneda.obj X).sections`. -/
@[simps]
def coneOfSectionCompYoneda (F : J ⥤ Cᵒᵖ) (X : C) (s : (F ⋙ yoneda.obj X).sections) : Cone F
    where
  pt := Opposite.op X
  π := compYonedaSectionsEquiv F X s

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