From a2a8c9be9292ab6a2813ac5ceebb53fb74313a7a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 29 Jun 2022 22:22:05 +0000 Subject: [PATCH] refactor(ring_theory/graded_algebra): use `add_submonoid_class` to generalize 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 --- src/algebra/direct_sum/internal.lean | 4 +- .../clifford_algebra/grading.lean | 5 +- src/ring_theory/graded_algebra/basic.lean | 127 +++++++++++++----- .../graded_algebra/homogeneous_ideal.lean | 96 ++++++------- src/ring_theory/graded_algebra/radical.lean | 11 +- 5 files changed, 151 insertions(+), 92 deletions(-) diff --git a/src/algebra/direct_sum/internal.lean b/src/algebra/direct_sum/internal.lean index 0afd18f4921cd..d7ba46b643318 100644 --- a/src/algebra/direct_sum/internal.lean +++ b/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 _ _ _ _ _ diff --git a/src/linear_algebra/clifford_algebra/grading.lean b/src/linear_algebra/clifford_algebra/grading.lean index cb7ae3dcb67bc..7f4e78aef4f9c 100644 --- a/src/linear_algebra/clifford_algebra/grading.lean +++ b/src/linear_algebra/clifford_algebra/grading.lean @@ -123,8 +123,7 @@ 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) @@ -132,7 +131,7 @@ begin 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 diff --git a/src/ring_theory/graded_algebra/basic.lean b/src/ring_theory/graded_algebra/basic.lean index 9decc67eec748..ae34e467f49e6 100644 --- a/src/ring_theory/graded_algebra/basic.lean +++ b/src/ring_theory/graded_algebra/basic.lean @@ -10,7 +10,7 @@ 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`. @@ -18,8 +18,11 @@ 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 diff --git a/src/ring_theory/graded_algebra/homogeneous_ideal.lean b/src/ring_theory/graded_algebra/homogeneous_ideal.lean index a5023af9bbadd..f4676a719003e 100644 --- a/src/ring_theory/graded_algebra/homogeneous_ideal.lean +++ b/src/ring_theory/graded_algebra/homogeneous_ideal.lean @@ -10,13 +10,13 @@ import ring_theory.graded_algebra.basic /-! # Homogeneous ideals of a graded algebra -This file defines homogeneous ideals of `graded_algebra 𝒜` where `𝒜 : ι → submodule R A` and +This file defines homogeneous ideals of `graded_ring 𝒜` where `𝒜 : ι → submodule R A` and operations on them. ## Main definitions For any `I : ideal A`: -* `ideal.is_homogeneous 𝒜 I`: The property that an ideal is closed under `graded_algebra.proj`. +* `ideal.is_homogeneous 𝒜 I`: The property that an ideal is closed under `graded_ring.proj`. * `homogeneous_ideal 𝒜`: The structure extending ideals which satisfy `ideal.is_homogeneous` * `ideal.homogeneous_core I 𝒜`: The largest homogeneous ideal smaller than `I`. * `ideal.homogeneous_hull I 𝒜`: The smallest homogeneous ideal larger than `I`. @@ -41,14 +41,15 @@ graded algebra, homogeneous open set_like direct_sum set open_locale big_operators pointwise direct_sum -variables {ι R A : Type*} +variables {ι σ R A : Type*} section homogeneous_def -variables [comm_semiring R] [semiring A] [algebra R A] -variables (𝒜 : ι → submodule R A) -variables [decidable_eq ι] [add_monoid ι] [graded_algebra 𝒜] +variables [semiring A] +variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) +variables [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] variable (I : ideal A) +include A /--An `I : ideal A` is homogeneous if for every `r ∈ I`, all homogeneous components of `r` are in `I`.-/ @@ -84,13 +85,14 @@ end homogeneous_def section homogeneous_core -variables [comm_semiring R] [semiring A] [algebra R A] -variables (𝒜 : ι → submodule R A) +variables [semiring A] +variables [set_like σ A] (𝒜 : ι → σ) variable (I : ideal A) +include A /-- For any `I : ideal A`, not necessarily homogeneous, `I.homogeneous_core' 𝒜` is the largest homogeneous ideal of `A` contained in `I`, as an ideal. -/ -def ideal.homogeneous_core' : ideal A := +def ideal.homogeneous_core' (I : ideal A) : ideal A := ideal.span (coe '' ((coe : subtype (is_homogeneous 𝒜) → A) ⁻¹' I)) lemma ideal.homogeneous_core'_mono : monotone (ideal.homogeneous_core' 𝒜) := @@ -103,32 +105,33 @@ end homogeneous_core section is_homogeneous_ideal_defs -variables [comm_semiring R] [semiring A] [algebra R A] -variables (𝒜 : ι → submodule R A) -variables [decidable_eq ι] [add_monoid ι] [graded_algebra 𝒜] +variables [semiring A] +variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) +variables [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] variable (I : ideal A) +include A lemma ideal.is_homogeneous_iff_forall_subset : - I.is_homogeneous 𝒜 ↔ ∀ i, (I : set A) ⊆ graded_algebra.proj 𝒜 i ⁻¹' I := + I.is_homogeneous 𝒜 ↔ ∀ i, (I : set A) ⊆ graded_ring.proj 𝒜 i ⁻¹' I := iff.rfl lemma ideal.is_homogeneous_iff_subset_Inter : - I.is_homogeneous 𝒜 ↔ (I : set A) ⊆ ⋂ i, graded_algebra.proj 𝒜 i ⁻¹' ↑I := + I.is_homogeneous 𝒜 ↔ (I : set A) ⊆ ⋂ i, graded_ring.proj 𝒜 i ⁻¹' ↑I := subset_Inter_iff.symm lemma ideal.mul_homogeneous_element_mem_of_mem {I : ideal A} (r x : A) (hx₁ : is_homogeneous 𝒜 x) (hx₂ : x ∈ I) (j : ι) : - graded_algebra.proj 𝒜 j (r * x) ∈ I := + graded_ring.proj 𝒜 j (r * x) ∈ I := begin classical, - rw [←direct_sum.sum_support_decompose 𝒜 r, finset.sum_mul, linear_map.map_sum], + rw [←direct_sum.sum_support_decompose 𝒜 r, finset.sum_mul, map_sum], apply ideal.sum_mem, intros k hk, obtain ⟨i, hi⟩ := hx₁, have mem₁ : (direct_sum.decompose 𝒜 r k : A) * x ∈ 𝒜 (k + i) := graded_monoid.mul_mem - (submodule.coe_mem _) hi, - erw [graded_algebra.proj_apply, direct_sum.decompose_of_mem 𝒜 mem₁, - coe_of_apply, submodule.coe_mk], + (set_like.coe_mem _) hi, + erw [graded_ring.proj_apply, direct_sum.decompose_of_mem 𝒜 mem₁, + coe_of_apply, set_like.coe_mk], split_ifs, { exact I.mul_mem_left _ hx₂ }, { exact I.zero_mem }, @@ -141,7 +144,8 @@ begin rw [ideal.span, finsupp.span_eq_range_total] at hr, rw linear_map.mem_range at hr, obtain ⟨s, rfl⟩ := hr, - rw [←graded_algebra.proj_apply, finsupp.total_apply, finsupp.sum, linear_map.map_sum], + rw [finsupp.total_apply, finsupp.sum, decompose_sum, dfinsupp.finset_sum_apply, + add_submonoid_class.coe_finset_sum], refine ideal.sum_mem _ _, rintros z hz1, rw [smul_eq_mul], @@ -207,9 +211,9 @@ section operations section semiring -variables [comm_semiring R] [semiring A] [algebra R A] -variables [decidable_eq ι] [add_monoid ι] -variables (𝒜 : ι → submodule R A) [graded_algebra 𝒜] +variables [semiring A] [decidable_eq ι] [add_monoid ι] +variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] +include A namespace ideal.is_homogeneous @@ -352,10 +356,11 @@ end homogeneous_ideal end semiring section comm_semiring -variables [comm_semiring R] [comm_semiring A] [algebra R A] +variables [comm_semiring A] variables [decidable_eq ι] [add_monoid ι] -variables {𝒜 : ι → submodule R A} [graded_algebra 𝒜] +variables [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] variable (I : ideal A) +include A lemma ideal.is_homogeneous.mul {I J : ideal A} (HI : I.is_homogeneous 𝒜) (HJ : J.is_homogeneous 𝒜) : (I * J).is_homogeneous 𝒜 := @@ -387,10 +392,10 @@ section homogeneous_core open homogeneous_ideal -variables [comm_semiring R] [semiring A] -variables [algebra R A] [decidable_eq ι] [add_monoid ι] -variables (𝒜 : ι → submodule R A) [graded_algebra 𝒜] +variables [semiring A] [decidable_eq ι] [add_monoid ι] +variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] variable (I : ideal A) +include A lemma ideal.homogeneous_core.gc : galois_connection to_ideal (ideal.homogeneous_core 𝒜) := λ I J, ⟨ @@ -430,10 +435,10 @@ section homogeneous_hull open homogeneous_ideal -variables [comm_semiring R] [semiring A] -variables [algebra R A] [decidable_eq ι] [add_monoid ι] -variables (𝒜 : ι → submodule R A) [graded_algebra 𝒜] +variables [semiring A] [decidable_eq ι] [add_monoid ι] +variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] variable (I : ideal A) +include A /--For any `I : ideal A`, not necessarily homogeneous, `I.homogeneous_hull 𝒜` is the smallest homogeneous ideal containing `I`. -/ @@ -479,18 +484,18 @@ homogeneous_ideal.to_ideal_injective $ I.is_homogeneous.to_ideal_homogeneous_hul variables (I 𝒜) lemma ideal.to_ideal_homogeneous_hull_eq_supr : - (I.homogeneous_hull 𝒜).to_ideal = ⨆ i, ideal.span (graded_algebra.proj 𝒜 i '' I) := + (I.homogeneous_hull 𝒜).to_ideal = ⨆ i, ideal.span (graded_ring.proj 𝒜 i '' I) := begin rw ←ideal.span_Union, apply congr_arg ideal.span _, ext1, - simp only [set.mem_Union, set.mem_image, mem_set_of_eq, graded_algebra.proj_apply, + simp only [set.mem_Union, set.mem_image, mem_set_of_eq, graded_ring.proj_apply, set_like.exists, exists_prop, subtype.coe_mk, set_like.mem_coe], end lemma ideal.homogeneous_hull_eq_supr : (I.homogeneous_hull 𝒜) = - ⨆ i, ⟨ideal.span (graded_algebra.proj 𝒜 i '' I), ideal.is_homogeneous_span 𝒜 _ + ⨆ i, ⟨ideal.span (graded_ring.proj 𝒜 i '' I), ideal.is_homogeneous_span 𝒜 _ (by {rintros _ ⟨x, -, rfl⟩, apply set_like.is_homogeneous_coe})⟩ := by { ext1, rw [ideal.to_ideal_homogeneous_hull_eq_supr, to_ideal_supr], refl } @@ -500,9 +505,9 @@ section galois_connection open homogeneous_ideal -variables [comm_semiring R] [semiring A] -variables [algebra R A] [decidable_eq ι] [add_monoid ι] -variables (𝒜 : ι → submodule R A) [graded_algebra 𝒜] +variables [semiring A] [decidable_eq ι] [add_monoid ι] +variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] +include A lemma ideal.homogeneous_hull.gc : galois_connection (ideal.homogeneous_hull 𝒜) to_ideal := λ I J, ⟨ @@ -525,12 +530,13 @@ end galois_connection section irrelevant_ideal -variables [comm_semiring R] [semiring A] -variables [algebra R A] [decidable_eq ι] +variables [semiring A] +variables [decidable_eq ι] variables [canonically_ordered_add_monoid ι] -variables (𝒜 : ι → submodule R A) [graded_algebra 𝒜] +variables [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜] +include A -open graded_algebra set_like.graded_monoid direct_sum +open graded_ring set_like.graded_monoid direct_sum /-- For a graded ring `⨁ᵢ 𝒜ᵢ` graded by a `canonically_ordered_add_monoid ι`, the irrelevant ideal @@ -544,17 +550,17 @@ of irrelevant ideal makes sense in a more general setting by defining it as the with `0` as i-th coordinate for all `i ≤ 0`, i.e. `{a | ∀ (i : ι), i ≤ 0 → aᵢ = 0}`. -/ def homogeneous_ideal.irrelevant : homogeneous_ideal 𝒜 := -⟨(graded_algebra.proj_zero_ring_hom 𝒜).ker, λ i r (hr : (decompose 𝒜 r 0 : A) = 0), begin +⟨(graded_ring.proj_zero_ring_hom 𝒜).ker, λ i r (hr : (decompose 𝒜 r 0 : A) = 0), begin change (decompose 𝒜 (decompose 𝒜 r _ : A) 0 : A) = 0, by_cases h : i = 0, - { rw [h, hr, decompose_zero, zero_apply, submodule.coe_zero] }, - { rw [decompose_of_mem_ne 𝒜 (submodule.coe_mem _) h] } + { rw [h, hr, decompose_zero, zero_apply, add_submonoid_class.coe_zero] }, + { rw [decompose_of_mem_ne 𝒜 (set_like.coe_mem _) h] } end⟩ @[simp] lemma homogeneous_ideal.mem_irrelevant_iff (a : A) : a ∈ homogeneous_ideal.irrelevant 𝒜 ↔ proj 𝒜 0 a = 0 := iff.rfl @[simp] lemma homogeneous_ideal.to_ideal_irrelevant : - (homogeneous_ideal.irrelevant 𝒜).to_ideal = (graded_algebra.proj_zero_ring_hom 𝒜).ker := rfl + (homogeneous_ideal.irrelevant 𝒜).to_ideal = (graded_ring.proj_zero_ring_hom 𝒜).ker := rfl end irrelevant_ideal diff --git a/src/ring_theory/graded_algebra/radical.lean b/src/ring_theory/graded_algebra/radical.lean index 9f737cf75aa82..f8935fb7c04cc 100644 --- a/src/ring_theory/graded_algebra/radical.lean +++ b/src/ring_theory/graded_algebra/radical.lean @@ -34,13 +34,14 @@ fails for a non-cancellative set see `counterexample/homogeneous_prime_not_prime homogeneous, radical -/ -open graded_algebra direct_sum set_like finset +open graded_ring direct_sum set_like finset open_locale big_operators -variables {ι R A : Type*} -variables [comm_semiring R] [comm_ring A] [algebra R A] +variables {ι σ A : Type*} +variables [comm_ring A] variables [linear_ordered_cancel_add_comm_monoid ι] -variables {𝒜 : ι → submodule R A} [graded_algebra 𝒜] +variables [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] +include A lemma ideal.is_homogeneous.is_prime_of_homogeneous_mem_or_mem {I : ideal A} (hI : I.is_homogeneous 𝒜) (I_ne_top : I ≠ ⊤) @@ -129,7 +130,7 @@ lemma ideal.is_homogeneous.is_prime_of_homogeneous_mem_or_mem { rw mem_filter at mem_max₁ mem_max₂, exact ⟨mem_max₁.2, mem_max₂.2⟩, }, intro rid, - cases homogeneous_mem_or_mem ⟨max₁, submodule.coe_mem _⟩ ⟨max₂, submodule.coe_mem _⟩ mem_I, + cases homogeneous_mem_or_mem ⟨max₁, set_like.coe_mem _⟩ ⟨max₂, set_like.coe_mem _⟩ mem_I, { apply neither_mem.1 h }, { apply neither_mem.2 h }, },