feat(ring_theory/mv_polynomial/homogeneous): Multivariate polynomials permit a nat-grading

src/algebra/direct_sum/algebra.lean

@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.direct_sum.ring
+import algebra.direct_sum.module
+
+/-! # Additively-graded algebra structures on `⨁ i, A i`
+
+This file provides `R`-algebra structures on external direct sums of `R`-modules.
+
+Recall that if `A i` are a family of `add_comm_monoid`s indexed by an `add_monoid`, then an instance
+of `direct_sum.gmonoid A` is a multiplication `A i → A j → A (i + j)` giving `⨁ i, A i` the
+structure of a semiring. In this file, we introduce the `direct_sum.galgebra R A` class for the case
+where all `A i` are `R`-modules. This is the extra structure needed to promote `⨁ i, A i` to an
+`R`-algebra.
+
+## Main definitions
+
+* `direct_sum.galgebra R A`, the typeclass.
+* `direct_sum.galgebra.of_submodules`, for creating the above instance from a collection of
+  submodules.
+* `direct_sum.to_algebra` extends `direct_sum.to_semiring` to produce an `alg_hom`.
+
+## Direct sums of subobjects
+
+Additionally, this module provides the instance `direct_sum.galgebra.of_submodules` which promotes
+any instance constructed with `direct_sum.gmonoid.of_submodules` to an `R`-algebra.
+
+-/
+
+universes uι uR uA uB
+
+variables {ι : Type uι}
+
+namespace direct_sum
+open_locale direct_sum
+
+variables (R : Type uR) (A : ι → Type uA) {B : Type uB} [decidable_eq ι]
+
+variables [comm_semiring R] [Π i, add_comm_monoid (A i)] [Π i, module R (A i)]
+variables [add_monoid ι] [gmonoid A]
+
+section
+
+local attribute [instance] ghas_one.to_sigma_has_one
+local attribute [instance] ghas_mul.to_sigma_has_mul
+
+/-- A graded version of `algebra`. An instance of `direct_sum.galgebra R A` endows `(⨁ i, A i)`
+with an `R`-algebra structure. -/
+class galgebra :=
+(to_fun : R →+ A 0)
+(map_one : to_fun 1 = ghas_one.one)
+(map_mul : ∀ r s, (⟨_, to_fun (r * s)⟩ : Σ i, A i) = ⟨_, ghas_mul.mul (to_fun r) (to_fun s)⟩)
+(commutes : ∀ r x, (⟨_, to_fun (r)⟩ : Σ i, A i) * x = x * ⟨_, to_fun (r)⟩)
+(smul_def : ∀ r (x : Σ i, A i), (⟨x.1, r • x.2⟩ : Σ i, A i) = ⟨_, to_fun (r)⟩ * x)
+
+end
+
+variables [semiring B] [galgebra R A] [algebra R B]
+
+instance : algebra R (⨁ i, A i) :=
+{ to_fun := (direct_sum.of A 0).comp galgebra.to_fun,
+  map_zero' := add_monoid_hom.map_zero _,
+  map_add' := add_monoid_hom.map_add _,
+  map_one' := (direct_sum.of A 0).congr_arg galgebra.map_one,
+  map_mul' := λ a b, begin
+    simp only [add_monoid_hom.comp_apply],
+    rw of_mul_of,
+    apply dfinsupp.single_eq_of_sigma_eq (galgebra.map_mul a b),
+  end,
+  commutes' := λ r x, begin
+    change add_monoid_hom.mul (direct_sum.of _ _ _) x =
+      add_monoid_hom.mul.flip (direct_sum.of _ _ _) x,
+    apply add_monoid_hom.congr_fun _ x,
+    ext i xi : 2,
+    dsimp only [add_monoid_hom.comp_apply, add_monoid_hom.mul_apply, add_monoid_hom.flip_apply],
+    rw [of_mul_of, of_mul_of],
+    apply dfinsupp.single_eq_of_sigma_eq (galgebra.commutes r ⟨i, xi⟩),
+  end,
+  smul_def' := λ r x, begin
+    change const_smul_hom _ r x = add_monoid_hom.mul (direct_sum.of _ _ _) x,
+    apply add_monoid_hom.congr_fun _ x,
+    ext i xi : 2,
+    dsimp only [add_monoid_hom.comp_apply, const_smul_hom_apply, add_monoid_hom.mul_apply],
+    rw [direct_sum.of_mul_of, ←of_smul],
+    apply dfinsupp.single_eq_of_sigma_eq (galgebra.smul_def r ⟨i, xi⟩),
+  end }
+
+section
+-- for `simps`
+local attribute [simp] linear_map.cod_restrict
+
+/-- A `direct_sum.gmonoid` instance produced by `direct_sum.gmonoid.of_submodules` is automatically
+a `direct_sum.galgebra`. -/
+@[simps to_fun_apply {simp_rhs := tt}]
+instance galgebra.of_submodules
+  (carriers : ι → submodule R B)
+  (one_mem : (1 : B) ∈ carriers 0)
+  (mul_mem : ∀ ⦃i j⦄ (gi : carriers i) (gj : carriers j), (gi * gj : B) ∈ carriers (i + j)) :
+  by haveI : gmonoid (λ i, carriers i) := gmonoid.of_submodules carriers one_mem mul_mem; exact
+  galgebra R (λ i, carriers i) :=
+by exact {
+  to_fun := begin
+    refine ((algebra.linear_map R B).cod_restrict (carriers 0) $ λ r, _).to_add_monoid_hom,
+    exact submodule.one_le.mpr one_mem (submodule.algebra_map_mem _),
+  end,
+  map_one := subtype.ext $ by exact (algebra_map R B).map_one,
+  map_mul := λ x y, sigma.subtype_ext (add_zero 0).symm $ (algebra_map R B).map_mul _ _,
+  commutes := λ r ⟨i, xi⟩,
+    sigma.subtype_ext ((zero_add i).trans (add_zero i).symm) $ algebra.commutes _ _,
+  smul_def := λ r ⟨i, xi⟩, sigma.subtype_ext (zero_add i).symm $ algebra.smul_def _ _ }
+
+end
+
+/-- A family of `linear_map`s preserving `direct_sum.ghas_one.one` and `direct_sum.ghas_mul.mul`
+describes an `alg_hom` on `⨁ i, A i`. This is a stronger version of `direct_sum.to_semiring`.
+
+Of particular interest is the case when `A i` are bundled subojects, `f` is the family of
+coercions such as `submodule.subtype (A i)`, and the `[gmonoid A]` structure originates from
+`direct_sum.gmonoid.of_add_submodules`, in which case the proofs about `ghas_one` and `ghas_mul`
+can be discharged by `rfl`. -/
+@[simps]
+def to_algebra
+  (f : Π i, A i →ₗ[R] B) (hone : f _ (ghas_one.one) = 1)
+  (hmul : ∀ {i j} (ai : A i) (aj : A j), f _ (ghas_mul.mul ai aj) = f _ ai * f _ aj)
+  (hcommutes : ∀ r, (f 0) (galgebra.to_fun r) = (algebra_map R B) r) :
+  (⨁ i, A i) →ₐ[R] B :=
+{ to_fun := to_semiring (λ i, (f i).to_add_monoid_hom) hone @hmul,
+  commutes' := λ r, (direct_sum.to_semiring_of _ _ _ _ _).trans (hcommutes r),
+  .. to_semiring (λ i, (f i).to_add_monoid_hom) hone @hmul}
+
+/-- Two `alg_hom`s out of a direct sum are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+lemma alg_hom_ext ⦃f g : (⨁ i, A i) →ₐ[R] B⦄
+  (h : ∀ i, f.to_linear_map.comp (lof _ _ A i) = g.to_linear_map.comp (lof _ _ A i)) : f = g :=
+alg_hom.coe_ring_hom_injective $
+  direct_sum.ring_hom_ext $ λ i, add_monoid_hom.ext $ linear_map.congr_fun (h i)
+
+end direct_sum
+
+/-! ### Concrete instances -/
+
+/-- A direct sum of copies of a `algebra` inherits the algebra structure.
+
+-/
+@[simps]
+instance algebra.direct_sum_galgebra {R A : Type*} [decidable_eq ι]
+  [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A] :
+  direct_sum.galgebra R (λ i : ι, A) :=
+{ to_fun := (algebra_map R A).to_add_monoid_hom,
+  map_one := (algebra_map R A).map_one,
+  map_mul := λ a b, sigma.ext (zero_add _).symm (heq_of_eq $ (algebra_map R A).map_mul a b),
+  commutes := λ r ⟨ai, a⟩, sigma.ext ((zero_add _).trans (add_zero _).symm)
+                                    (heq_of_eq $ algebra.commutes _ _),
+  smul_def := λ r ⟨ai, a⟩, sigma.ext (zero_add _).symm (heq_of_eq $ algebra.smul_def _ _) }
+
+namespace submodule
+
+variables {R A : Type*} [comm_semiring R]
+
+end submodule

