feat(CategoryTheory/Galois): generalize transitivity to arbitrary universes (#16664)

The construction of the isomorphism of `Aut F` with the inverse limit of the automorphism groups of the Galois objects restricts the target category of `F` to be `FintypeCat.{v}` where `v` is the `Hom`-universe of `C`. Still, the transitivity of the action of `Aut F` on the fibers of connected objects can be generalized to arbitrary `F : C ⥤ FintypeCat.{w}` by post-composing with an equivalence `FintypeCat.{v} ≌ FintypeCat.{w}`.

Author: chrisflav

Mathlib/CategoryTheory/FintypeCat.lean

@@ -99,7 +99,7 @@ def equivEquivIso {A B : FintypeCat} : A ≃ B ≃ (A ≅ B) where
   left_inv := by aesop_cat
   right_inv := by aesop_cat
 
-instance foo (X Y : FintypeCat) : Finite (X ⟶ Y) :=
+instance (X Y : FintypeCat) : Finite (X ⟶ Y) :=
   inferInstanceAs <| Finite (X → Y)
 
 instance (X Y : FintypeCat) : Finite (X ≅ Y) :=
@@ -198,5 +198,76 @@ lemma isSkeleton : IsSkeletonOf FintypeCat Skeleton Skeleton.incl where
   skel := Skeleton.is_skeletal
   eqv := by infer_instance
 
+section Universes
+
+universe v
+
+/-- If `u` and `v` are two arbitrary universes, we may construct a functor
+`uSwitch.{u, v} : FintypeCat.{u} ⥤ FintypeCat.{v}` by sending
+`X : FintypeCat.{u}` to `ULift.{v} (Fin (Fintype.card X))`. -/
+noncomputable def uSwitch : FintypeCat.{u} ⥤ FintypeCat.{v} where
+  obj X := FintypeCat.of <| ULift.{v} (Fin (Fintype.card X))
+  map {X Y} f x := ULift.up <| (Fintype.equivFin Y) (f ((Fintype.equivFin X).symm x.down))
+  map_comp {X Y Z} f g := by ext; simp
+
+/-- Switching the universe of an object `X : FintypeCat.{u}` does not change `X` up to equivalence
+of types. This is natural in the sense that it commutes with `uSwitch.map f` for
+any `f : X ⟶ Y` in `FintypeCat.{u}`. -/
+noncomputable def uSwitchEquiv (X : FintypeCat.{u}) :
+    uSwitch.{u, v}.obj X ≃ X :=
+  Equiv.ulift.trans (Fintype.equivFin X).symm
+
+lemma uSwitchEquiv_naturality {X Y : FintypeCat.{u}} (f : X ⟶ Y)
+    (x : uSwitch.{u, v}.obj X) :
+    f (X.uSwitchEquiv x) = Y.uSwitchEquiv (uSwitch.map f x) := by
+  simp only [uSwitch, uSwitchEquiv, Equiv.trans_apply]
+  erw [Equiv.ulift_apply, Equiv.ulift_apply]
+  simp only [Equiv.symm_apply_apply]
+
+lemma uSwitchEquiv_symm_naturality {X Y : FintypeCat.{u}} (f : X ⟶ Y) (x : X) :
+    uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (f x) := by
+  rw [← Equiv.apply_eq_iff_eq_symm_apply, ← uSwitchEquiv_naturality f,
+    Equiv.apply_symm_apply]
+
+lemma uSwitch_map_uSwitch_map {X Y : FintypeCat.{u}} (f : X ⟶ Y) :
+    uSwitch.map (uSwitch.map f) =
+    (equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).hom ≫
+      f ≫ (equivEquivIso ((uSwitch.obj Y).uSwitchEquiv.trans
+      Y.uSwitchEquiv)).inv := by
+  ext x
+  simp only [comp_apply, equivEquivIso_apply_hom, Equiv.trans_apply]
+  rw [uSwitchEquiv_naturality f, ← uSwitchEquiv_naturality]
+  rfl
+
+/-- `uSwitch.{u, v}` is an equivalence of categories with quasi-inverse `uSwitch.{v, u}`. -/
+noncomputable def uSwitchEquivalence : FintypeCat.{u} ≌ FintypeCat.{v} where
+  functor := uSwitch
+  inverse := uSwitch
+  unitIso := NatIso.ofComponents (fun X ↦ (equivEquivIso <|
+    (uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv).symm) <| by
+    simp [uSwitch_map_uSwitch_map]
+  counitIso := NatIso.ofComponents (fun X ↦ equivEquivIso <|
+    (uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv) <| by
+    simp [uSwitch_map_uSwitch_map]
+  functor_unitIso_comp X := by
+    ext x
+    simp [← uSwitchEquiv_naturality]
+
+instance : uSwitch.IsEquivalence :=
+  uSwitchEquivalence.isEquivalence_functor
+
+end Universes
 
 end FintypeCat
+
+namespace FunctorToFintypeCat
+
+universe u v w
+
+variable {C : Type u} [Category.{v} C] (F G : C ⥤ FintypeCat.{w}) {X Y : C}
+
+lemma naturality (σ : F ⟶ G) (f : X ⟶ Y) (x : F.obj X) :
+    σ.app Y (F.map f x) = G.map f (σ.app X x) :=
+  congr_fun (σ.naturality f) x
+
+end FunctorToFintypeCat

Mathlib/CategoryTheory/Galois/Action.lean

@@ -26,7 +26,7 @@ namespace PreGaloisCategory
 
 open Limits Functor
 
-variable {C : Type u} [Category.{u} C] (F : C ⥤ FintypeCat.{u})
+variable {C : Type u} [Category.{v} C] (F : C ⥤ FintypeCat.{u})
 
 /-- Any (fiber) functor `F : C ⥤ FintypeCat` naturally factors via
 the forgetful functor from `Action FintypeCat (MonCat.of (Aut F))` to `FintypeCat`. -/
@@ -76,7 +76,7 @@ noncomputable instance : PreservesFiniteProducts (functorToAction F) :=
   ⟨fun J _ ↦ Action.preservesLimitsOfShapeOfPreserves (functorToAction F)
     (inferInstanceAs <| PreservesLimitsOfShape (Discrete J) F)⟩
 
-noncomputable instance (G : Type u) [Group G] [Finite G] :
+noncomputable instance (G : Type*) [Group G] [Finite G] :
     PreservesColimitsOfShape (SingleObj G) (functorToAction F) :=
   Action.preservesColimitsOfShapeOfPreserves _ <|
     inferInstanceAs <| PreservesColimitsOfShape (SingleObj G) F

Mathlib/CategoryTheory/Galois/Basic.lean

@@ -3,16 +3,14 @@ Copyright (c) 2024 Christian Merten. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christian Merten
 -/
-import Mathlib.CategoryTheory.FintypeCat
 import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
 import Mathlib.CategoryTheory.Limits.FintypeCat
 import Mathlib.CategoryTheory.Limits.MonoCoprod
-import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
-import Mathlib.CategoryTheory.Limits.Shapes.Types
 import Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
 import Mathlib.CategoryTheory.Limits.Shapes.Diagonal
 import Mathlib.CategoryTheory.SingleObj
 import Mathlib.Data.Finite.Card
+import Mathlib.Logic.Equiv.TransferInstance
 
 /-!
 # Definition and basic properties of Galois categories
@@ -41,7 +39,7 @@ as this is not needed for the proof of the fundamental theorem on Galois categor
 
 -/
 
-universe u₁ u₂ v₁ v₂ w
+universe u₁ u₂ v₁ v₂ w t
 
 namespace CategoryTheory
 
@@ -117,6 +115,11 @@ instance : HasBinaryProducts C := hasBinaryProducts_of_hasTerminal_and_pullbacks
 
 instance : HasEqualizers C := hasEqualizers_of_hasPullbacks_and_binary_products
 
+-- A `PreGaloisCategory` has quotients by finite groups in arbitrary universes. -/
+instance {G : Type*} [Group G] [Finite G] : HasColimitsOfShape (SingleObj G) C := by
+  obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
+  exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm
+
 end
 
 namespace FiberFunctor
@@ -136,6 +139,12 @@ noncomputable instance : ReflectsColimitsOfShape (Discrete PEmpty.{1}) F :=
 noncomputable instance : PreservesFiniteLimits F :=
   preservesFiniteLimitsOfPreservesTerminalAndPullbacks F
 
+/-- Fiber functors preserve quotients by finite groups in arbitrary universes. -/
+noncomputable instance {G : Type*} [Group G] [Finite G] :
+    PreservesColimitsOfShape (SingleObj G) F := by
+  choose G' hg hf he using Finite.exists_type_univ_nonempty_mulEquiv G
+  exact Limits.preservesColimitsOfShapeOfEquiv he.some.toSingleObjEquiv.symm F
+
 /-- Fiber functors reflect monomorphisms. -/
 instance : ReflectsMonomorphisms F := ReflectsMonomorphisms.mk <| by
   intro X Y f _
@@ -157,6 +166,16 @@ instance : F.Faithful where
     haveI : IsIso (equalizer.ι f g) := isIso_of_reflects_iso _ F
     exact eq_of_epi_equalizer
 
+section
+
+/-- If `F` is a fiber functor and `E` is an equivalence between categories of finite types,
+then `F ⋙ E` is again a fiber functor. -/
+noncomputable def compRight (E : FintypeCat.{w} ⥤ FintypeCat.{t}) [E.IsEquivalence] :
+    FiberFunctor (F ⋙ E) where
+  preservesQuotientsByFiniteGroups G := compPreservesColimitsOfShape F E
+
+end
+
 end FiberFunctor
 
 variable {C : Type u₁} [Category.{u₂, u₁} C]

Mathlib/CategoryTheory/Galois/Examples.lean

@@ -74,7 +74,7 @@ instance {X Y : Action FintypeCat (MonCat.of G)} (f : X ⟶ Y) :
 
 /-- The category of finite sets has quotients by finite groups in arbitrary universes. -/
 instance [Finite G] : HasColimitsOfShape (SingleObj G) FintypeCat.{w} := by
-  obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_zero_nonempty_mulEquiv G
+  obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
   exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm
 
 noncomputable instance : PreservesFiniteLimits (forget (Action FintypeCat (MonCat.of G))) := by

Mathlib/CategoryTheory/Galois/GaloisObjects.lean

@@ -35,7 +35,7 @@ open Limits Functor
 
 noncomputable instance {G : Type v} [Group G] [Finite G] :
     PreservesColimitsOfShape (SingleObj G) FintypeCat.incl.{w} := by
-  choose G' hg hf e using Finite.exists_type_zero_nonempty_mulEquiv G
+  choose G' hg hf e using Finite.exists_type_univ_nonempty_mulEquiv G
   exact Limits.preservesColimitsOfShapeOfEquiv (Classical.choice e).toSingleObjEquiv.symm _
 
 /-- A connected object `X` of `C` is Galois if the quotient `X / Aut X` is terminal. -/

Mathlib/CategoryTheory/Galois/Prorepresentability.lean

@@ -6,7 +6,6 @@ Authors: Christian Merten
 import Mathlib.Algebra.Category.Grp.Limits
 import Mathlib.CategoryTheory.CofilteredSystem
 import Mathlib.CategoryTheory.Galois.Decomposition
-import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
 import Mathlib.CategoryTheory.Limits.IndYoneda
 import Mathlib.CategoryTheory.Limits.Preserves.Ulift
 
@@ -34,6 +33,20 @@ groups of all Galois objects.
 - `FiberFunctor.isPretransitive_of_isConnected`: The `Aut F` action on the fiber of a connected
   object is transitive.
 
+## Implementation details
+
+The pro-representability statement and the isomorphism of `Aut F` with the limit over the
+automorphism groups of all Galois objects naturally forces `F` to take values in `FintypeCat.{u₂}`
+where `u₂` is the `Hom`-universe of `C`. Since this is used to show that `Aut F` acts
+transitively on `F.obj X` for connected `X`, we a priori only obtain this result for
+the mentioned specialized universe setup. To obtain the result for `F` taking values in an arbitrary
+`FintypeCat.{w}`, we postcompose with an equivalence `FintypeCat.{w} ≌ FintypeCat.{u₂}` and apply
+the specialized result.
+
+In the following the section `Specialized` is reserved for the setup where `F` takes values in
+`FintypeCat.{u₂}` and the section `General` contains results holding for `F` taking values in
+an arbitrary `FintypeCat.{w}`.
+
 ## References
 
 * [lenstraGSchemes]: H. W. Lenstra. Galois theory for schemes.
@@ -49,9 +62,9 @@ namespace PreGaloisCategory
 open Limits Functor
 
 variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
-variable (F : C ⥤ FintypeCat.{u₂})
+
 /-- A pointed Galois object is a Galois object with a fixed point of its fiber. -/
-structure PointedGaloisObject : Type (max u₁ u₂) where
+structure PointedGaloisObject (F : C ⥤ FintypeCat.{w}) : Type (max u₁ u₂ w) where
   /-- The underlying object of `C`. -/
   obj : C
   /-- An element of the fiber of `obj`. -/
@@ -61,6 +74,10 @@ structure PointedGaloisObject : Type (max u₁ u₂) where
 
 namespace PointedGaloisObject
 
+section General
+
+variable (F : C ⥤ FintypeCat.{w})
+
 attribute [instance] isGalois
 
 instance (X : PointedGaloisObject F) : CoeDep (PointedGaloisObject F) X C where
@@ -117,6 +134,12 @@ lemma incl_obj (A : PointedGaloisObject F) : (incl F).obj A = A :=
 lemma incl_map {A B : PointedGaloisObject F} (f : A ⟶ B) : (incl F).map f = f.val :=
   rfl
 
+end General
+
+section Specialized
+
+variable (F : C ⥤ FintypeCat.{u₂})
+
 /-- `F ⋙ FintypeCat.incl` as a cocone over `(can F).op ⋙ coyoneda`.
 This is a colimit cocone (see `PreGaloisCategory.isColimìt`) -/
 def cocone : Cocone ((incl F).op ⋙ coyoneda) where
@@ -172,10 +195,16 @@ noncomputable def isColimit : IsColimit (cocone F) := by
 instance : HasColimit ((incl F).op ⋙ coyoneda) where
   exists_colimit := ⟨cocone F, isColimit F⟩
 
+end Specialized
+
 end PointedGaloisObject
 
 open PointedGaloisObject
 
+section Specialized
+
+variable (F : C ⥤ FintypeCat.{u₂})
+
 /-- The diagram sending each pointed Galois object to its automorphism group
 as an object of `C`. -/
 @[simps]
@@ -393,8 +422,9 @@ theorem FiberFunctor.isPretransitive_of_isGalois (X : C) [IsGalois X] :
   use (autMulEquivAutGalois F).symm ⟨a⟩
   simpa [mulAction_def, ha]
 
-/-- The `Aut F` action on the fiber of a connected object is transitive. -/
-instance FiberFunctor.isPretransitive_of_isConnected (X : C) [IsConnected X] :
+/-- The `Aut F` action on the fiber of a connected object is transitive. For a version
+with less restrictive universe assumptions, see `FiberFunctor.isPretransitive_of_isConnected`. -/
+private instance FiberFunctor.isPretransitive_of_isConnected' (X : C) [IsConnected X] :
     MulAction.IsPretransitive (Aut F) (F.obj X) := by
   obtain ⟨A, f, hgal⟩ := exists_hom_from_galois_of_connected F X
   have hs : Function.Surjective (F.map f) := surjective_of_nonempty_fiber_of_isConnected F f
@@ -408,6 +438,39 @@ instance FiberFunctor.isPretransitive_of_isConnected (X : C) [IsConnected X] :
   show (F.map f ≫ σ.hom.app X) a = F.map f b
   rw [σ.hom.naturality, FintypeCat.comp_apply, hσ]
 
+end Specialized
+
+section General
+
+variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
+
+/-- The `Aut F` action on the fiber of a connected object is transitive. -/
+instance FiberFunctor.isPretransitive_of_isConnected (X : C) [IsConnected X] :
+    MulAction.IsPretransitive (Aut F) (F.obj X) where
+  exists_smul_eq x y := by
+    let F' : C ⥤ FintypeCat.{u₂} := F ⋙ FintypeCat.uSwitch.{w, u₂}
+    letI : FiberFunctor F' := FiberFunctor.compRight _
+    let e (Y : C) : F'.obj Y ≃ F.obj Y := (F.obj Y).uSwitchEquiv
+    set x' : F'.obj X := (e X).symm x with hx'
+    set y' : F'.obj X := (e X).symm y with hy'
+    obtain ⟨g', (hg' : g'.hom.app X x' = y')⟩ := MulAction.exists_smul_eq (Aut F') x' y'
+    let gapp (Y : C) : F.obj Y ≅ F.obj Y := FintypeCat.equivEquivIso <|
+      (e Y).symm.trans <| (FintypeCat.equivEquivIso.symm (g'.app Y)).trans (e Y)
+    let g : F ≅ F := NatIso.ofComponents gapp <| fun {X Y} f ↦ by
+      ext x
+      simp only [FintypeCat.comp_apply, FintypeCat.equivEquivIso_apply_hom,
+        Equiv.trans_apply, FintypeCat.equivEquivIso_symm_apply_apply, Iso.app_hom, gapp, e]
+      erw [FintypeCat.uSwitchEquiv_naturality (F.map f)]
+      rw [← Functor.comp_map, ← FunctorToFintypeCat.naturality]
+      simp only [comp_obj, Functor.comp_map, F']
+      rw [FintypeCat.uSwitchEquiv_symm_naturality (F.map f)]
+    refine ⟨g, show (gapp X).hom x = y from ?_⟩
+    simp only [FintypeCat.equivEquivIso_apply_hom, Equiv.trans_apply,
+      FintypeCat.equivEquivIso_symm_apply_apply, Iso.app_hom, gapp]
+    rw [← hx', hg', hy', Equiv.apply_symm_apply]
+
+end General
+
 end PreGaloisCategory
 
 end CategoryTheory

Mathlib/Logic/Equiv/TransferInstance.lean

@@ -677,11 +677,13 @@ namespace Finite
 
 attribute [-instance] Fin.instMul
 
-/-- Any finite group in universe `u` is equivalent to some finite group in universe `0`. -/
-lemma exists_type_zero_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] :
-    ∃ (G' : Type) (_ : Group G') (_ : Fintype G'), Nonempty (G ≃* G') := by
+/-- Any finite group in universe `u` is equivalent to some finite group in universe `v`. -/
+lemma exists_type_univ_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] :
+    ∃ (G' : Type v) (_ : Group G') (_ : Fintype G'), Nonempty (G ≃* G') := by
   obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G
-  letI groupH : Group (Fin n) := Equiv.group e.symm
-  exact ⟨Fin n, inferInstance, inferInstance, ⟨MulEquiv.symm <| Equiv.mulEquiv e.symm⟩⟩
+  let f : Fin n ≃ ULift (Fin n) := Equiv.ulift.symm
+  let e : G ≃ ULift (Fin n) := e.trans f
+  letI groupH : Group (ULift (Fin n)) := e.symm.group
+  exact ⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩
 
 end Finite