refactor(ring_theory/graded_algebra): use add_submonoid_class to ge…

…neralize to graded rings (#14583)

Now that we have `add_submonoid_class`, we don't need to consider only families of submodules.
For convenience, this keeps around `graded_algebra` as an alias for `graded_ring` over a family of submodules, as this can help with elaboration here and there.

This renames:
* `graded_algebra` to `graded_ring`
* `graded_algebra.proj_zero_ring_hom` to `graded_ring.proj_zero_ring_hom`

adds:
* `direct_sum.decompose_ring_equiv`
* `graded_ring.proj`
* `graded_algebra` (as an alias for a suitable `graded_ring`

and removes:
* `graded_algebra.is_internal`, which was just an alias anyway.


Co-authored-by: Jujian Zhang <[email protected]>

src/algebra/direct_sum/internal.lean

@@ -143,8 +143,8 @@ def direct_sum.coe_ring_hom [add_monoid ι] [semiring R] [set_like σ R]
 direct_sum.to_semiring (λ i, add_submonoid_class.subtype (A i)) rfl (λ _ _ _ _, rfl)
 
 /-- The canonical ring isomorphism between `⨁ i, A i` and `R`-/
-@[simp] lemma direct_sum.coe_ring_hom_of [add_monoid ι] [semiring R]
-  (A : ι → add_submonoid R) [set_like.graded_monoid A] (i : ι) (x : A i) :
+@[simp] lemma direct_sum.coe_ring_hom_of [add_monoid ι] [semiring R] [set_like σ R]
+  [add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid A] (i : ι) (x : A i) :
   direct_sum.coe_ring_hom A (direct_sum.of (λ i, A i) i x) = x :=
 direct_sum.to_semiring_of _ _ _ _ _
 

src/linear_algebra/clifford_algebra/grading.lean

@@ -123,16 +123,15 @@ graded_algebra.of_alg_hom (even_odd Q)
 
 lemma supr_ι_range_eq_top : (⨆ i : ℕ, (ι Q).range ^ i) = ⊤ :=
 begin
-  rw [← (graded_algebra.is_internal $ λ i, even_odd Q i).submodule_supr_eq_top, eq_comm],
-  dunfold even_odd,
+  rw [← (direct_sum.decomposition.is_internal (even_odd Q)).submodule_supr_eq_top, eq_comm],
   calc    (⨆ (i : zmod 2) (j : {n // ↑n = i}), (ι Q).range ^ ↑j)
         = (⨆ (i : Σ i : zmod 2, {n : ℕ // ↑n = i}), (ι Q).range ^ (i.2 : ℕ)) : by rw supr_sigma
     ... = (⨆ (i : ℕ), (ι Q).range ^ i)
         : function.surjective.supr_congr (λ i, i.2) (λ i, ⟨⟨_, i, rfl⟩, rfl⟩) (λ _, rfl),
 end
 
 lemma even_odd_is_compl : is_compl (even_odd Q 0) (even_odd Q 1) :=
-(graded_algebra.is_internal (even_odd Q)).is_compl zero_ne_one $ begin
+(direct_sum.decomposition.is_internal (even_odd Q)).is_compl zero_ne_one $ begin
   have : (finset.univ : finset (zmod 2)) = {0, 1} := rfl,
   simpa using congr_arg (coe : finset (zmod 2) → set (zmod 2)) this,
 end

src/ring_theory/graded_algebra/basic.lean

@@ -10,16 +10,19 @@ import algebra.direct_sum.ring
 import group_theory.subgroup.basic
 
 /-!
-# Internally-graded algebras
+# Internally-graded rings and algebras
 
 This file defines the typeclass `graded_algebra 𝒜`, for working with an algebra `A` that is
 internally graded by a collection of submodules `𝒜 : ι → submodule R A`.
 See the docstring of that typeclass for more information.
 
 ## Main definitions
 
-* `graded_algebra 𝒜`: the typeclass, which is a combination of `set_like.graded_monoid`, and
+* `graded_ring 𝒜`: the typeclass, which is a combination of `set_like.graded_monoid`, and
   `direct_sum.decomposition 𝒜`.
+* `graded_algebra 𝒜`: A convenience alias for `graded_ring` when `𝒜` is a family of submodules.
+* `direct_sum.decompose_ring_equiv 𝒜 : A ≃ₐ[R] ⨁ i, 𝒜 i`, a more bundled version of
+  `direct_sum.decompose 𝒜`.
 * `direct_sum.decompose_alg_equiv 𝒜 : A ≃ₐ[R] ⨁ i, 𝒜 i`, a more bundled version of
   `direct_sum.decompose 𝒜`.
 * `graded_algebra.proj 𝒜 i` is the linear map from `A` to its degree `i : ι` component, such that
@@ -38,11 +41,14 @@ graded algebra, graded ring, graded semiring, decomposition
 
 open_locale direct_sum big_operators
 
-section graded_algebra
-
-variables {ι R A : Type*}
+variables {ι R A σ : Type*}
+section graded_ring
 variables [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A]
-variables (𝒜 : ι → submodule R A)
+variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ)
+
+include A
+
+open direct_sum
 
 /-- An internally-graded `R`-algebra `A` is one that can be decomposed into a collection
 of `submodule R A`s indexed by `ι` such that the canonical map `A → ⨁ i, 𝒜 i` is bijective and
@@ -53,11 +59,58 @@ Note that the fact that `A` is internally-graded, `graded_algebra 𝒜`, implies
 algebra structure `direct_sum.galgebra R (λ i, ↥(𝒜 i))`, which in turn makes available an
 `algebra R (⨁ i, 𝒜 i)` instance.
 -/
+class graded_ring (𝒜 : ι → σ) extends set_like.graded_monoid 𝒜, direct_sum.decomposition 𝒜.
+
+variables [graded_ring 𝒜]
+namespace direct_sum
 
-class graded_algebra extends set_like.graded_monoid 𝒜, direct_sum.decomposition 𝒜.
+/-- If `A` is graded by `ι` with degree `i` component `𝒜 i`, then it is isomorphic as
+a ring to a direct sum of components. -/
+def decompose_ring_equiv : A ≃+* ⨁ i, 𝒜 i := ring_equiv.symm
+{ map_mul' := (coe_ring_hom 𝒜).map_mul,
+  map_add' := (coe_ring_hom 𝒜).map_add,
+  ..(decompose_add_equiv 𝒜).symm }
 
-protected lemma graded_algebra.is_internal [graded_algebra 𝒜] : direct_sum.is_internal 𝒜 :=
-direct_sum.decomposition.is_internal _
+@[simp] lemma decompose_one : decompose 𝒜 (1 : A) = 1 := map_one (decompose_ring_equiv 𝒜)
+@[simp] lemma decompose_symm_one : (decompose 𝒜).symm 1 = (1 : A) :=
+map_one (decompose_ring_equiv 𝒜).symm
+
+@[simp] lemma decompose_mul (x y : A) : decompose 𝒜 (x * y) = decompose 𝒜 x * decompose 𝒜 y :=
+map_mul (decompose_ring_equiv 𝒜) x y
+@[simp] lemma decompose_symm_mul (x y : ⨁ i, 𝒜 i) :
+  (decompose 𝒜).symm (x * y) = (decompose 𝒜).symm x * (decompose 𝒜).symm y :=
+map_mul (decompose_ring_equiv 𝒜).symm x y
+
+end direct_sum
+
+/-- The projection maps of a graded ring -/
+def graded_ring.proj (i : ι) : A →+ A :=
+(add_submonoid_class.subtype (𝒜 i)).comp $
+  (dfinsupp.eval_add_monoid_hom i).comp $
+  ring_hom.to_add_monoid_hom $ ring_equiv.to_ring_hom $ direct_sum.decompose_ring_equiv 𝒜
+
+@[simp] lemma graded_ring.proj_apply (i : ι) (r : A) :
+  graded_ring.proj 𝒜 i r = (decompose 𝒜 r : ⨁ i, 𝒜 i) i := rfl
+
+lemma graded_ring.proj_recompose (a : ⨁ i, 𝒜 i) (i : ι) :
+  graded_ring.proj 𝒜 i ((decompose 𝒜).symm a) =
+  (decompose 𝒜).symm (direct_sum.of _ i (a i)) :=
+by rw [graded_ring.proj_apply, decompose_symm_of, equiv.apply_symm_apply]
+
+lemma graded_ring.mem_support_iff [Π i (x : 𝒜 i), decidable (x ≠ 0)] (r : A) (i : ι) :
+  i ∈ (decompose 𝒜 r).support ↔ graded_ring.proj 𝒜 i r ≠ 0 :=
+dfinsupp.mem_support_iff.trans add_submonoid_class.coe_eq_zero.not.symm
+
+end graded_ring
+
+section graded_algebra
+variables [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A]
+variables (𝒜 : ι → submodule R A)
+
+/-- A special case of `graded_ring` with `σ = submodule R A`. This is useful both because it
+can avoid typeclass search, and because it provides a more concise name. -/
+@[reducible]
+def graded_algebra := graded_ring 𝒜
 
 /-- A helper to construct a `graded_algebra` when the `set_like.graded_monoid` structure is already
 available. This makes the `left_inv` condition easier to prove, and phrases the `right_inv`
@@ -91,16 +144,6 @@ def decompose_alg_equiv : A ≃ₐ[R] ⨁ i, 𝒜 i := alg_equiv.symm
   commutes' := (coe_alg_hom 𝒜).commutes,
   ..(decompose_add_equiv 𝒜).symm }
 
-@[simp] lemma decompose_one : decompose 𝒜 (1 : A) = 1 := map_one (decompose_alg_equiv 𝒜)
-@[simp] lemma decompose_symm_one : (decompose 𝒜).symm 1 = (1 : A) :=
-map_one (decompose_alg_equiv 𝒜).symm
-
-@[simp] lemma decompose_mul (x y : A) : decompose 𝒜 (x * y) = decompose 𝒜 x * decompose 𝒜 y :=
-map_mul (decompose_alg_equiv 𝒜) x y
-@[simp] lemma decompose_symm_mul (x y : ⨁ i, 𝒜 i) :
-  (decompose 𝒜).symm (x * y) = (decompose 𝒜).symm x * (decompose 𝒜).symm y :=
-map_mul (decompose_alg_equiv 𝒜).symm x y
-
 end direct_sum
 
 open direct_sum
@@ -127,30 +170,39 @@ end graded_algebra
 
 section canonical_order
 
-open graded_algebra set_like.graded_monoid direct_sum
+open graded_ring set_like.graded_monoid direct_sum
 
-variables {ι R A : Type*}
-variables [comm_semiring R] [semiring A]
-variables [algebra R A] [decidable_eq ι]
+variables [semiring A] [decidable_eq ι]
 variables [canonically_ordered_add_monoid ι]
-variables (𝒜 : ι → submodule R A) [graded_algebra 𝒜]
+variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜]
 
 /--
 If `A` is graded by a canonically ordered add monoid, then the projection map `x ↦ x₀` is a ring
 homomorphism.
 -/
 @[simps]
-def graded_algebra.proj_zero_ring_hom : A →+* A :=
+def graded_ring.proj_zero_ring_hom : A →+* A :=
 { to_fun := λ a, decompose 𝒜 a 0,
   map_one' := decompose_of_mem_same 𝒜 one_mem,
-  map_zero' := by simp only [subtype.ext_iff_val, decompose_zero, zero_apply, submodule.coe_zero],
-  map_add' := λ _ _, by simp [subtype.ext_iff_val, decompose_add, add_apply, submodule.coe_add],
-  map_mul' := λ x y,
-    have m : ∀ x, x ∈ supr 𝒜,
-    from λ x, (graded_algebra.is_internal 𝒜).submodule_supr_eq_top.symm ▸ submodule.mem_top,
-    begin
-    refine submodule.supr_induction 𝒜 (m x) (λ i c hc, _) _ _,
-    { refine submodule.supr_induction 𝒜 (m y) (λ j c' hc', _) _ _,
+  map_zero' := by simp,
+  map_add' := λ _ _, by simp,
+  map_mul' := λ x y, begin
+    -- Convert the abstract add_submonoid into a concrete one. This is necessary as there is no
+    -- lattice structure on the abstract ones.
+    let 𝒜' : ι → add_submonoid A :=
+      λ i, (⟨𝒜 i, λ _ _, add_mem_class.add_mem, zero_mem_class.zero_mem _⟩ : add_submonoid A),
+    letI : graded_ring 𝒜' :=
+      { decompose' := (direct_sum.decompose 𝒜 : A → ⨁ i, 𝒜 i),
+        left_inv := direct_sum.decomposition.left_inv,
+        right_inv := direct_sum.decomposition.right_inv,
+        ..(by apply_instance : set_like.graded_monoid 𝒜), },
+    have m : ∀ x, x ∈ supr 𝒜',
+    { intro x,
+      rw direct_sum.is_internal.add_submonoid_supr_eq_top 𝒜'
+        (direct_sum.decomposition.is_internal 𝒜'),
+      exact add_submonoid.mem_top x },
+    refine add_submonoid.supr_induction 𝒜' (m x) (λ i c hc, _) _ _,
+    { refine add_submonoid.supr_induction 𝒜' (m y) (λ j c' hc', _) _ _,
       { by_cases h : i + j = 0,
         { rw [decompose_of_mem_same 𝒜 (show c * c' ∈ 𝒜 0, from h ▸ mul_mem hc hc'),
             decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0, from (add_eq_zero_iff.mp h).1 ▸ hc),
@@ -159,11 +211,12 @@ def graded_algebra.proj_zero_ring_hom : A →+* A :=
           cases (show i ≠ 0 ∨ j ≠ 0, by rwa [add_eq_zero_iff, not_and_distrib] at h) with h' h',
           { simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul] },
           { simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero] } } },
-      { simp only [decompose_zero, zero_apply, submodule.coe_zero, mul_zero] },
+      { simp only [decompose_zero, zero_apply, add_submonoid_class.coe_zero, mul_zero], },
       { intros _ _ hd he,
-        simp only [mul_add, decompose_add, add_apply, submodule.coe_add, hd, he] } },
-    { simp only [decompose_zero, zero_apply, submodule.coe_zero, zero_mul] },
-    { rintros _ _ ha hb, simp only [add_mul, decompose_add, add_apply, submodule.coe_add, ha, hb] },
+        simp only [mul_add, decompose_add, add_apply, add_mem_class.coe_add, hd, he] } },
+    { simp only [decompose_zero, zero_apply, add_submonoid_class.coe_zero, zero_mul] },
+    { rintros _ _ ha hb,
+      simp only [add_mul, decompose_add, add_apply, add_mem_class.coe_add, ha, hb] },
   end }
 
 end canonical_order