src/algebra/direct_sum/module.lean

@@ -56,6 +56,9 @@ dfinsupp.lmk
 /-- Inclusion of each component into the direct sum. -/
 def lof : Π i : ι, M i →ₗ[R] (⨁ i, M i) :=
 dfinsupp.lsingle
+
+lemma lof_eq_of (i : ι) (b : M i) : lof R ι M i b = of M i b := rfl
+
 variables {ι M}
 
 lemma single_eq_lof (i : ι) (b : M i) :
@@ -103,9 +106,13 @@ to_add_monoid.unique ψ.to_add_monoid_hom f
 
 variables {ψ} {ψ' : (⨁ i, M i) →ₗ[R] N}
 
-theorem to_module.ext (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) (f : ⨁ i, M i) :
-  ψ f = ψ' f :=
-by rw dfinsupp.lhom_ext' H
+/-- Two `linear_map`s out of a direct sum are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+theorem linear_map_ext ⦃ψ ψ' : (⨁ i, M i) →ₗ[R] N⦄
+  (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) : ψ = ψ' :=
+dfinsupp.lhom_ext' H
 
 /--
 The inclusion of a subset of the direct summands

src/algebra/direct_sum/ring.lean

@@ -95,11 +95,11 @@ class ghas_mul [has_add ι] [Π i, add_comm_monoid (A i)] :=
 variables {A}
 
 /-- `direct_sum.ghas_one` implies a `has_one (Σ i, A i)`, although this is only used as an instance
-locally to define notation in `direct_sum.gmonoid`. -/
+locally to define notation in `direct_sum.gmonoid` and similar typeclasses. -/
 def ghas_one.to_sigma_has_one [has_zero ι] [ghas_one A] : has_one (Σ i, A i) := ⟨⟨_, ghas_one.one⟩⟩
 
 /-- `direct_sum.ghas_mul` implies a `has_mul (Σ i, A i)`, although this is only used as an instance
-locally to define notation in `direct_sum.gmonoid`. -/
+locally to define notation in `direct_sum.gmonoid` and similar typeclasses. -/
 def ghas_mul.to_sigma_has_mul [has_add ι] [Π i, add_comm_monoid (A i)] [ghas_mul A] :
   has_mul (Σ i, A i) :=
 ⟨λ (x y : Σ i, A i), ⟨_, ghas_mul.mul x.snd y.snd⟩⟩
@@ -634,6 +634,15 @@ def lift_ring_hom :
       add_monoid_hom.comp_apply, to_semiring_coe_add_monoid_hom],
   end}
 
