feat(ring_theory/graded_algebra): projection map of graded algebra (#…

…10116)

This pr defines and proves some property about `graded_algebra.proj : A →ₗ[R] A`



Co-authored-by: jjaassoonn <jujian.zhang1998@out.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/direct_sum/basic.lean

@@ -202,6 +202,15 @@ to_add_monoid (λ i, (A i).subtype)
   add_submonoid_coe A (of (λ i, A i) i x) = x :=
 to_add_monoid_of _ _ _
 
+lemma coe_of_add_submonoid_apply {M : Type*} [decidable_eq ι] [add_comm_monoid M]
+  {A : ι → add_submonoid M} (i j : ι) (x : A i) :
+  (of _ i x j : M) = if i = j then x else 0 :=
+begin
+  obtain rfl | h := decidable.eq_or_ne i j,
+  { rw [direct_sum.of_eq_same, if_pos rfl], },
+  { rw [direct_sum.of_eq_of_ne _ _ _ _ h, if_neg h, add_submonoid.coe_zero], },
+end
+
 /-- The `direct_sum` formed by a collection of `add_submonoid`s of `M` is said to be internal if the
 canonical map `(⨁ i, A i) →+ M` is bijective.
 
@@ -229,6 +238,15 @@ to_add_monoid (λ i, (A i).subtype)
   add_subgroup_coe A (of (λ i, A i) i x) = x :=
 to_add_monoid_of _ _ _
 
+lemma coe_of_add_subgroup_apply {M : Type*} [decidable_eq ι] [add_comm_group M]
+  {A : ι → add_subgroup M} (i j : ι) (x : A i) :
+  (of _ i x j : M) = if i = j then x else 0 :=
+begin
+  obtain rfl | h := decidable.eq_or_ne i j,
+  { rw [direct_sum.of_eq_same, if_pos rfl], },
+  { rw [direct_sum.of_eq_of_ne _ _ _ _ h, if_neg h, add_subgroup.coe_zero], },
+end
+
 /-- The `direct_sum` formed by a collection of `add_subgroup`s of `M` is said to be internal if the
 canonical map `(⨁ i, A i) →+ M` is bijective.
 

src/algebra/direct_sum/internal.lean

@@ -39,7 +39,7 @@ mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as
 internally graded ring
 -/
 
-open_locale direct_sum
+open_locale direct_sum big_operators
 
 variables {ι : Type*} {S R : Type*} [decidable_eq ι]
 
@@ -77,6 +77,18 @@ direct_sum.to_semiring (λ i, (A i).subtype) rfl (λ _ _ _ _, rfl)
   direct_sum.submonoid_coe_ring_hom A (direct_sum.of (λ i, A i) i x) = x :=
 direct_sum.to_semiring_of _ _ _ _ _
 
