limitCone — Mathlib

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