feat(Algebra/Module/GradedModule): generalize + to +ᵥ in indicies (…

…#7573)

The action is now of signature `A i → M j → M (i +ᵥ j)` instead of `A i → M j → M (i + j)`.
These are defeq when `i` and `j` are of the same type.

This allow the grading type of the ring and module to be different, as long as one acts additively on the other, as requested on Zulip:

@AntoineChambert-Loir [said](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/submodules.20of.20a.20graded.20module/near/395408542):
> In our work with Maria Ines,  we had the impression that some basic work on graded stuff is still missing. For example, [...] graduations which are not indexed by the same thing on the ring and on the module (some action of one on the other would be required, of course )

@kbuzzard [said](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/submodules.20of.20a.20graded.20module/near/395411889):
> In alg geom it's pretty common to have the rings indexed by $ℕ$ and the modules by $ℤ$.

Mathlib is rather short on instances for additive actions, but with suitable instances this will allow the ring to be ℕ-graded and the module to be ℤ-graded.

Mathlib/Algebra/GradedMulAction.lean

@@ -11,7 +11,7 @@ import Mathlib.Algebra.GradedMonoid
 # Additively-graded multiplicative action structures
 
 This module provides a set of heterogeneous typeclasses for defining a multiplicative structure
-over the sigma type `GradedMonoid A` such that `(•) : A i → M j → M (i + j)`; that is to say, `A`
+over the sigma type `GradedMonoid A` such that `(•) : A i → M j → M (i +ᵥ j)`; that is to say, `A`
 has an additively-graded multiplicative action on `M`. The typeclasses are:
 
 * `GradedMonoid.GSmul A M`
@@ -47,7 +47,7 @@ graded action
 -/
 
 
-variable {ι : Type*}
+variable {ιA ιB ιM  : Type*}
 
 namespace GradedMonoid
 
@@ -56,44 +56,44 @@ namespace GradedMonoid
 
 section Defs
 
-variable (A : ι → Type*) (M : ι → Type*)
+variable (A : ιA → Type*) (M : ιM → Type*)
 
 /-- A graded version of `SMul`. Scalar multiplication combines grades additively, i.e.
 if `a ∈ A i` and `m ∈ M j`, then `a • b` must be in `M (i + j)`-/
-class GSmul [Add ι] where
+class GSmul [VAdd ιA ιM] where
   /-- The homogeneous multiplication map `smul` -/
-  smul {i j} : A i → M j → M (i + j)
+  smul {i j} : A i → M j → M (i +ᵥ j)
 #align graded_monoid.ghas_smul GradedMonoid.GSmul
 
 /-- A graded version of `Mul.toSMul` -/
-instance GMul.toGSmul [Add ι] [GMul A] : GSmul A A where smul := GMul.mul
+instance GMul.toGSmul [Add ιA] [GMul A] : GSmul A A where smul := GMul.mul
 #align graded_monoid.ghas_mul.to_ghas_smul GradedMonoid.GMul.toGSmul
 
-instance GSmul.toSMul [Add ι] [GSmul A M] : SMul (GradedMonoid A) (GradedMonoid M) :=
+instance GSmul.toSMul [VAdd ιA ιM] [GSmul A M] : SMul (GradedMonoid A) (GradedMonoid M) :=
   ⟨fun x y ↦ ⟨_, GSmul.smul x.snd y.snd⟩⟩
 #align graded_monoid.ghas_smul.to_has_smul GradedMonoid.GSmul.toSMul
 
-theorem mk_smul_mk [Add ι] [GSmul A M] {i j} (a : A i) (b : M j) :
-    mk i a • mk j b = mk (i + j) (GSmul.smul a b) :=
+theorem mk_smul_mk [VAdd ιA ιM] [GSmul A M] {i j} (a : A i) (b : M j) :
+    mk i a • mk j b = mk (i +ᵥ j) (GSmul.smul a b) :=
   rfl
 #align graded_monoid.mk_smul_mk GradedMonoid.mk_smul_mk
 
 /-- A graded version of `MulAction`. -/
-class GMulAction [AddMonoid ι] [GMonoid A] extends GSmul A M where
+class GMulAction [AddMonoid ιA] [VAdd ιA ιM] [GMonoid A] extends GSmul A M where
   /-- One is the neutral element for `•` -/
   one_smul (b : GradedMonoid M) : (1 : GradedMonoid A) • b = b
   /-- Associativity of `•` and `*` -/
   mul_smul (a a' : GradedMonoid A) (b : GradedMonoid M) : (a * a') • b = a • a' • b
 #align graded_monoid.gmul_action GradedMonoid.GMulAction
 
 /-- The graded version of `Monoid.toMulAction`. -/
-instance GMonoid.toGMulAction [AddMonoid ι] [GMonoid A] : GMulAction A A :=
+instance GMonoid.toGMulAction [AddMonoid ιA] [GMonoid A] : GMulAction A A :=
   { GMul.toGSmul _ with
     one_smul := GMonoid.one_mul
     mul_smul := GMonoid.mul_assoc }
 #align graded_monoid.gmonoid.to_gmul_action GradedMonoid.GMonoid.toGMulAction
 
-instance GMulAction.toMulAction [AddMonoid ι] [GMonoid A] [GMulAction A M] :
+instance GMulAction.toMulAction [AddMonoid ιA] [GMonoid A] [VAdd ιA ιM] [GMulAction A M] :
     MulAction (GradedMonoid A) (GradedMonoid M)
     where
   one_smul := GMulAction.one_smul
@@ -112,14 +112,14 @@ section Subobjects
 variable {R : Type*}
 
 /-- A version of `GradedMonoid.GSmul` for internally graded objects. -/
-class SetLike.GradedSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
-  (A : ι → S) (B : ι → N) : Prop where
+class SetLike.GradedSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [VAdd ιA ιB]
+  (A : ιA → S) (B : ιB → N) : Prop where
   /-- Multiplication is homogeneous -/
-  smul_mem : ∀ ⦃i j : ι⦄ {ai bj}, ai ∈ A i → bj ∈ B j → ai • bj ∈ B (i + j)
+  smul_mem : ∀ ⦃i : ιA⦄ ⦃j : ιB⦄ {ai bj}, ai ∈ A i → bj ∈ B j → ai • bj ∈ B (i +ᵥ j)
 #align set_like.has_graded_smul SetLike.GradedSmul
 
-instance SetLike.toGSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
-    (A : ι → S) (B : ι → N) [SetLike.GradedSmul A B] :
+instance SetLike.toGSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [VAdd ιA ιB]
+    (A : ιA → S) (B : ιB → N) [SetLike.GradedSmul A B] :
     GradedMonoid.GSmul (fun i ↦ A i) fun i ↦ B i where
   smul a b := ⟨a.1 • b.1, SetLike.GradedSmul.smul_mem a.2 b.2⟩
 #align set_like.ghas_smul SetLike.toGSmul
@@ -133,15 +133,15 @@ example {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
     (@GradedMonoid.GSmul.smul ι (fun i ↦ A i) (fun i ↦ B i) _ _ i j x y : M) = x.1 • y.1 := by simp
 -/
 @[simp,nolint simpNF]
-theorem SetLike.coe_GSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
-    (A : ι → S) (B : ι → N) [SetLike.GradedSmul A B] {i j : ι} (x : A i) (y : B j) :
-    (@GradedMonoid.GSmul.smul ι (fun i ↦ A i) (fun i ↦ B i) _ _ i j x y : M) = x.1 • y.1 :=
+theorem SetLike.coe_GSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [VAdd ιA ιB]
+    (A : ιA → S) (B : ιB → N) [SetLike.GradedSmul A B] {i : ιA} {j : ιB} (x : A i) (y : B j) :
+    (@GradedMonoid.GSmul.smul ιA ιB (fun i ↦ A i) (fun i ↦ B i) _ _ i j x y : M) = x.1 • y.1 :=
   rfl
 #align set_like.coe_ghas_smul SetLike.coe_GSmul
 
 /-- Internally graded version of `Mul.toSMul`. -/
-instance SetLike.GradedMul.toGradedSmul [AddMonoid ι] [Monoid R] {S : Type*} [SetLike S R]
-    (A : ι → S) [SetLike.GradedMonoid A] : SetLike.GradedSmul A A where
+instance SetLike.GradedMul.toGradedSmul [AddMonoid ιA] [Monoid R] {S : Type*} [SetLike S R]
+    (A : ιA → S) [SetLike.GradedMonoid A] : SetLike.GradedSmul A A where
   smul_mem _ _ _ _ hi hj := SetLike.GradedMonoid.toGradedMul.mul_mem hi hj
 #align set_like.has_graded_mul.to_has_graded_smul SetLike.GradedMul.toGradedSmul
 
@@ -151,10 +151,10 @@ section HomogeneousElements
 
 variable {S R N M : Type*} [SetLike S R] [SetLike N M]
 
-theorem SetLike.Homogeneous.graded_smul [Add ι] [SMul R M] {A : ι → S} {B : ι → N}
+theorem SetLike.Homogeneous.graded_smul [VAdd ιA ιB] [SMul R M] {A : ιA → S} {B : ιB → N}
     [SetLike.GradedSmul A B] {a : R} {b : M} :
     SetLike.Homogeneous A a → SetLike.Homogeneous B b → SetLike.Homogeneous B (a • b)
-  | ⟨i, hi⟩, ⟨j, hj⟩ => ⟨i + j, SetLike.GradedSmul.smul_mem hi hj⟩
+  | ⟨i, hi⟩, ⟨j, hj⟩ => ⟨i +ᵥ j, SetLike.GradedSmul.smul_mem hi hj⟩
 #align set_like.is_homogeneous.graded_smul SetLike.Homogeneous.graded_smul
 
 end HomogeneousElements

Mathlib/Algebra/Module/GradedModule.lean

@@ -27,28 +27,28 @@ section
 
 open DirectSum
 
-variable {ι : Type*} (A : ι → Type*) (M : ι → Type*)
+variable {ιA ιB : Type*} (A : ιA → Type*) (M : ιB → Type*)
 
 namespace DirectSum
 
 open GradedMonoid
 
 /-- A graded version of `DistribMulAction`. -/
-class GdistribMulAction [AddMonoid ι] [GMonoid A] [∀ i, AddMonoid (M i)] extends
-  GMulAction A M where
+class GdistribMulAction [AddMonoid ιA] [VAdd ιA ιB] [GMonoid A] [∀ i, AddMonoid (M i)]
+    extends GMulAction A M where
   smul_add {i j} (a : A i) (b c : M j) : smul a (b + c) = smul a b + smul a c
   smul_zero {i j} (a : A i) : smul a (0 : M j) = 0
 #align direct_sum.gdistrib_mul_action DirectSum.GdistribMulAction
 
 /-- A graded version of `Module`. -/
-class Gmodule [AddMonoid ι] [∀ i, AddMonoid (A i)] [∀ i, AddMonoid (M i)] [GMonoid A] extends
-  GdistribMulAction A M where
+class Gmodule [AddMonoid ιA] [VAdd ιA ιB] [∀ i, AddMonoid (A i)] [∀ i, AddMonoid (M i)] [GMonoid A]
+    extends GdistribMulAction A M where
   add_smul {i j} (a a' : A i) (b : M j) : smul (a + a') b = smul a b + smul a' b
   zero_smul {i j} (b : M j) : smul (0 : A i) b = 0
 #align direct_sum.gmodule DirectSum.Gmodule
 
 /-- A graded version of `Semiring.toModule`. -/
-instance GSemiring.toGmodule [AddMonoid ι] [∀ i : ι, AddCommMonoid (A i)]
+instance GSemiring.toGmodule [AddMonoid ιA] [∀ i : ιA, AddCommMonoid (A i)]
     [h : GSemiring A] : Gmodule A A :=
   { GMonoid.toGMulAction A with
     smul_add := fun _ _ _ => h.mul_add _ _ _
@@ -57,11 +57,11 @@ instance GSemiring.toGmodule [AddMonoid ι] [∀ i : ι, AddCommMonoid (A i)]
     zero_smul := fun _ => h.zero_mul _ }
 #align direct_sum.gsemiring.to_gmodule DirectSum.GSemiring.toGmodule
 
-variable [AddMonoid ι] [∀ i : ι, AddCommMonoid (A i)] [∀ i, AddCommMonoid (M i)]
+variable [AddMonoid ιA] [VAdd ιA ιB] [∀ i : ιA, AddCommMonoid (A i)] [∀ i, AddCommMonoid (M i)]
 
 /-- The piecewise multiplication from the `Mul` instance, as a bundled homomorphism. -/
 @[simps]
-def gsmulHom [GMonoid A] [Gmodule A M] {i j} : A i →+ M j →+ M (i + j) where
+def gsmulHom [GMonoid A] [Gmodule A M] {i j} : A i →+ M j →+ M (i +ᵥ j) where
   toFun a :=
     { toFun := fun b => GSmul.smul a b
       map_zero' := GdistribMulAction.smul_zero _
@@ -74,7 +74,7 @@ namespace Gmodule
 
 /-- For graded monoid `A` and a graded module `M` over `A`. `Gmodule.smulAddMonoidHom` is the
 `⨁ᵢ Aᵢ`-scalar multiplication on `⨁ᵢ Mᵢ` induced by `gsmul_hom`. -/
-def smulAddMonoidHom [DecidableEq ι] [GMonoid A] [Gmodule A M] :
+def smulAddMonoidHom [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M] :
     (⨁ i, A i) →+ (⨁ i, M i) →+ ⨁ i, M i :=
   toAddMonoid fun _i =>
     AddMonoidHom.flip <|
@@ -85,42 +85,47 @@ section
 
 open GradedMonoid DirectSum Gmodule
 
-instance [DecidableEq ι] [GMonoid A] [Gmodule A M] : SMul (⨁ i, A i) (⨁ i, M i) where
+instance [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M] :
+    SMul (⨁ i, A i) (⨁ i, M i) where
   smul x y := smulAddMonoidHom A M x y
 
 @[simp]
-theorem smul_def [DecidableEq ι] [GMonoid A] [Gmodule A M] (x : ⨁ i, A i) (y : ⨁ i, M i) :
+theorem smul_def [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
+    (x : ⨁ i, A i) (y : ⨁ i, M i) :
     x • y = smulAddMonoidHom _ _ x y := rfl
 #align direct_sum.gmodule.smul_def DirectSum.Gmodule.smul_def
 
 @[simp]
-theorem smulAddMonoidHom_apply_of_of [DecidableEq ι] [GMonoid A] [Gmodule A M] {i j} (x : A i)
-    (y : M j) :
-    smulAddMonoidHom A M (DirectSum.of A i x) (of M j y) = of M (i + j) (GSmul.smul x y) := by
+theorem smulAddMonoidHom_apply_of_of [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
+    {i j} (x : A i) (y : M j) :
+    smulAddMonoidHom A M (DirectSum.of A i x) (of M j y) = of M (i +ᵥ j) (GSmul.smul x y) := by
   simp [smulAddMonoidHom]
 #align direct_sum.gmodule.smul_add_monoid_hom_apply_of_of DirectSum.Gmodule.smulAddMonoidHom_apply_of_of
 
 -- @[simp] -- Porting note: simpNF lint
-theorem of_smul_of [DecidableEq ι] [GMonoid A] [Gmodule A M] {i j} (x : A i) (y : M j) :
-    DirectSum.of A i x • of M j y = of M (i + j) (GSmul.smul x y) :=
+theorem of_smul_of [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
+    {i j} (x : A i) (y : M j) :
+    DirectSum.of A i x • of M j y = of M (i +ᵥ j) (GSmul.smul x y) :=
   smulAddMonoidHom_apply_of_of _ _ _ _
 #align direct_sum.gmodule.of_smul_of DirectSum.Gmodule.of_smul_of
 
 open AddMonoidHom
 
 -- Porting note: renamed to one_smul' since DirectSum.Gmodule.one_smul already exists
 -- Almost identical to the proof of `direct_sum.one_mul`
-private theorem one_smul' [DecidableEq ι] [GMonoid A] [Gmodule A M] (x : ⨁ i, M i) :
+private theorem one_smul' [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
+    (x : ⨁ i, M i) :
     (1 : ⨁ i, A i) • x = x := by
   suffices smulAddMonoidHom A M 1 = AddMonoidHom.id (⨁ i, M i) from FunLike.congr_fun this x
   apply DirectSum.addHom_ext; intro i xi
-  rw [show (1 : DirectSum ι fun i => A i) = (of A 0) GOne.one by rfl]
+  rw [show (1 : DirectSum ιA fun i => A i) = (of A 0) GOne.one by rfl]
   rw [smulAddMonoidHom_apply_of_of]
   exact DirectSum.of_eq_of_gradedMonoid_eq (one_smul (GradedMonoid A) <| GradedMonoid.mk i xi)
 
 -- Porting note: renamed to mul_smul' since DirectSum.Gmodule.mul_smul already exists
 -- Almost identical to the proof of `direct_sum.mul_assoc`
-private theorem mul_smul' [DecidableEq ι] [GSemiring A] [Gmodule A M] (a b : ⨁ i, A i)
+private theorem mul_smul' [DecidableEq ιA] [DecidableEq ιB] [GSemiring A] [Gmodule A M]
+    (a b : ⨁ i, A i)
     (c : ⨁ i, M i) : (a * b) • c = a • b • c := by
   suffices
     (-- `fun a b c ↦ (a * b) • c` as a bundled hom
@@ -140,7 +145,8 @@ private theorem mul_smul' [DecidableEq ι] [GSemiring A] [Gmodule A M] (a b : 
       (mul_smul (GradedMonoid.mk ai ax) (GradedMonoid.mk bi bx) (GradedMonoid.mk ci cx))
 
 /-- The `Module` derived from `gmodule A M`. -/
-instance module [DecidableEq ι] [GSemiring A] [Gmodule A M] : Module (⨁ i, A i) (⨁ i, M i) where
+instance module [DecidableEq ιA] [DecidableEq ιB] [GSemiring A] [Gmodule A M] :
+    Module (⨁ i, A i) (⨁ i, M i) where
   smul := (· • ·)
   one_smul := one_smul' _ _
   mul_smul := mul_smul' _ _
@@ -160,30 +166,28 @@ end
 
 open DirectSum BigOperators
 
-variable {ι R A M σ σ' : Type*}
+variable {ιA ιM R A M σ σ' : Type*}
 
-variable [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A]
+variable [AddMonoid ιA] [AddAction ιA ιM] [CommSemiring R] [Semiring A] [Algebra R A]
 
-variable (𝓐 : ι → σ') [SetLike σ' A]
+variable (𝓐 : ιA → σ') [SetLike σ' A]
 
-variable (𝓜 : ι → σ)
+variable (𝓜 : ιM → σ)
 
 namespace SetLike
 
 instance gmulAction [AddMonoid M] [DistribMulAction A M] [SetLike σ M] [SetLike.GradedMonoid 𝓐]
     [SetLike.GradedSmul 𝓐 𝓜] : GradedMonoid.GMulAction (fun i => 𝓐 i) fun i => 𝓜 i :=
-  { SetLike.toGSmul 𝓐
-      𝓜 with
-    one_smul := fun ⟨_i, _m⟩ => Sigma.subtype_ext (zero_add _) (one_smul _ _)
+  { SetLike.toGSmul 𝓐 𝓜 with
+    one_smul := fun ⟨_i, _m⟩ => Sigma.subtype_ext (zero_vadd _ _) (one_smul _ _)
     mul_smul := fun ⟨_i, _a⟩ ⟨_j, _a'⟩ ⟨_k, _b⟩ =>
-      Sigma.subtype_ext (add_assoc _ _ _) (mul_smul _ _ _) }
+      Sigma.subtype_ext (add_vadd _ _ _) (mul_smul _ _ _) }
 #align set_like.gmul_action SetLike.gmulAction
 
 instance gdistribMulAction [AddMonoid M] [DistribMulAction A M] [SetLike σ M]
     [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜] :
     DirectSum.GdistribMulAction (fun i => 𝓐 i) fun i => 𝓜 i :=
-  { SetLike.gmulAction 𝓐
-      𝓜 with
+  { SetLike.gmulAction 𝓐 𝓜 with
     smul_add := fun _a _b _c => Subtype.ext <| smul_add _ _ _
     smul_zero := fun _a => Subtype.ext <| smul_zero _ }
 #align set_like.gdistrib_mul_action SetLike.gdistribMulAction
@@ -194,8 +198,7 @@ variable [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A]
 /-- `[SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜]` is the internal version of graded
   module, the internal version can be translated into the external version `gmodule`. -/
 instance gmodule : DirectSum.Gmodule (fun i => 𝓐 i) fun i => 𝓜 i :=
-  { SetLike.gdistribMulAction 𝓐
-      𝓜 with
+  { SetLike.gdistribMulAction 𝓐 𝓜 with
     smul := fun x y => ⟨(x : A) • (y : M), SetLike.GradedSmul.smul_mem x.2 y.2⟩
     add_smul := fun _a _a' _b => Subtype.ext <| add_smul _ _ _
     zero_smul := fun _b => Subtype.ext <| zero_smul _ _ }
@@ -212,15 +215,15 @@ set_option maxHeartbeats 300000 in -- Porting note: needs more Heartbeats to ela
 /-- The smul multiplication of `A` on `⨁ i, 𝓜 i` from `(⨁ i, 𝓐 i) →+ (⨁ i, 𝓜 i) →+ ⨁ i, 𝓜 i`
 turns `⨁ i, 𝓜 i` into an `A`-module
 -/
-def isModule [DecidableEq ι] [GradedRing 𝓐] : Module A (⨁ i, 𝓜 i) :=
+def isModule [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] : Module A (⨁ i, 𝓜 i) :=
   { Module.compHom _ (DirectSum.decomposeRingEquiv 𝓐 : A ≃+* ⨁ i, 𝓐 i).toRingHom with
     smul := fun a b => DirectSum.decompose 𝓐 a • b }
 #align graded_module.is_module GradedModule.isModule
 
 /-- `⨁ i, 𝓜 i` and `M` are isomorphic as `A`-modules.
 "The internal version" and "the external version" are isomorphism as `A`-modules.
 -/
-def linearEquiv [DecidableEq ι] [GradedRing 𝓐] [DirectSum.Decomposition 𝓜] :
+def linearEquiv [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] [DirectSum.Decomposition 𝓜] :
     @LinearEquiv A A _ _ (RingHom.id A) (RingHom.id A) _ _ M (⨁ i, 𝓜 i) _
     _ _ (by letI := isModule 𝓐 𝓜; infer_instance) := by
   letI h := isModule 𝓐 𝓜