feat: port Topology.Category.Top.Limits.Basic (#3487)

Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>

Mathlib.lean

@@ -1905,6 +1905,7 @@ import Mathlib.Topology.Category.Born
 import Mathlib.Topology.Category.Top.Adjunctions
 import Mathlib.Topology.Category.Top.Basic
 import Mathlib.Topology.Category.Top.EpiMono
+import Mathlib.Topology.Category.Top.Limits.Basic
 import Mathlib.Topology.Category.Top.Opens
 import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Connected

Mathlib/Topology/Category/Top/Basic.lean

@@ -81,11 +81,11 @@ def of (X : Type u) [TopologicalSpace X] : TopCat :=
 set_option linter.uppercaseLean3 false in
 #align Top.of TopCat.of
 
-instance (X : TopCat) : TopologicalSpace X :=
+instance topologicalSpace_coe (X : TopCat) : TopologicalSpace X :=
   X.str
 
 -- Porting note: cannot see through forget
-instance (X : TopCat) : TopologicalSpace <| (forget TopCat).obj X := by
+instance topologicalSpace_forget (X : TopCat) : TopologicalSpace <| (forget TopCat).obj X := by
   change TopologicalSpace X
   infer_instance
 
@@ -94,7 +94,7 @@ theorem coe_of (X : Type u) [TopologicalSpace X] : (of X : Type u) = X := rfl
 set_option linter.uppercaseLean3 false in
 #align Top.coe_of TopCat.coe_of
 
-instance : Inhabited TopCat :=
+instance inhabited : Inhabited TopCat :=
   ⟨TopCat.of Empty⟩
 
 -- porting note: added to ease the port of `AlgebraicTopology.TopologicalSimplex`

Mathlib/Topology/Category/Top/Limits/Basic.lean

@@ -0,0 +1,221 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot, Scott Morrison, Mario Carneiro, Andrew Yang
+
+! This file was ported from Lean 3 source module topology.category.Top.limits.basic
+! leanprover-community/mathlib commit 8195826f5c428fc283510bc67303dd4472d78498
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Category.Top.Basic
+import Mathlib.CategoryTheory.Limits.ConcreteCategory
+
+/-!
+# The category of topological spaces has all limits and colimits
+
+Further, these limits and colimits are preserved by the forgetful functor --- that is, the
+underlying types are just the limits in the category of types.
+-/
+
+-- Porting note: every ML3 decl has an uppercase letter
+set_option linter.uppercaseLean3 false
+
+open TopologicalSpace
+
+open CategoryTheory
+
+open CategoryTheory.Limits
+
+open Opposite
+
+/--
+Universe inequalities in Mathlib 3 are expressed through use of `max u v`. Unfortunately,
+this leads to unbound universes which cannot be solved for during unification, eg
+`max u v =?= max v ?`.
+The current solution is to wrap `Type max u v` in `TypeMax.{u,v}`
+to expose both universe parameters directly.
+
+Similarly, for other concrete categories for which we need to refer to the maximum of two universes
+(e.g. any category for which we are constructing limits), we need an analogous abbreviation.
+-/
+@[nolint checkUnivs]
+abbrev TopCatMax.{u, v} := TopCat.{max u v}
+
+universe v u w
+
+noncomputable section
+
+namespace TopCat
+
+variable {J : Type v} [SmallCategory J]
+
+local notation "forget" => forget TopCat
+
+/-- A choice of limit cone for a functor `F : J ⥤ TopCat`.
+Generally you should just use `limit.cone F`, unless you need the actual definition
+(which is in terms of `Types.limitCone`).
+-/
+def limitCone (F : J ⥤ TopCatMax.{v, u}) : Cone F where
+  pt := TopCat.of { u : ∀ j : J, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j }
+  π :=
+    { app := fun j =>
+        { toFun := fun u => u.val j
+          -- Porting note: `continuity` from the original mathlib3 proof failed here.
+          continuous_toFun := Continuous.comp (continuous_apply _) (continuous_subtype_val) }
+      naturality := fun X Y f => by
+        -- Automation fails in various ways in this proof. Why?!
+        dsimp
+        rw [Category.id_comp]
+        apply ContinuousMap.ext
+        intro a
+        exact (a.2 f).symm }
+#align Top.limit_cone TopCat.limitCone
+
+/-- A choice of limit cone for a functor `F : J ⥤ TopCat` whose topology is defined as an
+infimum of topologies infimum.
+Generally you should just use `limit.cone F`, unless you need the actual definition
+(which is in terms of `Types.limitCone`).
+-/
+def limitConeInfi (F : J ⥤ TopCatMax.{v, u}) : Cone F where
+  pt :=
+    ⟨(Types.limitCone.{v,u} (F ⋙ forget)).pt,
+      ⨅ j, (F.obj j).str.induced ((Types.limitCone.{v,u} (F ⋙ forget)).π.app j)⟩
+  π :=
+    { app := fun j =>
+        ⟨(Types.limitCone.{v,u} (F ⋙ forget)).π.app j, continuous_iff_le_induced.mpr (infᵢ_le _ _)⟩
+      naturality := fun _ _ f =>
+        ContinuousMap.coe_injective ((Types.limitCone.{v,u} (F ⋙ forget)).π.naturality f) }
+#align Top.limit_cone_infi TopCat.limitConeInfi
+
+/-- The chosen cone `TopCat.limitCone F` for a functor `F : J ⥤ TopCat` is a limit cone.
+Generally you should just use `limit.isLimit F`, unless you need the actual definition
+(which is in terms of `Types.limitConeIsLimit`).
+-/
+def limitConeIsLimit (F : J ⥤ TopCatMax.{v, u}) : IsLimit (limitCone.{v,u} F) where
+  lift S :=
+    { toFun := fun x =>
+        ⟨fun j => S.π.app _ x, fun f => by
+          dsimp
+          erw [← S.w f]
+          rfl⟩
+      continuous_toFun :=
+        Continuous.subtype_mk (continuous_pi <| fun j => (S.π.app j).2) fun x i j f => by
+          dsimp
+          rw [← S.w f]
+          rfl }
+  uniq S m h := by
+    apply ContinuousMap.ext ; intros a ; apply Subtype.ext ; funext j
+    dsimp
+    rw [← h]
+    rfl
+#align Top.limit_cone_is_limit TopCat.limitConeIsLimit
+
+/-- The chosen cone `TopCat.limitConeInfi F` for a functor `F : J ⥤ TopCat` is a limit cone.
+Generally you should just use `limit.isLimit F`, unless you need the actual definition
+(which is in terms of `Types.limitConeIsLimit`).
+-/
+def limitConeInfiIsLimit (F : J ⥤ TopCatMax.{v, u}) : IsLimit (limitConeInfi.{v,u} F) := by
+  refine IsLimit.ofFaithful forget (Types.limitConeIsLimit.{v,u} (F ⋙ forget))
+    -- Porting note: previously could infer all ?_ except continuity
+    (fun s => ⟨fun v => ⟨ fun j => (Functor.mapCone forget s).π.app j v, ?_⟩, ?_⟩) fun s => ?_
+  · dsimp [Functor.sections]
+    intro _ _ _
+    rw [←comp_apply, ←s.π.naturality]
+    dsimp
+    rw [Category.id_comp]
+  · exact
+    continuous_iff_coinduced_le.mpr
+      (le_infᵢ fun j =>
+        coinduced_le_iff_le_induced.mp <|
+          (continuous_iff_coinduced_le.mp (s.π.app j).continuous : _))
+  · rfl
+#align Top.limit_cone_infi_is_limit TopCat.limitConeInfiIsLimit
+
+instance topCat_hasLimitsOfSize : HasLimitsOfSize.{v} TopCatMax.{v, u}
+    where has_limits_of_shape _ :=
+    { has_limit := fun F =>
+        HasLimit.mk
+          { cone := limitCone.{v,u} F
+            isLimit := limitConeIsLimit F } }
+#align Top.Top_has_limits_of_size TopCat.topCat_hasLimitsOfSize
+
+instance topCat_hasLimits : HasLimits TopCat.{u} :=
+  TopCat.topCat_hasLimitsOfSize.{u, u}
+#align Top.Top_has_limits TopCat.topCat_hasLimits
+
+instance forgetPreservesLimitsOfSize :
+    PreservesLimitsOfSize.{v, v} forget where
+  preservesLimitsOfShape {_} :=
+    { preservesLimit := fun {F} =>
+        preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v,v} F)
+          (Types.limitConeIsLimit.{v,v} (F ⋙ forget)) }
+#align Top.forget_preserves_limits_of_size TopCat.forgetPreservesLimitsOfSize
+
+instance forgetPreservesLimits : PreservesLimits forget :=
+  TopCat.forgetPreservesLimitsOfSize.{u}
+#align Top.forget_preserves_limits TopCat.forgetPreservesLimits
+
+/-- A choice of colimit cocone for a functor `F : J ⥤ TopCat`.
+Generally you should just use `colimit.cocone F`, unless you need the actual definition
+(which is in terms of `Types.colimitCocone`).
+-/
+def colimitCocone (F : J ⥤ TopCatMax.{v, u}) : Cocone F where
+  pt :=
+    ⟨(Types.colimitCocone.{v,u} (F ⋙ forget)).pt,
+      ⨆ j, (F.obj j).str.coinduced ((Types.colimitCocone (F ⋙ forget)).ι.app j)⟩
+  ι :=
+    { app := fun j =>
+        ⟨(Types.colimitCocone (F ⋙ forget)).ι.app j, continuous_iff_coinduced_le.mpr <|
+          -- Porting note: didn't need function before
+          le_supᵢ (fun j => coinduced ((Types.colimitCocone (F ⋙ forget)).ι.app j) (F.obj j).str) j⟩
+      naturality := fun _ _ f =>
+        ContinuousMap.coe_injective ((Types.colimitCocone (F ⋙ forget)).ι.naturality f) }
+#align Top.colimit_cocone TopCat.colimitCocone
+
+/-- The chosen cocone `TopCat.colimitCocone F` for a functor `F : J ⥤ TopCat` is a colimit cocone.
+Generally you should just use `colimit.isColimit F`, unless you need the actual definition
+(which is in terms of `Types.colimitCoconeIsColimit`).
+-/
+def colimitCoconeIsColimit (F : J ⥤ TopCatMax.{v, u}) : IsColimit (colimitCocone F) := by
+  refine
+    IsColimit.ofFaithful forget (Types.colimitCoconeIsColimit _) (fun s =>
+    -- Porting note: it appears notation for forget breaks dot notation (also above)
+    -- Porting note: previously function was inferred
+      ⟨Quot.lift (fun p => (Functor.mapCocone forget s).ι.app p.fst p.snd) ?_, ?_⟩) fun s => ?_
+  · intro _ _ ⟨_,h⟩
+    dsimp
+    rw [h, Functor.comp_map, ← comp_apply, s.ι.naturality]
+    dsimp
+    rw [Category.comp_id]
+  · exact
+    continuous_iff_le_induced.mpr
+      (supᵢ_le fun j =>
+        coinduced_le_iff_le_induced.mp <|
+          (continuous_iff_coinduced_le.mp (s.ι.app j).continuous : _))
+  · rfl
+#align Top.colimit_cocone_is_colimit TopCat.colimitCoconeIsColimit
+
+instance topCat_hasColimitsOfSize : HasColimitsOfSize.{v,v} TopCatMax.{v, u} where
+  has_colimits_of_shape _ :=
+    { has_colimit := fun F =>
+        HasColimit.mk
+          { cocone := colimitCocone F
+            isColimit := colimitCoconeIsColimit F } }
+#align Top.Top_has_colimits_of_size TopCat.topCat_hasColimitsOfSize
+
+instance topCat_hasColimits : HasColimits TopCat.{u} :=
+  TopCat.topCat_hasColimitsOfSize.{u, u}
+#align Top.Top_has_colimits TopCat.topCat_hasColimits
+
+instance forgetPreservesColimitsOfSize :
+    PreservesColimitsOfSize.{v, v} forget where
+  preservesColimitsOfShape :=
+    { preservesColimit := fun {F} =>
+        preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit F)
+          (Types.colimitCoconeIsColimit (F ⋙ forget)) }
+#align Top.forget_preserves_colimits_of_size TopCat.forgetPreservesColimitsOfSize
+
+instance forgetPreservesColimits : PreservesColimits (forget : TopCat.{u} ⥤ Type u) :=
+  TopCat.forgetPreservesColimitsOfSize.{u, u}
+#align Top.forget_preserves_colimits TopCat.forgetPreservesColimits