limitCone — Mathlib

Lean4
/-- The explicit limit cone in `ProfiniteGrp`. -/
abbrev limitCone : Limits.Cone F
    where
  pt := ofProfinite (Profinite.limitCone (F ⋙ (forget₂ ProfiniteGrp Profinite))).pt
  π :=
    { app := fun j =>
        ⟨{  toFun := fun x => x.1 j
            map_one' := rfl
            map_mul' := fun x y => rfl
            continuous_toFun := by exact (continuous_apply j).comp (continuous_iff_le_induced.mpr fun U a => a) }⟩
      naturality := fun i j f =>
        by
        simp only [Functor.const_obj_obj, Functor.comp_obj, Functor.const_obj_map, Category.id_comp, Functor.comp_map]
        congr
        exact funext fun x => (x.2 f).symm }
Похожие утверждения