+/-- Two `ring_hom`s out of a direct sum are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+lemma ring_hom_ext ⦃f g : (⨁ i, A i) →+* R⦄
+  (h : ∀ i, (↑f : (⨁ i, A i) →+ R).comp (of A i) = (↑g : (⨁ i, A i) →+ R).comp (of A i)) :
+  f = g :=
+direct_sum.lift_ring_hom.symm.injective $ subtype.ext $ funext h
+
 end to_semiring
 
 end direct_sum

src/algebra/monoid_algebra_to_direct_sum.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import algebra.direct_sum.ring
+import algebra.direct_sum.algebra
 import algebra.monoid_algebra
 import data.finsupp.to_dfinsupp
 
@@ -24,6 +24,7 @@ Note that since `direct_sum.has_mul` combines indices additively, there is no eq
   * `add_monoid_algebra_equiv_direct_sum : add_monoid_algebra M ι ≃ (⨁ i : ι, M)`
   * `add_monoid_algebra_add_equiv_direct_sum : add_monoid_algebra M ι ≃+ (⨁ i : ι, M)`
   * `add_monoid_algebra_ring_equiv_direct_sum R : add_monoid_algebra M ι ≃+* (⨁ i : ι, M)`
+  * `add_monoid_algebra_alg_equiv_direct_sum R : add_monoid_algebra A ι ≃ₐ[R] (⨁ i : ι, A)`
 
 ## Theorems
 
