From efbbb767b2d953a930f9898cc9063c7718f69888 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 13 Dec 2021 15:33:25 +0000 Subject: [PATCH] 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 Co-authored-by: Eric Wieser --- src/algebra/direct_sum/internal.lean | 21 ++++++++++++++- src/algebra/graded_monoid.lean | 32 ++++++++++++++++++++++- src/ring_theory/graded_algebra/basic.lean | 3 +-- 3 files changed, 52 insertions(+), 4 deletions(-) diff --git a/src/algebra/direct_sum/internal.lean b/src/algebra/direct_sum/internal.lean index 23ef8cc141d6f..e0ca023d67fad 100644 --- a/src/algebra/direct_sum/internal.lean +++ b/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 diff --git a/src/algebra/graded_monoid.lean b/src/algebra/graded_monoid.lean index 3436aa1c6aee4..6c4f3b05c41e8 100644 --- a/src/algebra/graded_monoid.lean +++ b/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,6 +65,7 @@ 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 @@ -71,6 +73,9 @@ information it would contain is already supplied by `graded_monoid` when `A` is 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 diff --git a/src/ring_theory/graded_algebra/basic.lean b/src/ring_theory/graded_algebra/basic.lean index e61f7b0069e17..3aa60bdbe375f 100644 --- a/src/ring_theory/graded_algebra/basic.lean +++ b/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],