feat(ring_theory/graded_algebra): homogeneous_element (#10118)

This pr is about what `homogeneous_element` of graded ring is.

We need this definition to make the definition of homogeneous ideal more natural, i.e. we can say that a homogeneous ideal is just an ideal spanned by homogeneous elements.



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

src/algebra/direct_sum/internal.lean

@@ -41,7 +41,10 @@ internally graded ring
 
 open_locale direct_sum big_operators
 
-variables {ι : Type*} {S R : Type*} [decidable_eq ι]
+variables {ι : Type*} {S R : Type*}
+
+section direct_sum
+variables [decidable_eq ι]
 
 /-! #### From `add_submonoid`s -/
 
@@ -203,3 +206,19 @@ 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
+
+end direct_sum
+
+section homogeneous_element
+
+lemma set_like.is_homogeneous_zero_submodule [has_zero ι]
+  [semiring S] [add_comm_monoid R] [module S R]
+  (A : ι → submodule S R) : set_like.is_homogeneous A (0 : R) :=
+⟨0, submodule.zero_mem _⟩
+
+lemma set_like.is_homogeneous.smul [comm_semiring S] [semiring R] [algebra S R]
+  {A : ι → submodule S R} {s : S}
+  {r : R} (hr : set_like.is_homogeneous A r) : set_like.is_homogeneous A (s • r) :=
+let ⟨i, hi⟩ := hr in ⟨i, submodule.smul_mem _ _ hi⟩
+
+end homogeneous_element

src/algebra/graded_monoid.lean

@@ -7,9 +7,10 @@ import algebra.group.inj_surj
 import data.list.big_operators
 import data.list.prod_monoid
 import data.list.range
+import group_theory.group_action.defs
+import group_theory.submonoid.basic
 import data.set_like.basic
 import data.sigma.basic
-import group_theory.group_action.defs
 
 /-!
 # Additively-graded multiplicative structures
@@ -64,13 +65,17 @@ provides the `Prop` typeclasses:
 * `set_like.has_graded_mul A` (which provides the obvious `graded_monoid.ghas_mul A` instance)
 * `set_like.graded_monoid A` (which provides the obvious `graded_monoid.gmonoid A` and
   `graded_monoid.gcomm_monoid A` instances)
+* `set_like.is_homogeneous A` (which says that `a` is homogeneous iff `a ∈ A i` for some `i : ι`)
 
 Strictly this last class is unecessary as it has no fields not present in its parents, but it is
 included for convenience. Note that there is no need for `graded_ring` or similar, as all the
 information it would contain is already supplied by `graded_monoid` when `A` is a collection
 of additively-closed set_like objects such as `submodules`. These constructions are explored in
 `algebra.direct_sum.internal`.
 
+This file also contains the definition of `set_like.homogeneous_submonoid A`, which is, as the name
+suggests, the submonoid consisting of all the homogeneous elements.
+
 ## tags
 
 graded monoid
@@ -505,3 +510,28 @@ subtype.ext $ set_like.coe_list_dprod _ _ _ _
 end dprod
 
 end subobjects
+
+section homogeneous_elements
+
+variables {R S : Type*} [set_like S R]
+
+/-- An element `a : R` is said to be homogeneous if there is some `i : ι` such that `a ∈ A i`. -/
+def set_like.is_homogeneous (A : ι → S) (a : R) : Prop := ∃ i, a ∈ A i
+
+lemma set_like.is_homogeneous_one [has_zero ι] [has_one R]
+  (A : ι → S) [set_like.has_graded_one A] : set_like.is_homogeneous A (1 : R) :=
+⟨0, set_like.has_graded_one.one_mem⟩
+
+lemma set_like.is_homogeneous.mul [has_add ι] [has_mul R] {A : ι → S}
+  [set_like.has_graded_mul A] {a b : R} :
+  set_like.is_homogeneous A a → set_like.is_homogeneous A b → set_like.is_homogeneous A (a * b)
+| ⟨i, hi⟩ ⟨j, hj⟩ := ⟨i + j, set_like.has_graded_mul.mul_mem hi hj⟩
+
+/-- When `A` is a `set_like.graded_monoid A`, then the homogeneous elements forms a submonoid. -/
+def set_like.homogeneous_submonoid [add_monoid ι] [monoid R]
+  (A : ι → S) [set_like.graded_monoid A] : submonoid R :=
+{ carrier := { a | set_like.is_homogeneous A a },
+  one_mem' := set_like.is_homogeneous_one A,
+  mul_mem' := λ a b, set_like.is_homogeneous.mul }
+
+end homogeneous_elements

src/ring_theory/graded_algebra/basic.lean

@@ -122,8 +122,7 @@ by rw [graded_algebra.decompose_of_mem _ hx, direct_sum.of_eq_of_ne _ _ _ _ hij,
 
 variable [Π (i : ι) (x : 𝒜 i), decidable (x ≠ 0)]
 
-lemma graded_algebra.mem_support_iff
-  (r : A) (i : ι) :
+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],