@@ -53,7 +54,7 @@ Note that there is no `add_monoid_algebra` equivalent to `finsupp.single`, so ma
 still involve this definition.
 -/
 
-variables {ι : Type*} {R : Type*} {M : Type*}
+variables {ι : Type*} {R : Type*} {M : Type*} {A : Type*}
 
 open_locale direct_sum
 
@@ -172,8 +173,9 @@ noncomputable def add_monoid_algebra_add_equiv_direct_sum
   map_add' := add_monoid_algebra.to_direct_sum_add,
   .. add_monoid_algebra_equiv_direct_sum}
 
-/-- `add_monoid_algebra` is equivalent to a homogenous direct sum.
-This is non-computable because `add_monoid_algebra` is noncomputable. -/
+/-- The ring version of `add_monoid_algebra.to_add_monoid_algebra`. Note that this is
+`noncomputable` because `add_monoid_algebra.has_add` is noncomputable. -/
+@[simps {fully_applied := ff}]
 noncomputable def add_monoid_algebra_ring_equiv_direct_sum
   [decidable_eq ι] [add_monoid ι] [semiring M]
   [Π m : M, decidable (m ≠ 0)] :
@@ -182,4 +184,15 @@ noncomputable def add_monoid_algebra_ring_equiv_direct_sum
   map_mul' := add_monoid_algebra.to_direct_sum_mul,
   ..(add_monoid_algebra_add_equiv_direct_sum : add_monoid_algebra M ι ≃+ ⨁ i : ι, M) }
 
+/-- The algebra version of `add_monoid_algebra.to_add_monoid_algebra`. Note that this is
+`noncomputable` because `add_monoid_algebra.has_add` is noncomputable. -/
+@[simps {fully_applied := ff}]
+noncomputable def add_monoid_algebra_alg_equiv_direct_sum
+  [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A]
+  [Π m : A, decidable (m ≠ 0)] :
+  add_monoid_algebra A ι ≃ₐ[R] ⨁ i : ι, A :=
+{ to_fun := add_monoid_algebra.to_direct_sum, inv_fun := direct_sum.to_add_monoid_algebra,
+  commutes' := λ r, add_monoid_algebra.to_direct_sum_single _ _,
+  ..(add_monoid_algebra_ring_equiv_direct_sum : add_monoid_algebra A ι ≃+* ⨁ i : ι, A) }
+
 end equivs

src/linear_algebra/direct_sum/tensor_product.lean

@@ -37,14 +37,10 @@ begin
     (lift $ direct_sum.to_module R _ _ $ λ i₁, flip $ direct_sum.to_module R _ _ $ λ i₂,
       flip $ curry $ direct_sum.lof R (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))
     (direct_sum.to_module R _ _ $ λ i, map (direct_sum.lof R _ _ _) (direct_sum.lof R _ _ _))
-    (linear_map.ext $ direct_sum.to_module.ext _ $ λ i, mk_compr₂_inj $
-      linear_map.ext $ λ x₁, linear_map.ext $ λ x₂, _)
-    (mk_compr₂_inj $ linear_map.ext $ direct_sum.to_module.ext _ $ λ i₁, linear_map.ext $ λ x₁,
-      linear_map.ext $ direct_sum.to_module.ext _ $ λ i₂, linear_map.ext $ λ x₂, _),
+    _ _; [ext ⟨i₁, i₂⟩ x₁ x₂ : 4, ext i₁ i₂ x₁ x₂ : 5],
   repeat { rw compr₂_apply <|> rw comp_apply <|> rw id_apply <|> rw mk_apply <|>
     rw direct_sum.to_module_lof <|> rw map_tmul <|> rw lift.tmul <|> rw flip_apply <|>
     rw curry_apply },
-  cases i; refl
 end
 
 @[simp] theorem direct_sum_lof_tmul_lof (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :