From 41a8b73ab845a3a8b3b80aa4e04d85c897a55b43 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Fri, 24 Nov 2023 14:23:37 +0000 Subject: [PATCH 1/7] chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit --- .../Category/Profinite/CofilteredLimit.lean | 28 ++++++++++++++++--- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean index 63035ff10b9bd..d012969773445 100644 --- a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean +++ b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean @@ -33,9 +33,27 @@ open CategoryTheory open CategoryTheory.Limits -universe u +/-- +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. -variable {J : Type u} [SmallCategory J] [IsCofiltered J] {F : J ⥤ Profinite.{u}} (C : Cone F) +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.{u, v} := Profinite.{max u v} + +universe u v + +variable {J : Type v} [SmallCategory J] [IsCofiltered J] {F : J ⥤ ProfiniteMax.{u, v}} (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 +63,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 +233,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 +258,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' From 3887289dc158379b039e90056d8461351b3df99c Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Fri, 24 Nov 2023 15:46:24 +0000 Subject: [PATCH 2/7] fix errors in Noebeling --- Mathlib/Topology/Category/Profinite/Nobeling.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index acc37c3ac0177..a075acbf3e40c 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/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⟩ From 156506ff0fdfb2816c2d29370ca7e9b70dec7e12 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Sun, 26 Nov 2023 00:21:23 +0000 Subject: [PATCH 3/7] resolve TODO --- .../Topology/Category/Profinite/AsLimit.lean | 10 +++--- .../Topology/Category/Profinite/Basic.lean | 33 ++++++++++++------- .../Category/Profinite/CofilteredLimit.lean | 14 -------- .../Topology/Category/Profinite/Product.lean | 10 +++--- 4 files changed, 31 insertions(+), 36 deletions(-) diff --git a/Mathlib/Topology/Category/Profinite/AsLimit.lean b/Mathlib/Topology/Category/Profinite/AsLimit.lean index 82df2d7476d43..c806893d68d39 100644 --- a/Mathlib/Topology/Category/Profinite/AsLimit.lean +++ b/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 diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean index c45526e5e2799..d04a45fe7b52f 100644 --- a/Mathlib/Topology/Category/Profinite/Basic.lean +++ b/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 -/ diff --git a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean index d012969773445..495e15fcf3a48 100644 --- a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean +++ b/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,19 +32,6 @@ open CategoryTheory open CategoryTheory.Limits -/-- -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.{u, v} := Profinite.{max u v} - universe u v variable {J : Type v} [SmallCategory J] [IsCofiltered J] {F : J ⥤ ProfiniteMax.{u, v}} (C : Cone F) diff --git a/Mathlib/Topology/Category/Profinite/Product.lean b/Mathlib/Topology/Category/Profinite/Product.lean index 41cefdc8d8b5e..f3a74831a9426 100644 --- a/Mathlib/Topology/Category/Profinite/Product.lean +++ b/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. -/ From 8acd2bfae5fd31c0976db5d0346d422289469f23 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dagur=20T=C3=B3mas=20=C3=81sgeirsson?= Date: Wed, 29 Nov 2023 14:47:13 +0000 Subject: [PATCH 4/7] Update Mathlib/Topology/Category/Profinite/Basic.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> --- Mathlib/Topology/Category/Profinite/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean index d04a45fe7b52f..6d22c333f9112 100644 --- a/Mathlib/Topology/Category/Profinite/Basic.lean +++ b/Mathlib/Topology/Category/Profinite/Basic.lean @@ -27,7 +27,7 @@ compact, Hausdorff and totally disconnected. ## TODO -* Define procategories and prove that `Profinite` is equiavalent to `Pro (FintypeCat)`. +* Define procategories and prove that `Profinite` is equivalent to `Pro (FintypeCat)`. ## Tags From 0b8e38945717fa57150e55b9147f194449d6cd58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dagur=20T=C3=B3mas=20=C3=81sgeirsson?= Date: Wed, 29 Nov 2023 14:47:19 +0000 Subject: [PATCH 5/7] Update Mathlib/Topology/Category/Profinite/Basic.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> --- Mathlib/Topology/Category/Profinite/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean index 6d22c333f9112..636bb1f4797c2 100644 --- a/Mathlib/Topology/Category/Profinite/Basic.lean +++ b/Mathlib/Topology/Category/Profinite/Basic.lean @@ -241,7 +241,7 @@ end DiscreteTopology end Profinite /-- -Universe inequalities in Mathlib 3 are expressed through use of `max u v`. Unfortunately, +Many definitions involving universe inequalities in Mathlib 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}` From c002d202be882b7179ec1e0b98e3bc050342ac03 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dagur=20T=C3=B3mas=20=C3=81sgeirsson?= Date: Wed, 29 Nov 2023 14:48:24 +0000 Subject: [PATCH 6/7] Update Basic.lean --- Mathlib/Topology/Category/Profinite/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean index 636bb1f4797c2..43dd882235b6d 100644 --- a/Mathlib/Topology/Category/Profinite/Basic.lean +++ b/Mathlib/Topology/Category/Profinite/Basic.lean @@ -241,8 +241,8 @@ end DiscreteTopology end Profinite /-- -Many definitions involving universe inequalities in Mathlib are expressed through use of `max u v`. Unfortunately, -this leads to unbound universes which cannot be solved for during unification, eg +Many definitions involving universe inequalities in Mathlib 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. From ee240e440ccc20bb16ea09b6fdd9a3da62b68bcb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dagur=20T=C3=B3mas=20=C3=81sgeirsson?= Date: Wed, 29 Nov 2023 14:50:16 +0000 Subject: [PATCH 7/7] Update Mathlib/Topology/Category/Profinite/Basic.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/Topology/Category/Profinite/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean index 43dd882235b6d..bf4a73b35c3b0 100644 --- a/Mathlib/Topology/Category/Profinite/Basic.lean +++ b/Mathlib/Topology/Category/Profinite/Basic.lean @@ -241,7 +241,7 @@ end DiscreteTopology end Profinite /-- -Many definitions involving universe inequalities in Mathlib are expressed through use of `max u v`. +Many definitions involving universe inequalities in Mathlib 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}`