chore(CategoryTheory/Action): generalize universes (#24547)

Since #21652 the universe restrictions are no longer necessary. This also allows to remove some universe restrictions in the Galois category API.

Author: chrisflav

Mathlib/CategoryTheory/Action/Basic.lean

@@ -27,7 +27,7 @@ universe u v
 
 open CategoryTheory Limits
 
-variable (V : Type (u + 1)) [LargeCategory V]
+variable (V : Type*) [Category V]
 
 -- Note: this is _not_ a categorical action of `G` on `V`.
 /-- An `Action V G` represents a bundled action of
@@ -36,7 +36,7 @@ the monoid `G` on an object of some category `V`.
 As an example, when `V = ModuleCat R`, this is an `R`-linear representation of `G`,
 while when `V = Type` this is a `G`-action.
 -/
-structure Action (G : Type u) [Monoid G] where
+structure Action (G : Type*) [Monoid G] where
   /-- The object this action acts on -/
   V : V
   /-- The underlying monoid homomorphism of this action -/
@@ -46,11 +46,11 @@ namespace Action
 
 variable {V}
 
-theorem ρ_one {G : Type u} [Monoid G] (A : Action V G) : A.ρ 1 = 𝟙 A.V := by simp
+theorem ρ_one {G : Type*} [Monoid G] (A : Action V G) : A.ρ 1 = 𝟙 A.V := by simp
 
 /-- When a group acts, we can lift the action to the group of automorphisms. -/
 @[simps]
-def ρAut {G : Type u} [Group G] (A : Action V G) : G →* Aut A.V where
+def ρAut {G : Type*} [Group G] (A : Action V G) : G →* Aut A.V where
   toFun g :=
     { hom := A.ρ g
       inv := A.ρ (g⁻¹ : G)
@@ -59,11 +59,11 @@ def ρAut {G : Type u} [Group G] (A : Action V G) : G →* Aut A.V where
   map_one' := Aut.ext A.ρ.map_one
   map_mul' x y := Aut.ext (A.ρ.map_mul x y)
 
-variable (G : Type u) [Monoid G]
+variable (G : Type*) [Monoid G]
 
 section
 
-instance inhabited' : Inhabited (Action (Type u) G) :=
+instance inhabited' : Inhabited (Action (Type*) G) :=
   ⟨⟨PUnit, 1⟩⟩
 
 /-- The trivial representation of a group. -/
@@ -311,7 +311,7 @@ taking actions of `H` to actions of `G`.
 (This makes sense for any homomorphism, but the name is natural when `f` is a monomorphism.)
 -/
 @[simps]
-def res {G H : Type u} [Monoid G] [Monoid H] (f : G →* H) : Action V H ⥤ Action V G where
+def res {G H : Type*} [Monoid G] [Monoid H] (f : G →* H) : Action V H ⥤ Action V G where
   obj M :=
     { V := M.V
       ρ := M.ρ.comp f }
@@ -323,21 +323,21 @@ def res {G H : Type u} [Monoid G] [Monoid H] (f : G →* H) : Action V H ⥤ Act
 the identity functor on `Action V G`.
 -/
 @[simps!]
-def resId {G : Type u} [Monoid G] : res V (MonoidHom.id G) ≅ 𝟭 (Action V G) :=
+def resId {G : Type*} [Monoid G] : res V (MonoidHom.id G) ≅ 𝟭 (Action V G) :=
   NatIso.ofComponents fun M => mkIso (Iso.refl _)
 
 /-- The natural isomorphism from the composition of restrictions along homomorphisms
 to the restriction along the composition of homomorphism.
 -/
 @[simps!]
-def resComp {G H K : Type u} [Monoid G] [Monoid H] [Monoid K]
+def resComp {G H K : Type*} [Monoid G] [Monoid H] [Monoid K]
     (f : G →* H) (g : H →* K) : res V g ⋙ res V f ≅ res V (g.comp f) :=
   NatIso.ofComponents fun M => mkIso (Iso.refl _)
 
 -- TODO promote `res` to a pseudofunctor from
 -- the locally discrete bicategory constructed from `Monᵒᵖ` to `Cat`, sending `G` to `Action V G`.
 
-variable {G H : Type u} [Monoid G] [Monoid H] (f : G →* H)
+variable {G H : Type*} [Monoid G] [Monoid H] (f : G →* H)
 
 /-- The functor from `Action V H` to `Action V G` induced by a morphism `f : G → H` is faithful. -/
 instance : (res V f).Faithful where
@@ -361,12 +361,12 @@ end Action
 
 namespace CategoryTheory.Functor
 
-variable {V} {W : Type (u + 1)} [LargeCategory W]
+variable {V} {W : Type*} [Category W]
 
 /-- A functor between categories induces a functor between
 the categories of `G`-actions within those categories. -/
 @[simps]
-def mapAction (F : V ⥤ W) (G : Type u) [Monoid G] : Action V G ⥤ Action W G where
+def mapAction (F : V ⥤ W) (G : Type*) [Monoid G] : Action V G ⥤ Action W G where
   obj M :=
     { V := F.obj M.V
       ρ :=

Mathlib/CategoryTheory/Action/Concrete.lean

@@ -13,7 +13,7 @@ import Mathlib.GroupTheory.QuotientGroup.Defs
 /-!
 # Constructors for `Action V G` for some concrete categories
 
-We construct `Action (Type u) G` from a `[MulAction G X]` instance and give some applications.
+We construct `Action (Type*) G` from a `[MulAction G X]` instance and give some applications.
 -/
 
 assert_not_exists Field
@@ -25,12 +25,12 @@ open CategoryTheory Limits
 namespace Action
 
 /-- Bundles a type `H` with a multiplicative action of `G` as an `Action`. -/
-def ofMulAction (G H : Type u) [Monoid G] [MulAction G H] : Action (Type u) G where
+def ofMulAction (G : Type*) (H : Type u) [Monoid G] [MulAction G H] : Action (Type u) G where
   V := H
   ρ := @MulAction.toEndHom _ _ _ (by assumption)
 
 @[simp]
-theorem ofMulAction_apply {G H : Type u} [Monoid G] [MulAction G H] (g : G) (x : H) :
+theorem ofMulAction_apply {G H : Type*} [Monoid G] [MulAction G H] (g : G) (x : H) :
     (ofMulAction G H).ρ g x = (g • x : H) :=
   rfl
 
@@ -68,7 +68,7 @@ def diagonal (G : Type u) [Monoid G] (n : ℕ) : Action (Type u) G :=
   Action.ofMulAction G (Fin n → G)
 
 /-- We have `Fin 1 → G ≅ G` as `G`-sets, with `G` acting by left multiplication. -/
-def diagonalOneIsoLeftRegular (G : Type u) [Monoid G] : diagonal G 1 ≅ leftRegular G :=
+def diagonalOneIsoLeftRegular (G : Type*) [Monoid G] : diagonal G 1 ≅ leftRegular G :=
   Action.mkIso (Equiv.funUnique _ _).toIso fun _ => rfl
 
 namespace FintypeCat
@@ -80,13 +80,13 @@ instance (G : Type*) (X : Type*) [Monoid G] [MulAction G X] [Fintype X] :
   inferInstanceAs <| MulAction G X
 
 /-- Bundles a finite type `H` with a multiplicative action of `G` as an `Action`. -/
-def ofMulAction (G : Type u) (H : FintypeCat.{u}) [Monoid G] [MulAction G H] :
+def ofMulAction (G : Type*) (H : FintypeCat.{u}) [Monoid G] [MulAction G H] :
     Action FintypeCat G where
   V := H
   ρ := @MulAction.toEndHom _ _ _ (by assumption)
 
 @[simp]
-theorem ofMulAction_apply {G : Type u} {H : FintypeCat.{u}} [Monoid G] [MulAction G H]
+theorem ofMulAction_apply {G : Type*} {H : FintypeCat.{u}} [Monoid G] [MulAction G H]
     (g : G) (x : H) : (FintypeCat.ofMulAction G H).ρ g x = (g • x : H) :=
   rfl
 
@@ -172,7 +172,7 @@ section ToMulAction
 variable {V : Type (u + 1)} [LargeCategory V] {FV : V → V → Type*} {CV : V → Type*}
 variable [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)] [ConcreteCategory V FV]
 
-instance instMulAction {G : Type u} [Monoid G] (X : Action V G) :
+instance instMulAction {G : Type*} [Monoid G] (X : Action V G) :
     MulAction G (ToType X) where
   smul g x := ConcreteCategory.hom (X.ρ g) x
   one_smul x := by
@@ -184,7 +184,7 @@ instance instMulAction {G : Type u} [Monoid G] (X : Action V G) :
     simp
 
 /- Specialize `instMulAction` to assist typeclass inference. -/
-instance {G : Type u} [Monoid G] (X : Action FintypeCat G) : MulAction G X.V :=
+instance {G : Type*} [Monoid G] (X : Action FintypeCat G) : MulAction G X.V :=
   Action.instMulAction X
 
 end ToMulAction

Mathlib/CategoryTheory/Action/Continuous.lean

@@ -24,12 +24,10 @@ of `HasForget₂` instances.
 
 -/
 
-universe u v
-
 open CategoryTheory Limits
 
-variable (V : Type (u + 1)) [LargeCategory V] [HasForget V] [HasForget₂ V TopCat]
-variable (G : Type u) [Monoid G] [TopologicalSpace G]
+variable (V : Type*) [Category V] [HasForget V] [HasForget₂ V TopCat]
+variable (G : Type*) [Monoid G] [TopologicalSpace G]
 
 namespace Action
 

Mathlib/CategoryTheory/Action/Limits.lean

@@ -23,7 +23,7 @@ universe u v w₁ w₂ t₁ t₂
 
 open CategoryTheory Limits
 
-variable {V : Type (u + 1)} [LargeCategory V] {G : Type u} [Monoid G]
+variable {V : Type*} [Category V] {G : Type*} [Monoid G]
 
 namespace Action
 
@@ -41,7 +41,7 @@ instance [HasLimits V] : HasLimits (Action V G) :=
   Adjunction.has_limits_of_equivalence (Action.functorCategoryEquivalence _ _).functor
 
 /-- If `V` has limits of shape `J`, so does `Action V G`. -/
-instance hasLimitsOfShape {J : Type w₁} [Category.{w₂} J] [HasLimitsOfShape J V] :
+instance hasLimitsOfShape {J : Type*} [Category J] [HasLimitsOfShape J V] :
     HasLimitsOfShape J (Action V G) :=
   Adjunction.hasLimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor
 
@@ -57,20 +57,20 @@ instance [HasColimits V] : HasColimits (Action V G) :=
   Adjunction.has_colimits_of_equivalence (Action.functorCategoryEquivalence _ _).functor
 
 /-- If `V` has colimits of shape `J`, so does `Action V G`. -/
-instance hasColimitsOfShape {J : Type w₁} [Category.{w₂} J]
+instance hasColimitsOfShape {J : Type*} [Category J]
     [HasColimitsOfShape J V] : HasColimitsOfShape J (Action V G) :=
   Adjunction.hasColimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor
 
 end Limits
 
 section Preservation
 
-variable {C : Type t₁} [Category.{t₂} C]
+variable {C : Type*} [Category C]
 
 /-- `F : C ⥤ SingleObj G ⥤ V` preserves the limit of some `K : J ⥤ C` if it does
 evaluated at `SingleObj.star G`. -/
 private lemma SingleObj.preservesLimit (F : C ⥤ SingleObj G ⥤ V)
-    {J : Type w₁} [Category.{w₂} J] (K : J ⥤ C)
+    {J : Type*} [Category J] (K : J ⥤ C)
     (h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))) :
     PreservesLimit K F := by
   apply preservesLimit_of_evaluation
