feat(ring_theory/graded_algebra/homogeneous_ideal): definition of irr…

…elevant ideal of a graded algebra (#12548)

For an `ℕ`-graded ring `⨁ᵢ 𝒜ᵢ`, the irrelevant ideal refers to `⨁_{i>0} 𝒜ᵢ`.

This construction is used in the Proj construction in algebraic geometry.

src/ring_theory/graded_algebra/basic.lean

@@ -138,7 +138,6 @@ lemma graded_algebra.decompose_of_mem_ne {x : A} {i j : ι} (hx : x ∈ 𝒜 i)
   (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 : ι) :
@@ -158,3 +157,44 @@ begin
 end
 
 end graded_algebra
+
+section canonical_order
+
+open graded_algebra set_like.graded_monoid direct_sum
+
+variables {ι R A : Type*}
+variables [comm_semiring R] [semiring A]
+variables [algebra R A] [decidable_eq ι]
+variables [canonically_ordered_add_monoid ι]
+variables (𝒜 : ι → submodule R A) [graded_algebra 𝒜]
+
+/--
+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 :=
+{ to_fun := λ a, decompose 𝒜 a 0,
+  map_one' := decompose_of_mem_same 𝒜 one_mem,
+  map_zero' := by simp only [subtype.ext_iff_val, map_zero, zero_apply, submodule.coe_zero],
+  map_add' := λ _ _, by simp [subtype.ext_iff_val, map_add, add_apply, submodule.coe_add],
+  map_mul' := λ x y,
+    have m : ∀ x, x ∈ supr 𝒜, from λ x, (is_internal 𝒜).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', _) _ _,
+      { 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),
+            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0, from (add_eq_zero_iff.mp h).2 ▸ hc')] },
+        { rw [decompose_of_mem_ne 𝒜 (mul_mem hc hc') h],
+          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 [map_zero, zero_apply, submodule.coe_zero, mul_zero] },
+      { intros _ _ hd he, simp only [mul_add, map_add, add_apply, submodule.coe_add, hd, he] } },
+    { simp only [map_zero, zero_apply, submodule.coe_zero, zero_mul] },
+    { rintros _ _ ha hb, simp only [add_mul, map_add, add_apply, submodule.coe_add, ha, hb] },
+  end }
+
+end canonical_order

src/ring_theory/graded_algebra/homogeneous_ideal.lean

@@ -3,12 +3,10 @@ Copyright (c) 2021 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Eric Wieser
 -/
-
 import ring_theory.ideal.basic
 import ring_theory.ideal.operations
 import linear_algebra.finsupp
 import ring_theory.graded_algebra.basic
-
 /-!
 # Homogeneous ideals of a graded algebra
 
@@ -471,3 +469,39 @@ lemma ideal.homogeneous_hull_eq_Inf (I : ideal A) :
 eq.symm $ is_glb.Inf_eq $ (ideal.homogeneous_hull.gc 𝒜).is_least_l.is_glb
 
 end galois_connection
+
+section irrelevant_ideal
+
+variables [comm_semiring R] [semiring A]
+variables [algebra R A] [decidable_eq ι]
+variables [canonically_ordered_add_monoid ι]
+variables (𝒜 : ι → submodule R A) [graded_algebra 𝒜]
+
+open graded_algebra set_like.graded_monoid direct_sum
+
+/--
+For a graded ring `⨁ᵢ 𝒜ᵢ` graded by a `canonically_ordered_add_monoid ι`, the irrelevant ideal
+refers to `⨁_{i>0} 𝒜ᵢ`, or equivalently `{a | a₀ = 0}`. This definition is used in `Proj`
+construction where `ι` is always `ℕ` so the irrelevant ideal is simply elements with `0` as
+0-th coordinate.
+
+# Future work
+Here in the definition, `ι` is assumed to be `canonically_ordered_add_monoid`. However, the notion
+of irrelevant ideal makes sense in a more general setting by defining it as the ideal of elements
+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
+  change (decompose 𝒜 (decompose 𝒜 r _) 0 : A) = 0,
+  by_cases h : i = 0,
+  { rw [h, hr, map_zero, zero_apply, submodule.coe_zero] },
+  { rw [decompose_of_mem_ne 𝒜 (submodule.coe_mem _) h] }
+end⟩
+
+@[simp] lemma homogeneous_ideal.mem_irrelevant_iff (a : A) :
+  a ∈ homogeneous_ideal.irrelevant 𝒜 ↔ proj 𝒜 0 a = 0 := iff.rfl
+
+@[simp, norm_cast] lemma homogeneous_ideal.coe_irrelevant :
+  ↑(homogeneous_ideal.irrelevant 𝒜) = (graded_algebra.proj_zero_ring_hom 𝒜).ker := rfl
+
+end irrelevant_ideal