Lean4
/-- An explicit limit cone for a functor `F : J ⥤ CompHaus`, defined in terms of
`TopCat.limitCone`. -/
def limitCone {J : Type v} [SmallCategory J] (F : J ⥤ CompHaus.{max v u}) : Limits.Cone F :=
letI FF : J ⥤ TopCat := F ⋙ compHausToTop
{ pt :=
{ toTop := (TopCat.limitCone FF).pt
is_compact :=
by
change CompactSpace {u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), (F.map f) (u i) = u j}
rw [← isCompact_iff_compactSpace]
apply IsClosed.isCompact
have :
{u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j} =
⋂ (i : J) (j : J) (f : i ⟶ j), {u | F.map f (u i) = u j} :=
by
ext1
simp only [Set.mem_iInter, Set.mem_setOf_eq]
rw [this]
apply isClosed_iInter
intro i
apply isClosed_iInter
intro j
apply isClosed_iInter
intro f
apply isClosed_eq
· exact ((F.map f).hom.continuous).comp (continuous_apply i)
· exact continuous_apply j
is_hausdorff :=
show T2Space {u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), (F.map f) (u i) = u j} from inferInstance
prop := trivial }
π :=
{ app := fun j => (TopCat.limitCone FF).π.app j
naturality := by
intro _ _ f
ext ⟨x, hx⟩
simp only [Functor.const_obj_map]
exact (hx f).symm } }