@@ -79,17 +79,17 @@ private lemma SingleObj.preservesLimit (F : C ⥤ SingleObj G ⥤ V)
 
 /-- `F : C ⥤ Action V G` preserves the limit of some `K : J ⥤ C` if
 if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
-lemma preservesLimit_of_preserves (F : C ⥤ Action V G) {J : Type w₁}
-    [Category.{w₂} J] (K : J ⥤ C)
+lemma preservesLimit_of_preserves (F : C ⥤ Action V G) {J : Type*}
+    [Category J] (K : J ⥤ C)
     (h : PreservesLimit K (F ⋙ Action.forget V G)) : PreservesLimit K F := by
   let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor
   have : PreservesLimit K F' := SingleObj.preservesLimit _ _ h
   apply preservesLimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor
 
 /-- `F : C ⥤ Action V G` preserves limits of some shape `J`
 if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
-lemma preservesLimitsOfShape_of_preserves (F : C ⥤ Action V G) {J : Type w₁}
-    [Category.{w₂} J] (h : PreservesLimitsOfShape J (F ⋙ Action.forget V G)) :
+lemma preservesLimitsOfShape_of_preserves (F : C ⥤ Action V G) {J : Type*}
+    [Category J] (h : PreservesLimitsOfShape J (F ⋙ Action.forget V G)) :
     PreservesLimitsOfShape J F := by
   constructor
   intro K
