chore(RepresentationTheory/FiniteIndex): generalize universes (#37271)

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

Author: Whysoserioushah

Mathlib/RepresentationTheory/FiniteIndex.lean

@@ -29,14 +29,14 @@ TODO : Fix the universe constraint
 
 @[expose] public section
 
-universe u
+universe t w u u' v v'
 
 namespace Rep
 
 open CategoryTheory Finsupp TensorProduct Representation
 
-variable {k G : Type u} [CommRing k] [Group G] {S : Subgroup G}
-  [DecidableRel (QuotientGroup.rightRel S)] (A : Rep.{u} k S)
+variable {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G}
+  [DecidableRel (QuotientGroup.rightRel S)] (A : Rep.{w} k S)
 
 /-- Let `S ≤ G` be a subgroup and `(A, ρ)` a `k`-linear `S`-representation. Then given `g : G` and
 `a : A`, this is the function `G → A` sending `sg` to `ρ(s)(a)` for all `s : S` and everything else
@@ -170,7 +170,7 @@ lemma indToCoind_coindToInd : A.coindToInd ∘ₗ A.indToCoind = LinearMap.id :=
 The forward map sends `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`, and the inverse sends `f : G → A` to
 `∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧` for `1 ≤ i ≤ n`. -/
 @[simps! hom_hom_toLinearMap inv_hom_toLinearMap]
-noncomputable def indCoindIso (A : Rep.{u} k S) :
+noncomputable def indCoindIso (A : Rep.{max w u} k S) :
     ind S.subtype A ≅ coind S.subtype A :=
   mkIso (.mk (.ofLinear (indToCoind A) (coindToInd A)
     (coindToInd_indToCoind A) (indToCoind_coindToInd A)) <| fun g ↦ by ext; simp)
@@ -181,91 +181,93 @@ variable (k S)
 `Coind_G^S` functors `Rep k S ⥤ Rep k G`. -/
 @[simps! hom_app inv_app]
 noncomputable def indCoindNatIso :
-    indFunctor k S.subtype ≅ coindFunctor k S.subtype :=
-  NatIso.ofComponents (fun (A : Rep.{u} k S) => indCoindIso A) fun f => by
+    indFunctor k S.subtype ≅ coindFunctor.{max w u} k S.subtype :=
+  NatIso.ofComponents (fun (A : Rep k S) => indCoindIso A) fun f => by
     simp only [indFunctor_obj, coindFunctor_obj];
     ext g1 x g2
     simp [indToCoind, indMap, indToCoindAux_comm]
 
 /-- Given a finite index subgroup `S ≤ G`, `Ind_S^G` is right adjoint to the restriction functor
 `Res k G ⥤ Res k S`, since it is naturally isomorphic to `Coind_S^G`. -/
 noncomputable def resIndAdjunction :
-    resFunctor.{u} S.subtype ⊣ indFunctor k S.subtype :=
-  (resCoindAdjunction k S.subtype).ofNatIsoRight (indCoindNatIso k S).symm
+    resFunctor.{max w u v} S.subtype ⊣ indFunctor.{max w u v} k S.subtype :=
+  (resCoindAdjunction.{max w u v} k S.subtype).ofNatIsoRight (indCoindNatIso.{max w u v} k S).symm
+
 
 omit [DecidableRel (QuotientGroup.rightRel S)] in
 @[instance] -- Note: we must use `@[instance] theorem` here due to [lean4#5595](https://github.com/leanprover/lean4/issues/5595).
 theorem instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype :
-    (indFunctor.{u} k S.subtype).IsRightAdjoint :=
+    (indFunctor.{max w u v} k S.subtype).IsRightAdjoint :=
   open scoped Classical in (resIndAdjunction k S).isRightAdjoint
 
 variable {k S}
 
 @[simp]
-lemma resIndAdjunction_counit_app (A : Rep.{u} k S) :
-    (resIndAdjunction k S).counit.app A =
-      (resFunctor S.subtype).map (indCoindIso A).hom ≫
-      (resCoindAdjunction k S.subtype).counit.app A := rfl
+lemma resIndAdjunction_counit_app (A : Rep.{max w u v} k S) :
+    (resIndAdjunction.{w, u, v} k S).counit.app A =
+      (resFunctor S.subtype).map (indCoindIso.{max w (max u v)} A).hom ≫
+      (resCoindAdjunction.{max w u} k S.subtype).counit.app A := rfl
 
 @[simp]
-lemma resIndAdjunction_unit_app (B : Rep.{u} k G) :
-    (resIndAdjunction k S).unit.app B = (resCoindAdjunction k S.subtype).unit.app B ≫
-      (indCoindIso (res S.subtype B)).inv := rfl
+lemma resIndAdjunction_unit_app (B : Rep.{max w u v} k G) :
+    (resIndAdjunction.{w, u, v} k S).unit.app B =
+      (resCoindAdjunction.{max w u} k S.subtype).unit.app B ≫
+      (indCoindIso.{max w (max u v)} (res S.subtype B)).inv := rfl
 
 set_option backward.isDefEq.respectTransparency false in
-lemma resIndAdjunction_homEquiv_apply (A : Rep.{u} k S)
-    {B : Rep.{u} k G} (f : res S.subtype B ⟶ A) :
-    (resIndAdjunction k S).homEquiv _ _ f =
-      resCoindHomEquiv S.subtype B A f ≫ (indCoindIso A).inv := by
+lemma resIndAdjunction_homEquiv_apply (A : Rep.{max w u v} k S)
+    {B : Rep.{max w u v} k G} (f : res S.subtype B ⟶ A) :
+    (resIndAdjunction.{w, u, v} k S).homEquiv _ _ f =
+      resCoindHomEquiv.{max w u v} S.subtype B A f ≫ (indCoindIso.{max w u v} A).inv := by
   rw [resIndAdjunction, Adjunction.homEquiv_ofNatIsoRight_apply]
   simp [resCoindHomEquiv]
 
-lemma resIndAdjunction_homEquiv_symm_apply (A : Rep.{u} k S)
-    {B : Rep.{u} k G}
-    (f : B ⟶ (indFunctor.{u} k S.subtype).obj A) :
+lemma resIndAdjunction_homEquiv_symm_apply (A : Rep.{max w u v} k S)
+    {B : Rep.{max w u v} k G}
+    (f : B ⟶ (indFunctor k S.subtype).obj A) :
     ((resIndAdjunction k S).homEquiv _ _).symm f =
-      (resCoindHomEquiv S.subtype B A).symm (f ≫ (indCoindIso A).hom) := by
+      (resCoindHomEquiv.{max w u v} S.subtype B A).symm (f ≫ (indCoindIso.{max w u v} A).hom) := by
   rfl
 
 variable (k S) in
 /-- Given a finite index subgroup `S ≤ G`, `Coind_S^G` is left adjoint to the restriction functor
 `Res k G ⥤ Res k S`, since it is naturally isomorphic to `Ind_S^G`. -/
 noncomputable def coindResAdjunction :
-    coindFunctor.{u} k S.subtype ⊣ resFunctor S.subtype :=
-  (indResAdjunction k S.subtype).ofNatIsoLeft (indCoindNatIso k S)
+    coindFunctor k S.subtype ⊣ resFunctor.{max w u v} S.subtype :=
+  (indResAdjunction k S.subtype).ofNatIsoLeft (indCoindNatIso.{max w u v} k S)
 
 omit [DecidableRel (QuotientGroup.rightRel S)] in
 @[instance] -- Note: we must use `@[instance] theorem` here due to [lean4#5595](https://github.com/leanprover/lean4/issues/5595).
 theorem instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype :
-    (coindFunctor.{u} k S.subtype).IsLeftAdjoint :=
+    (coindFunctor.{max w u v} k S.subtype).IsLeftAdjoint :=
   open scoped Classical in (coindResAdjunction k S).isLeftAdjoint
 
 @[simp]
-lemma coindResAdjunction_counit_app (B : Rep.{u} k G) :
-    (coindResAdjunction k S).counit.app B =
-      (indCoindIso (res S.subtype B)).inv ≫
+lemma coindResAdjunction_counit_app (B : Rep.{max w u v} k G) :
+    (coindResAdjunction.{w, u, v} k S).counit.app B =
+      (indCoindIso.{max w u v} (res S.subtype B)).inv ≫
       (indResAdjunction k S.subtype).counit.app B := by
   rfl
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
-lemma coindResAdjunction_unit_app (A : Rep k S) :
+lemma coindResAdjunction_unit_app (A : Rep.{max w u v} k S) :
     (coindResAdjunction k S).unit.app A = (indResAdjunction k S.subtype).unit.app A ≫
-      (resFunctor S.subtype).map (indCoindIso A).hom := by
+      (resFunctor S.subtype).map (indCoindIso.{max w u v} A).hom := by
   ext
   simp [coindResAdjunction, Adjunction.ofNatIsoLeft,
     indResAdjunction, indCoindIso]
 
-lemma coindResAdjunction_homEquiv_apply (A : Rep.{u} k S)
-    {B : Rep.{u} k G} (f : coind S.subtype A ⟶ B) :
+lemma coindResAdjunction_homEquiv_apply (A : Rep.{max w u v} k S)
+    {B : Rep k G} (f : coind S.subtype A ⟶ B) :
     (coindResAdjunction k S).homEquiv _ _ f =
-      indResHomEquiv S.subtype A B ((indCoindIso A).hom ≫ f) := by
+      indResHomEquiv S.subtype A B ((indCoindIso.{max w u v} A).hom ≫ f) := by
   rfl
 
-lemma coindResAdjunction_homEquiv_symm_apply (A : Rep.{u} k S)
-    {B : Rep.{u} k G} (f : A ⟶ res S.subtype B) :
-    ((coindResAdjunction k S).homEquiv _ _).symm f =
-      (indCoindIso A).inv ≫ (indResHomEquiv S.subtype A B).symm f := by
+lemma coindResAdjunction_homEquiv_symm_apply (A : Rep.{max w u v} k S)
+    {B : Rep k G} (f : A ⟶ res S.subtype B) :
+    ((coindResAdjunction.{max w u v} k S).homEquiv _ _).symm f =
+      (indCoindIso.{max w u v} A).inv ≫ (indResHomEquiv S.subtype A B).symm f := by
   simp only [coindResAdjunction, indResAdjunction,
     Adjunction.homEquiv_ofNatIsoLeft_symm_apply _]
   simp