English
A cocone on Profinite extends to a coherent cocone on the extended diagram.
Русский
Коконика на Profinite распространяется на согласованный коконический объект в расширенной диаграмме.
LaTeX
$$$\\mathrm{Extend.cocone}:\\;\\text{Cocone on }(\\mathrm{CostructuredArrow}^{\\mathrm{op}}) \\to C$$$
Lean4
/-- Given a functor `G` from `Profiniteᵒᵖ` and `S : Profinite`, we obtain a cocone on
`(CostructuredArrow.proj toProfinite.op ⟨S⟩ ⋙ toProfinite.op ⋙ G)` with cocone point `G.obj ⟨S⟩`.
Whiskering this cocone with `Profinite.Extend.functorOp c` gives `G.mapCocone c.op` as we check in
the example below.
-/
@[simps]
def cocone (S : Profinite) : Cocone (CostructuredArrow.proj toProfinite.op ⟨S⟩ ⋙ toProfinite.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 [← map_comp, this]) }