@@ -109,7 +109,7 @@ lemma preservesLimitsOfSize_of_preserves (F : C ⥤ Action V G)
 /-- `F : C ⥤ SingleObj G ⥤ V` preserves the colimit of some `K : J ⥤ C` if it does
 evaluated at `SingleObj.star G`. -/
 private lemma SingleObj.preservesColimit (F : C ⥤ SingleObj G ⥤ V)
-    {J : Type w₁} [Category.{w₂} J] (K : J ⥤ C)
+    {J : Type*} [Category J] (K : J ⥤ C)
     (h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))) :
     PreservesColimit K F := by
   apply preservesColimit_of_evaluation
@@ -118,17 +118,17 @@ private lemma SingleObj.preservesColimit (F : C ⥤ SingleObj G ⥤ V)
 
 /-- `F : C ⥤ Action V G` preserves the colimit of some `K : J ⥤ C` if
 if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
-lemma preservesColimit_of_preserves (F : C ⥤ Action V G) {J : Type w₁}
-    [Category.{w₂} J] (K : J ⥤ C)
+lemma preservesColimit_of_preserves (F : C ⥤ Action V G) {J : Type*}
+    [Category J] (K : J ⥤ C)
     (h : PreservesColimit K (F ⋙ Action.forget V G)) : PreservesColimit K F := by
   let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor
   have : PreservesColimit K F' := SingleObj.preservesColimit _ _ h
   apply preservesColimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor
 
 /-- `F : C ⥤ Action V G` preserves colimits of some shape `J`
 if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
