English
For a functor G: LightProfiniteᵒᵖ ⥤ C and S ∈ LightProfinite, define a cocone on the diagram CostructuredArrow.proj toLightProfinite.op ⟨S⟩ ⋙ toLightProfinite.op ⋙ G with apex G.obj ⟨S⟩ and legs given by G.map i.hom, and naturality ensured by functoriality.
Русский
Для функторa G: LightProfiniteᵒᵖ ⥤ C и S ∈ LightProfinite задаётся кокон на диаграмме CostructuredArrow.proj toLightProfinite.op ⟨S⟩ ⋙ toLightProfinite.op ⋙ G с вершиной G.obj ⟨S⟩ и ножками i.hom, натуральность обеспечивается функторной связью.
LaTeX
$$$\operatorname{Cocone}\left( \mathrm{CostructuredArrow.proj\ toLightProfinite.op\; ⟨S⟩} \circ \mathrm{toLightProfinite.op} \circ G \right), \quad \mathrm{pt}=G(⟨S⟩), \quad \iota_i = G(i.\mathrm{hom}).$$$
Lean4
/-- Given a functor `G` from `LightProfiniteᵒᵖ` and `S : LightProfinite`, we obtain a cocone on
`(CostructuredArrow.proj toLightProfinite.op ⟨S⟩ ⋙ toLightProfinite.op ⋙ G)` with cocone point
`G.obj ⟨S⟩`.
Whiskering this cocone with `LightProfinite.Extend.functorOp c` gives `G.mapCocone c.op` as we
check in the example below.
-/
@[simps]
def cocone (S : LightProfinite) : Cocone (CostructuredArrow.proj toLightProfinite.op ⟨S⟩ ⋙ toLightProfinite.op ⋙ G)
where
pt := G.obj ⟨S⟩
ι :=
{ app := fun i ↦ G.map i.hom
naturality := fun _ _ f ↦
(by
have := f.w
simp only [op_obj, const_obj_obj, op_map, CostructuredArrow.right_eq_id, const_obj_map,
Category.comp_id] at this
simp only [comp_obj, CostructuredArrow.proj_obj, op_obj, const_obj_obj, Functor.comp_map,
CostructuredArrow.proj_map, op_map, ← map_comp, this, const_obj_map, Category.comp_id]) }
