coneOfSectionCompCoyoneda — Mathlib

English

The cone obtained from a section s of F ⋙ coyoneda.obj X is defined by apex X.unop and legs given by the canonical bijection compCoyonedaSectionsEquiv.

Русский

Конус, полученный из секции s диаграммы через coyoneda.obj X, имеет вершину X.unop и стороны, заданные каноническим биекциям compCoyonedaSectionsEquiv.

LaTeX

$$$\\text{ConeOfSectionCoyoneda}(F,X,s) = \\text{Cone}$ с вершиной $X^{\\mathrm{unop}}$ и ребрами $\\pi$ через $\\text{compCoyonedaSectionsEquiv } F X s$$$

Lean4

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

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