-lemma preservesColimitsOfShape_of_preserves (F : C ⥤ Action V G) {J : Type w₁}
-    [Category.{w₂} J] (h : PreservesColimitsOfShape J (F ⋙ Action.forget V G)) :
+lemma preservesColimitsOfShape_of_preserves (F : C ⥤ Action V G) {J : Type*}
+    [Category J] (h : PreservesColimitsOfShape J (F ⋙ Action.forget V G)) :
     PreservesColimitsOfShape J F := by
   constructor
   intro K
@@ -149,13 +149,13 @@ end Preservation
 
 section Forget
 
-noncomputable instance {J : Type w₁} [Category.{w₂} J] [HasLimitsOfShape J V] :
+noncomputable instance {J : Type*} [Category J] [HasLimitsOfShape J V] :
     PreservesLimitsOfShape J (Action.forget V G) := by
   show PreservesLimitsOfShape J ((Action.functorCategoryEquivalence V G).functor ⋙
     (evaluation (SingleObj G) V).obj (SingleObj.star G))
   infer_instance
 
-noncomputable instance {J : Type w₁} [Category.{w₂} J] [HasColimitsOfShape J V] :
+noncomputable instance {J : Type*} [Category J] [HasColimitsOfShape J V] :
     PreservesColimitsOfShape J (Action.forget V G) := by
   show PreservesColimitsOfShape J ((Action.functorCategoryEquivalence V G).functor ⋙
     (evaluation (SingleObj G) V).obj (SingleObj.star G))