+lemma direct_sum.coe_mul_apply_add_submonoid [add_monoid ι] [semiring R]
+  (A : ι → add_submonoid R) [set_like.graded_monoid A]
+  [Π (i : ι) (x : A i), decidable (x ≠ 0)] (r r' : ⨁ i, A i) (i : ι) :
+  ((r * r') i : R) =
+    ∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support),
+      r ij.1 * r' ij.2 :=
+begin
+  rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply,
+    add_submonoid.coe_finset_sum],
+  simp_rw [direct_sum.coe_of_add_submonoid_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
+end
+
 /-! #### From `add_subgroup`s -/
 
 namespace add_subgroup
@@ -107,6 +119,18 @@ direct_sum.to_semiring (λ i, (A i).subtype) rfl (λ _ _ _ _, rfl)
   direct_sum.subgroup_coe_ring_hom A (direct_sum.of (λ i, A i) i x) = x :=
 direct_sum.to_semiring_of _ _ _ _ _
 
+lemma direct_sum.coe_mul_apply_add_subgroup [add_monoid ι] [ring R]
+  (A : ι → add_subgroup R) [set_like.graded_monoid A] [Π (i : ι) (x : A i), decidable (x ≠ 0)]
+  (r r' : ⨁ i, A i) (i : ι) :
+  ((r * r') i : R) =
+    ∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support),
+      r ij.1 * r' ij.2 :=
+begin
+  rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply,
+    add_subgroup.coe_finset_sum],
+  simp_rw [direct_sum.coe_of_add_subgroup_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
+end
+
 /-! #### From `submodules`s -/
 
 namespace submodule
@@ -167,3 +191,15 @@ direct_sum.to_algebra S _ (λ i, (A i).subtype) rfl (λ _ _ _ _, rfl) (λ _, rfl
   (A : ι → submodule S R) [h : set_like.graded_monoid A] (i : ι) (x : A i) :
   direct_sum.submodule_coe_alg_hom A (direct_sum.of (λ i, A i) i x) = x :=
 direct_sum.to_semiring_of _ rfl (λ _ _ _ _, rfl) _ _
+
+lemma direct_sum.coe_mul_apply_submodule [add_monoid ι]
+  [comm_semiring S] [semiring R] [algebra S R]
+  (A : ι → submodule S R) [Π (i : ι) (x : A i), decidable (x ≠ 0)]
+  [set_like.graded_monoid A] (r r' : ⨁ i, A i) (i : ι) :
+  ((r * r') i : R) =
+    ∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support),
+      r ij.1 * r' ij.2 :=
+begin
+  rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply, submodule.coe_sum],
+  simp_rw [direct_sum.coe_of_submodule_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
+end

src/algebra/direct_sum/module.lean

@@ -210,6 +210,13 @@ def submodule_coe : (⨁ i, A i) →ₗ[R] M := to_module R ι M (λ i, (A i).su
 @[simp] lemma submodule_coe_of (i : ι) (x : A i) : submodule_coe A (of (λ i, A i) i x) = x :=
 to_add_monoid_of _ _ _
 
+lemma coe_of_submodule_apply (i j : ι) (x : A i) :
+  (direct_sum.of _ i x j : M) = if i = j then x else 0 :=
+begin
+  obtain rfl | h := decidable.eq_or_ne i j,
+  { rw [direct_sum.of_eq_same, if_pos rfl], },
+  { rw [direct_sum.of_eq_of_ne _ _ _ _ h, if_neg h, submodule.coe_zero], },
+end
 
 /-- The `direct_sum` formed by a collection of `submodule`s of `M` is said to be internal if the
 canonical map `(⨁ i, A i) →ₗ[R] M` is bijective.

src/algebra/direct_sum/ring.lean

@@ -6,6 +6,7 @@ Authors: Eric Wieser
 import group_theory.subgroup.basic
 import algebra.graded_monoid
 import algebra.direct_sum.basic
+import algebra.big_operators.pi
 
 /-!
 # Additively-graded multiplicative structures on `⨁ i, A i`
@@ -223,6 +224,24 @@ begin
     exact of_eq_of_graded_monoid_eq (pow_succ (graded_monoid.mk _ a) n).symm, },
 end
 
+open_locale big_operators
+
+/-- A heavily unfolded version of the definition of multiplication -/
+lemma mul_eq_sum_support_ghas_mul
+  [Π (i : ι) (x : A i), decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
+  a * a' =
+    ∑ (ij : ι × ι) in (dfinsupp.support a).product (dfinsupp.support a'),
+      direct_sum.of _ _ (graded_monoid.ghas_mul.mul (a ij.fst) (a' ij.snd)) :=
+begin
+  change direct_sum.mul_hom _ a a' = _,
+  dsimp [direct_sum.mul_hom, direct_sum.to_add_monoid, dfinsupp.lift_add_hom_apply],
+  simp only [dfinsupp.sum_add_hom_apply, dfinsupp.sum, dfinsupp.finset_sum_apply,
+    add_monoid_hom.coe_sum, finset.sum_apply, add_monoid_hom.flip_apply,
+    add_monoid_hom.comp_hom_apply_apply, add_monoid_hom.comp_apply,
+    direct_sum.gmul_hom_apply_apply],
+  rw finset.sum_product,
+end
+
 end semiring
 
 section comm_semiring

src/group_theory/subgroup/basic.lean

@@ -376,6 +376,19 @@ coe_subtype H ▸ monoid_hom.map_pow _ _ _
 @[simp, norm_cast, to_additive] lemma coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = x ^ n :=
 coe_subtype H ▸ monoid_hom.map_zpow _ _ _
 
+@[simp, norm_cast, to_additive] theorem coe_list_prod (l : list H) :
+  (l.prod : G) = (l.map coe).prod :=
+H.to_submonoid.coe_list_prod l
+
+@[simp, norm_cast, to_additive] theorem coe_multiset_prod {G} [comm_group G] (H : subgroup G)
+  (m : multiset H) : (m.prod : G) = (m.map coe).prod :=
+H.to_submonoid.coe_multiset_prod m
+
+@[simp, norm_cast, to_additive] theorem coe_finset_prod {ι G} [comm_group G] (H : subgroup G)
+  (f : ι → H) (s : finset ι) :
+  ↑(∏ i in s, f i) = (∏ i in s, f i : G) :=
+H.to_submonoid.coe_finset_prod f s
+
 /-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
 @[to_additive "The inclusion homomorphism from a additive subgroup `H` contained in `K` to `K`."]
 def inclusion {H K : subgroup G} (h : H ≤ K) : H →* K :=

src/ring_theory/graded_algebra/basic.lean

@@ -5,6 +5,8 @@ Authors: Eric Wieser, Kevin Buzzard, Jujian Zhang
 -/
 import algebra.direct_sum.algebra
 import algebra.direct_sum.internal
+import algebra.direct_sum.ring
+import group_theory.subgroup.basic
 
 /-!
 # Internally-graded algebras
@@ -19,6 +21,10 @@ See the docstring of that typeclass for more information.
   a constructive version of `direct_sum.submodule_is_internal 𝒜`.
 * `graded_algebra.decompose : A ≃ₐ[R] ⨁ i, 𝒜 i`, which breaks apart an element of the algebra into
   its constituent pieces.
+* `graded_algebra.proj 𝒜 i` is the linear map from `A` to its degree `i : ι` component, such that
+  `proj 𝒜 i x = decompose 𝒜 x i`.
+* `graded_algebra.support 𝒜 r` is the `finset ι` containing the `i : ι` such that the degree `i`
+  component of `r` is not zero.
 
 ## Implementation notes
 
@@ -48,18 +54,19 @@ 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_algebra extends set_like.graded_monoid 𝒜 :=
 (decompose' : A → ⨁ i, 𝒜 i)
 (left_inv : function.left_inverse decompose' (direct_sum.submodule_coe 𝒜))
 (right_inv : function.right_inverse decompose' (direct_sum.submodule_coe 𝒜))
 
-lemma graded_ring.is_internal [graded_algebra 𝒜] :
+lemma graded_algebra.is_internal [graded_algebra 𝒜] :
   direct_sum.submodule_is_internal 𝒜 :=
 ⟨graded_algebra.left_inv.injective, graded_algebra.right_inv.surjective⟩
 
 variable [graded_algebra 𝒜]
 
-/-- If `A` is graded by `ι` with degree `i` component `𝒜 i`, then it is isomorphic as 
+/-- If `A` is graded by `ι` with degree `i` component `𝒜 i`, then it is isomorphic as
 an algebra to a direct sum of components. -/
 def graded_algebra.decompose : A ≃ₐ[R] ⨁ i, 𝒜 i := alg_equiv.symm
 { to_fun := direct_sum.submodule_coe_alg_hom 𝒜,
@@ -77,4 +84,59 @@ def graded_algebra.decompose : A ≃ₐ[R] ⨁ i, 𝒜 i := alg_equiv.symm
   (graded_algebra.decompose 𝒜).symm (direct_sum.of _ i x) = x :=
 direct_sum.submodule_coe_alg_hom_of 𝒜 _ _
 
+/-- The projection maps of graded algebra-/
+def graded_algebra.proj (𝒜 : ι → submodule R A) [graded_algebra 𝒜] (i : ι) : A →ₗ[R] A :=
+(𝒜 i).subtype.comp $
+  (dfinsupp.lapply i).comp $
+  (graded_algebra.decompose 𝒜).to_alg_hom.to_linear_map
+
+@[simp] lemma graded_algebra.proj_apply (i : ι) (r : A) :
+  graded_algebra.proj 𝒜 i r = (graded_algebra.decompose 𝒜 r : ⨁ i, 𝒜 i) i := rfl
+
+/-- The support of `r` is the `finset` where `proj R A i r ≠ 0 ↔ i ∈ r.support`-/
+def graded_algebra.support [Π (i : ι) (x : 𝒜 i), decidable (x ≠ 0)]
+  (r : A) : finset ι :=
+(graded_algebra.decompose 𝒜 r).support
+
+lemma graded_algebra.proj_recompose (a : ⨁ i, 𝒜 i) (i : ι) :
+  graded_algebra.proj 𝒜 i ((graded_algebra.decompose 𝒜).symm a) =
+  (graded_algebra.decompose 𝒜).symm (direct_sum.of _ i (a i)) :=
+by rw [graded_algebra.proj_apply, graded_algebra.decompose_symm_of, alg_equiv.apply_symm_apply]
+
+@[simp] lemma graded_algebra.decompose_coe {i : ι} (x : 𝒜 i) :
+  graded_algebra.decompose 𝒜 x = direct_sum.of _ i x :=
+by rw [←graded_algebra.decompose_symm_of, alg_equiv.apply_symm_apply]
+
+lemma graded_algebra.decompose_of_mem {x : A} {i : ι} (hx : x ∈ 𝒜 i) :
+  graded_algebra.decompose 𝒜 x = direct_sum.of _ i (⟨x, hx⟩ : 𝒜 i) :=
+graded_algebra.decompose_coe _ ⟨x, hx⟩
+
+lemma graded_algebra.decompose_of_mem_same {x : A} {i : ι} (hx : x ∈ 𝒜 i) :
+  (graded_algebra.decompose 𝒜 x i : A) = x :=
+by rw [graded_algebra.decompose_of_mem _ hx, direct_sum.of_eq_same, subtype.coe_mk]
+
+lemma graded_algebra.decompose_of_mem_ne {x : A} {i j : ι} (hx : x ∈ 𝒜 i) (hij : i ≠ j):
+  (graded_algebra.decompose 𝒜 x j : A) = 0 :=
+by rw [graded_algebra.decompose_of_mem _ hx, direct_sum.of_eq_of_ne _ _ _ _ hij, submodule.coe_zero]
+
+
+variable [Π (i : ι) (x : 𝒜 i), decidable (x ≠ 0)]
+
+lemma graded_algebra.mem_support_iff
+  (r : A) (i : ι) :
+  i ∈ graded_algebra.support 𝒜 r ↔ graded_algebra.proj 𝒜 i r ≠ 0 :=
+begin
+  rw [graded_algebra.support, dfinsupp.mem_support_iff, graded_algebra.proj_apply],
+  simp only [ne.def, submodule.coe_eq_zero],
+end
+
+lemma graded_algebra.sum_support_decompose (r : A) :
+  ∑ i in graded_algebra.support 𝒜 r, (graded_algebra.decompose 𝒜 r i : A) = r :=
+begin
+  conv_rhs { rw [←(graded_algebra.decompose 𝒜).symm_apply_apply r,
+    ←direct_sum.sum_support_of _ (graded_algebra.decompose 𝒜 r)] },
+  rw [alg_equiv.map_sum, graded_algebra.support],
+  simp_rw graded_algebra.decompose_symm_of,
+end
+
 end graded_algebra