cocone — Mathlib

English

Define a canonical cocone on X : Discrete α ⥤ C with apex ∐(X.obj Discrete.mk j) and legs given by the Discrete.natTrans to the Sigma injections.

Русский

Задаётся канонический когон X: Discrete α ⥤ C с вершиной ∐(X.obj Discrete.mk j) и стрелами через Discrete.natTrans к инъекциям Sigma.

LaTeX

$$$\\text{cocone}_X = (\\operatorname{pt} = \\coprod_j X(\\mathrm{Discrete.mk}\u205f j),\\; \\iota_j = \\mathrm{Discrete.natTrans}(\\lambda j, \\Sigma.ι (X. obj (Discrete.mk j)) ))$$$

Lean4

/-- A colimit cocone for `X : Discrete α ⥤ C` that is given
by `∐ (fun j => X.obj (Discrete.mk j))`. -/
@[simps]
def cocone : Cocone X where
  pt := ∐ (fun j => X.obj (Discrete.mk j))
  ι := Discrete.natTrans (fun _ => Sigma.ι (fun j ↦ X.obj ⟨j⟩) _)

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