@@ -179,24 +179,24 @@ noncomputable instance [HasFiniteColimits V] : PreservesFiniteColimits (Action.f
     infer_instance
   apply comp_preservesFiniteColimits
 
-instance {J : Type w₁} [Category.{w₂} J] (F : J ⥤ Action V G) :
+instance {J : Type*} [Category J] (F : J ⥤ Action V G) :
     ReflectsLimit F (Action.forget V G) where
   reflects h := ⟨by
     apply isLimitOfReflects ((Action.functorCategoryEquivalence V G).functor)
     exact evaluationJointlyReflectsLimits _ (fun _ => h)⟩
 
-instance {J : Type w₁} [Category.{w₂} J] :
+instance {J : Type*} [Category J] :
     ReflectsLimitsOfShape J (Action.forget V G) where
 
 instance : ReflectsLimits (Action.forget V G) where
 
-instance {J : Type w₁} [Category.{w₂} J] (F : J ⥤ Action V G) :
+instance {J : Type*} [Category J] (F : J ⥤ Action V G) :
     ReflectsColimit F (Action.forget V G) where
   reflects h := ⟨by
     apply isColimitOfReflects ((Action.functorCategoryEquivalence V G).functor)
     exact evaluationJointlyReflectsColimits _ (fun _ => h)⟩
 
-noncomputable instance {J : Type w₁} [Category.{w₂} J] :
+noncomputable instance {J : Type*} [Category J] :
     ReflectsColimitsOfShape J (Action.forget V G) where
 
 noncomputable instance : ReflectsColimits (Action.forget V G) where
@@ -296,7 +296,7 @@ instance functorCategoryEquivalence_linear :
 theorem smul_hom {X Y : Action V G} (r : R) (f : X ⟶ Y) : (r • f).hom = r • f.hom :=
   rfl
 
-variable {H : Type u} [Monoid H] (f : G →* H)
+variable {H : Type*} [Monoid H] (f : G →* H)
 
 instance res_additive : (res V f).Additive where
 
@@ -307,8 +307,8 @@ end Linear
 section Abelian
 
 /-- Auxiliary construction for the `Abelian (Action V G)` instance. -/
-def abelianAux : Action V G ≌ ULift.{u} (SingleObj G) ⥤ V :=
-  (functorCategoryEquivalence V G).trans (Equivalence.congrLeft ULift.equivalence)
+def abelianAux : Action V G ≌ (SingleObj G) ⥤ V :=
+  functorCategoryEquivalence V G
 
 noncomputable instance [Abelian V] : Abelian (Action V G) :=
   abelianOfEquivalence abelianAux.functor
@@ -319,7 +319,7 @@ end Action
 
 namespace CategoryTheory.Functor
 
-variable {W : Type (u + 1)} [LargeCategory W] (F : V ⥤ W) (G : Type u) [Monoid G] [Preadditive V]
+variable {W : Type*} [Category W] (F : V ⥤ W) (G : Type*) [Monoid G] [Preadditive V]
   [Preadditive W]
 
 instance mapAction_preadditive [F.Additive] : (F.mapAction G).Additive where

Mathlib/CategoryTheory/Action/Monoidal.lean

@@ -19,11 +19,11 @@ We show:
 * When `V` is monoidal, braided, or symmetric, so is `Action V G`.
 -/
 
-universe u v
+universe u
 
 open CategoryTheory Limits MonoidalCategory
 
-variable {V : Type (u + 1)} [LargeCategory V] {G : Type u} [Monoid G]
+variable {V : Type*} [Category V] {G : Type*} [Monoid G]
 
 namespace Action
 
@@ -144,7 +144,7 @@ lemma FunctorCategoryEquivalence.functor_δ (A B : Action V G) :
     δ FunctorCategoryEquivalence.functor A B = 𝟙 _ := rfl
 
 
-variable (H : Type u) [Group H]
+variable (H : Type*) [Group H]
 
 instance [RightRigidCategory V] : RightRigidCategory (SingleObj H ⥤ V) := by
   infer_instance
@@ -227,7 +227,7 @@ noncomputable def leftRegularTensorIso (G : Type u) [Group G] (X : Action (Type
 /-- The natural isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on
 each factor. -/
 @[simps!]
-noncomputable def diagonalSucc (G : Type u) [Monoid G] (n : ℕ) :
+noncomputable def diagonalSucc (G : Type*) [Monoid G] (n : ℕ) :
     diagonal G (n + 1) ≅ leftRegular G ⊗ diagonal G n :=
   mkIso (Fin.consEquiv _).symm.toIso fun _ => rfl
 
@@ -237,7 +237,7 @@ namespace CategoryTheory.Functor
 
 open Action
 
-variable {W : Type (u + 1)} [LargeCategory W] [MonoidalCategory V] [MonoidalCategory W]
+variable {W : Type*} [Category W] [MonoidalCategory V] [MonoidalCategory W]
   (F : V ⥤ W)
 
 open Functor.LaxMonoidal Functor.OplaxMonoidal Functor.Monoidal