Lean4
/-- Given a functor `G` from `LightProfinite` and `S : LightProfinite`, we obtain a cone on
`(StructuredArrow.proj S toLightProfinite ⋙ toLightProfinite ⋙ G)` with cone point `G.obj S`.
Whiskering this cone with `LightProfinite.Extend.functor c` gives `G.mapCone c` as we check in the
example below.
-/
def cone (S : LightProfinite) : Cone (StructuredArrow.proj S toLightProfinite ⋙ toLightProfinite ⋙ G)
where
pt := G.obj S
π :=
{ app := fun i ↦ G.map i.hom
naturality := fun _ _ f ↦
(by
have := f.w
simp only [const_obj_obj, StructuredArrow.left_eq_id, const_obj_map, Category.id_comp,
StructuredArrow.w] at this
simp only [const_obj_obj, comp_obj, StructuredArrow.proj_obj, const_obj_map, Category.id_comp,
Functor.comp_map, StructuredArrow.proj_map, ← map_comp, StructuredArrow.w]) }
