[Merged by Bors] - chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit

Mathlib/Topology/Category/Profinite/AsLimit.lean

@@ -64,12 +64,12 @@ def asLimitCone : CategoryTheory.Limits.Cone X.diagram :=
 set_option linter.uppercaseLean3 false in
 #align Profinite.as_limit_cone Profinite.asLimitCone
 
-instance isIso_asLimitCone_lift : IsIso ((limitConeIsLimit X.diagram).lift X.asLimitCone) :=
+instance isIso_asLimitCone_lift : IsIso ((limitConeIsLimit.{u, u} X.diagram).lift X.asLimitCone) :=
   isIso_of_bijective _
     (by
       refine' ⟨fun a b h => _, fun a => _⟩
       · refine' DiscreteQuotient.eq_of_forall_proj_eq fun S => _
-        apply_fun fun f : (limitCone X.diagram).pt => f.val S at h
+        apply_fun fun f : (limitCone.{u, u} X.diagram).pt => f.val S at h
         exact h
       · obtain ⟨b, hb⟩ :=
           DiscreteQuotient.exists_of_compat (fun S => a.val S) fun _ _ h => a.prop (homOfLE h)
@@ -87,15 +87,15 @@ set_option linter.uppercaseLean3 false in
 /-- The isomorphism between `X` and the explicit limit of `X.diagram`,
 induced by lifting `X.asLimitCone`.
 -/
-def isoAsLimitConeLift : X ≅ (limitCone X.diagram).pt :=
-  asIso <| (limitConeIsLimit _).lift X.asLimitCone
+def isoAsLimitConeLift : X ≅ (limitCone.{u, u} X.diagram).pt :=
+  asIso <| (limitConeIsLimit.{u, u} _).lift X.asLimitCone
 set_option linter.uppercaseLean3 false in
 #align Profinite.iso_as_limit_cone_lift Profinite.isoAsLimitConeLift
 
 /-- The isomorphism of cones `X.asLimitCone` and `Profinite.limitCone X.diagram`.
 The underlying isomorphism is defeq to `X.isoAsLimitConeLift`.
 -/
-def asLimitConeIso : X.asLimitCone ≅ limitCone _ :=
+def asLimitConeIso : X.asLimitCone ≅ limitCone.{u, u} _ :=
   Limits.Cones.ext (isoAsLimitConeLift _) fun _ => rfl
 set_option linter.uppercaseLean3 false in
 #align Profinite.as_limit_cone_iso Profinite.asLimitConeIso

Mathlib/Topology/Category/Profinite/Basic.lean

@@ -27,9 +27,7 @@ compact, Hausdorff and totally disconnected.
 
 ## TODO
 
-0. Link to category of projective limits of finite discrete sets.
-1. finite coproducts
-2. Clausen/Scholze topology on the category `Profinite`.
+* Define procategories and prove that `Profinite` is equiavalent to `Pro (FintypeCat)`.
 
 ## Tags
 
@@ -39,7 +37,7 @@ profinite
 
 set_option linter.uppercaseLean3 false
 
-universe u
+universe v u
 
 open CategoryTheory
 
@@ -242,20 +240,31 @@ end DiscreteTopology
 
 end Profinite
 
+/--
+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 ProfiniteMax.{w, w'} := Profinite.{max w w'}
+
 namespace Profinite
 
--- TODO the following construction of limits could be generalised
--- to allow diagrams in lower universes.
 /-- 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 u} [SmallCategory J] (F : J ⥤ Profinite.{u}) : Limits.Cone F where
+def limitCone {J : Type v} [SmallCategory J] (F : J ⥤ ProfiniteMax.{v, u}) : Limits.Cone F where
   pt :=
-    { toCompHaus := (CompHaus.limitCone.{u, u} (F ⋙ profiniteToCompHaus)).pt
+    { toCompHaus := (CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).pt
       isTotallyDisconnected := by
         change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _)
         exact Subtype.totallyDisconnectedSpace }
   π :=
