limitCone — Mathlib

Lean4
/-- An explicit limit cone for a functor `F : J ⥤ Profinite`, defined in terms of
`CompHaus.limitCone`, which is defined in terms of `TopCat.limitCone`. -/
def limitCone {J : Type v} [SmallCategory J] (F : J ⥤ Profinite.{max u v}) : Limits.Cone F
    where
  pt :=
    { toTop := (CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).pt.toTop
      prop := by
        change TotallyDisconnectedSpace ({u : ∀ j : J, F.obj j | _} : Type _)
        exact Subtype.totallyDisconnectedSpace }
  π :=
    { app := (CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app
      naturality := by
        intro j k f
        ext ⟨g, p⟩
        exact (p f).symm }
Похожие утверждения