-  { app := (CompHaus.limitCone.{u, u} (F ⋙ profiniteToCompHaus)).π.app
+  { app := (CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app
     -- Porting note: was `by tidy`:
     naturality := by
       intro j k f
@@ -264,12 +273,12 @@ def limitCone {J : Type u} [SmallCategory J] (F : J ⥤ Profinite.{u}) : Limits.
 #align Profinite.limit_cone Profinite.limitCone
 
 /-- The limit cone `Profinite.limitCone F` is indeed a limit cone. -/
-def limitConeIsLimit {J : Type u} [SmallCategory J] (F : J ⥤ Profinite.{u}) :
+def limitConeIsLimit {J : Type v} [SmallCategory J] (F : J ⥤ ProfiniteMax.{v, u}) :
     Limits.IsLimit (limitCone F) where
   lift S :=
-    (CompHaus.limitConeIsLimit.{u, u} (F ⋙ profiniteToCompHaus)).lift
+    (CompHaus.limitConeIsLimit.{v, u} (F ⋙ profiniteToCompHaus)).lift
       (profiniteToCompHaus.mapCone S)
-  uniq S m h := (CompHaus.limitConeIsLimit.{u, u} _).uniq (profiniteToCompHaus.mapCone S) _ h
+  uniq S m h := (CompHaus.limitConeIsLimit.{v, u} _).uniq (profiniteToCompHaus.mapCone S) _ h
 #align Profinite.limit_cone_is_limit Profinite.limitConeIsLimit
 
 /-- The adjunction between CompHaus.to_Profinite and Profinite.to_CompHaus -/

Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

@@ -24,7 +24,6 @@ This file contains some theorems about cofiltered limits of profinite sets.
   of profinite sets factors through one of the components.
 -/
 
-
 namespace Profinite
 
 open scoped Classical
@@ -33,9 +32,14 @@ open CategoryTheory
 
 open CategoryTheory.Limits
 
-universe u
+universe u v
+
+variable {J : Type v} [SmallCategory J] [IsCofiltered J] {F : J ⥤ ProfiniteMax.{u, v}} (C : Cone F)
 
-variable {J : Type u} [SmallCategory J] [IsCofiltered J] {F : J ⥤ Profinite.{u}} (C : Cone F)
+noncomputable
+instance preserves_smaller_limits_toTopCat :
+    PreservesLimitsOfSize.{v, v} (toTopCat : ProfiniteMax.{v, u} ⥤ TopCatMax.{v, u}) :=
+  Limits.preservesLimitsOfSizeShrink.{v, max u v, v, max u v} _
 
 -- include hC
 -- Porting note: I just add `(hC : IsLimit C)` explicitly as a hypothesis to all the theorems
@@ -45,9 +49,10 @@ a clopen set in one of the terms in the limit.
 -/
 theorem exists_clopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) :
     ∃ (j : J) (V : Set (F.obj j)) (_ : IsClopen V), U = C.π.app j ⁻¹' V := by
+  have := preserves_smaller_limits_toTopCat.{u, v}
   -- First, we have the topological basis of the cofiltered limit obtained by pulling back
   -- clopen sets from the factors in the limit. By continuity, all such sets are again clopen.
-  have hB := TopCat.isTopologicalBasis_cofiltered_limit.{u, u} (F ⋙ Profinite.toTopCat)
+  have hB := TopCat.isTopologicalBasis_cofiltered_limit.{u, v} (F ⋙ Profinite.toTopCat)
       (Profinite.toTopCat.mapCone C) (isLimitOfPreserves _ hC) (fun j => {W | IsClopen W}) ?_
       (fun i => isClopen_univ) (fun i U1 U2 hU1 hU2 => hU1.inter hU2) ?_
   rotate_left
@@ -214,6 +219,7 @@ set_option linter.uppercaseLean3 false in
 one of the components. -/
 theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstant C.pt α) :
     ∃ (j : J) (g : LocallyConstant (F.obj j) α), f = g.comap (C.π.app _) := by
+  have := preserves_smaller_limits_toTopCat.{u, v}
   let S := f.discreteQuotient
   let ff : S → α := f.lift
   cases isEmpty_or_nonempty S
@@ -238,7 +244,7 @@ theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstan
     suffices : Nonempty C.pt; exact IsEmpty.false (S.proj this.some)
     let D := Profinite.toTopCat.mapCone C
     have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC
-    have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{u, u} _)).inv
+    have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{v, max u v} _)).inv
     exact cond.map CD
   · let f' : LocallyConstant C.pt S := ⟨S.proj, S.proj_isLocallyConstant⟩
     obtain ⟨j, g', hj⟩ := exists_locallyConstant_finite_nonempty _ hC f'

Mathlib/Topology/Category/Profinite/Nobeling.lean

@@ -677,8 +677,8 @@ theorem fin_comap_jointlySurjective
     (hC : IsClosed C)
     (f : LocallyConstant C ℤ) : ∃ (s : Finset I)
     (g : LocallyConstant (π C (· ∈ s)) ℤ), f = g.comap (ProjRestrict C (· ∈ s)) := by
-  obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant (Finset I)ᵒᵖ _ _ _
-    (spanCone hC.isCompact) _
+  obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant.{0, u, u} (Finset I)ᵒᵖ _ _ _
+    (spanCone hC.isCompact) ℤ
     (spanCone_isLimit hC.isCompact) f
   exact ⟨(Opposite.unop J), g, h⟩
 

Mathlib/Topology/Category/Profinite/Product.lean

@@ -94,13 +94,13 @@ def indexCone : Cone (indexFunctor hC) where
   π := { app := fun J ↦ π_app C (· ∈ unop J) }
 
 instance isIso_indexCone_lift :
-    IsIso ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC)) :=
+    IsIso ((limitConeIsLimit.{u, u} (indexFunctor hC)).lift (indexCone hC)) :=
   haveI : CompactSpace C := by rwa [← isCompact_iff_compactSpace]
   isIso_of_bijective _
     (by
       refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩
       · refine eq_of_forall_π_app_eq a b (fun J ↦ ?_)
-        apply_fun fun f : (limitCone (indexFunctor hC)).pt => f.val (op J) at h
+        apply_fun fun f : (limitCone.{u, u} (indexFunctor hC)).pt => f.val (op J) at h
         exact h
       · suffices : ∃ (x : C), ∀ (J : Finset ι), π_app C (· ∈ J) x = a.val (op J)
         · obtain ⟨b, hb⟩ := this
@@ -133,12 +133,12 @@ instance isIso_indexCone_lift :
 noncomputable
 def isoindexConeLift :
     @Profinite.of C _ (by rwa [← isCompact_iff_compactSpace]) _ _ ≅
-    (Profinite.limitCone (indexFunctor hC)).pt :=
-  asIso <| (Profinite.limitConeIsLimit _).lift (indexCone hC)
+    (Profinite.limitCone.{u, u} (indexFunctor hC)).pt :=
+  asIso <| (Profinite.limitConeIsLimit.{u, u} _).lift (indexCone hC)
 
 /-- The isomorphism of cones induced by `isoindexConeLift`. -/
 noncomputable
-def asLimitindexConeIso : indexCone hC ≅ Profinite.limitCone _ :=
+def asLimitindexConeIso : indexCone hC ≅ Profinite.limitCone.{u, u} _ :=
   Limits.Cones.ext (isoindexConeLift hC) fun _ => rfl
 
 /-- `indexCone` is a limit cone. -/