feat(RingTheory/GradedAlgebra): define homogeneous submodule (#18728)

and redefine homogeneous ideal as a homogeneous submodule

rename `SetLike.Homogeneous` to `SetLike.IsHomogeneousElem`
introduced `DirectSum.SetLike.Homogeneous` to mean a set $S$ is homogeneous iff for all $s \in S$, all of its projection $s_i \in S$ as well.



Co-authored-by: zjj <zjj@zjj>
Co-authored-by: Johan Commelin <johan@commelin.net>

Author: 3 people

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -6,7 +6,7 @@ Authors: Johan Commelin, Eric Wieser, Jujian Zhang
 import Mathlib.Algebra.Divisibility.Finite
 import Mathlib.Algebra.Divisibility.Prod
 import Mathlib.Data.Fintype.Units
-import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
+import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
 
 /-!
 # A homogeneous ideal that is homogeneously prime but not prime
@@ -138,8 +138,9 @@ theorem I_isHomogeneous : Ideal.IsHomogeneous (grading R) I := by
   rw [Set.image_singleton]
   rfl
 
+
 theorem homogeneous_mem_or_mem : ∀ {x y : R × R},
-    SetLike.Homogeneous (grading R) x → SetLike.Homogeneous (grading R) y →
+    SetLike.IsHomogeneousElem (grading R) x → SetLike.IsHomogeneousElem (grading R) y →
     x * y ∈ I → x ∈ I ∨ y ∈ I := by
   have h2 : Prime (2:R) := by
     unfold Prime

Mathlib.lean

@@ -4606,7 +4606,8 @@ import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.FreeRing
 import Mathlib.RingTheory.Generators
 import Mathlib.RingTheory.GradedAlgebra.Basic
-import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
+import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
+import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
 import Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
 import Mathlib.RingTheory.GradedAlgebra.Noetherian
 import Mathlib.RingTheory.GradedAlgebra.Radical

Mathlib/Algebra/DirectSum/Decomposition.lean

@@ -91,6 +91,12 @@ def decompose : M ≃ ⨁ i, ℳ i where
   left_inv := Decomposition.left_inv
   right_inv := Decomposition.right_inv
 
+omit [AddSubmonoidClass σ M] in
+/-- A substructure `p ⊆ M` is homogeneous if for every `m ∈ p`, all homogeneous components
+  of `m` are in `p`. -/
+def SetLike.IsHomogeneous {P : Type*} [SetLike P M] (p : P) : Prop :=
+  ∀ (i : ι) ⦃m : M⦄, m ∈ p → (DirectSum.decompose ℳ m i : M) ∈ p
+
 protected theorem Decomposition.inductionOn {p : M → Prop} (h_zero : p 0)
     (h_homogeneous : ∀ {i} (m : ℳ i), p (m : M)) (h_add : ∀ m m' : M, p m → p m' → p (m + m')) :
     ∀ m, p m := by
@@ -174,6 +180,15 @@ theorem sum_support_decompose [∀ (i) (x : ℳ i), Decidable (x ≠ 0)] (r : M)
   rw [decompose_symm_sum]
   simp_rw [decompose_symm_of]
 
+theorem AddSubmonoidClass.IsHomogeneous.mem_iff
+    {P : Type*} [SetLike P M] [AddSubmonoidClass P M] (p : P)
+    (hp : SetLike.IsHomogeneous ℳ p) {x} :
+    x ∈ p ↔ ∀ i, (decompose ℳ x i : M) ∈ p := by
+  classical
+  refine ⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩
+  rw [← DirectSum.sum_support_decompose ℳ x]
+  exact sum_mem (fun i _ ↦ hx i)
+
 end AddCommMonoid
 
 /-- The `-` in the statements below doesn't resolve without this line.

Mathlib/Algebra/DirectSum/Internal.lean

@@ -397,11 +397,11 @@ end SetLike.GradeZero
 section HomogeneousElement
 
 theorem SetLike.homogeneous_zero_submodule [Zero ι] [Semiring S] [AddCommMonoid R] [Module S R]
-    (A : ι → Submodule S R) : SetLike.Homogeneous A (0 : R) :=
+    (A : ι → Submodule S R) : SetLike.IsHomogeneousElem A (0 : R) :=
   ⟨0, Submodule.zero_mem _⟩
 
 theorem SetLike.Homogeneous.smul [CommSemiring S] [Semiring R] [Algebra S R] {A : ι → Submodule S R}
-    {s : S} {r : R} (hr : SetLike.Homogeneous A r) : SetLike.Homogeneous A (s • r) :=
+    {s : S} {r : R} (hr : SetLike.IsHomogeneousElem A r) : SetLike.IsHomogeneousElem A (s • r) :=
   let ⟨i, hi⟩ := hr
   ⟨i, Submodule.smul_mem _ _ hi⟩
 

Mathlib/Algebra/GradedMonoid.lean

@@ -80,7 +80,7 @@ in `Algebra.DirectSum.Internal`.
 
 This file also defines:
 
-* `SetLike.isHomogeneous A` (which says that `a` is homogeneous iff `a ∈ A i` for some `i : ι`)
+* `SetLike.IsHomogeneousElem A` (which says that `a` is homogeneous iff `a ∈ A i` for some `i : ι`)
 * `SetLike.homogeneousSubmonoid A`, which is, as the name suggests, the submonoid consisting of
   all the homogeneous elements.
 
@@ -649,27 +649,36 @@ section HomogeneousElements
 variable {R S : Type*} [SetLike S R]
 
 /-- An element `a : R` is said to be homogeneous if there is some `i : ι` such that `a ∈ A i`. -/
-def SetLike.Homogeneous (A : ι → S) (a : R) : Prop :=
+def SetLike.IsHomogeneousElem (A : ι → S) (a : R) : Prop :=
   ∃ i, a ∈ A i
 
 @[simp]
-theorem SetLike.homogeneous_coe {A : ι → S} {i} (x : A i) : SetLike.Homogeneous A (x : R) :=
+theorem SetLike.isHomogeneousElem_coe {A : ι → S} {i} (x : A i) :
+    SetLike.IsHomogeneousElem A (x : R) :=
   ⟨i, x.prop⟩
 
-theorem SetLike.homogeneous_one [Zero ι] [One R] (A : ι → S) [SetLike.GradedOne A] :
-    SetLike.Homogeneous A (1 : R) :=
+@[deprecated (since := "2025-01-31")] alias SetLike.homogeneous_coe :=
+  SetLike.isHomogeneousElem_coe
+
+theorem SetLike.isHomogeneousElem_one [Zero ι] [One R] (A : ι → S) [SetLike.GradedOne A] :
+    SetLike.IsHomogeneousElem A (1 : R) :=
   ⟨0, SetLike.one_mem_graded _⟩
 
-theorem SetLike.homogeneous_mul [Add ι] [Mul R] {A : ι → S} [SetLike.GradedMul A] {a b : R} :
-    SetLike.Homogeneous A a → SetLike.Homogeneous A b → SetLike.Homogeneous A (a * b)
+@[deprecated (since := "2025-01-31")] alias SetLike.homogeneous_one := SetLike.isHomogeneousElem_one
+
+theorem SetLike.IsHomogeneousElem.mul [Add ι] [Mul R] {A : ι → S} [SetLike.GradedMul A] {a b : R} :
+    SetLike.IsHomogeneousElem A a → SetLike.IsHomogeneousElem A b →
+    SetLike.IsHomogeneousElem A (a * b)
   | ⟨i, hi⟩, ⟨j, hj⟩ => ⟨i + j, SetLike.mul_mem_graded hi hj⟩
 
+@[deprecated (since := "2025-01-31")] alias SetLike.homogeneous_mul := SetLike.IsHomogeneousElem.mul
+
 /-- When `A` is a `SetLike.GradedMonoid A`, then the homogeneous elements forms a submonoid. -/
 def SetLike.homogeneousSubmonoid [AddMonoid ι] [Monoid R] (A : ι → S) [SetLike.GradedMonoid A] :
     Submonoid R where
-  carrier := { a | SetLike.Homogeneous A a }
-  one_mem' := SetLike.homogeneous_one A
-  mul_mem' a b := SetLike.homogeneous_mul a b
+  carrier := { a | SetLike.IsHomogeneousElem A a }
+  one_mem' := SetLike.isHomogeneousElem_one A
+  mul_mem' a b := SetLike.IsHomogeneousElem.mul a b
 
 end HomogeneousElements
 

Mathlib/Algebra/GradedMulAction.lean

@@ -129,9 +129,13 @@ section HomogeneousElements
 
 variable {S R N M : Type*} [SetLike S R] [SetLike N M]
 
-theorem SetLike.Homogeneous.graded_smul [VAdd ιA ιB] [SMul R M] {A : ιA → S} {B : ιB → N}
+theorem SetLike.IsHomogeneousElem.graded_smul [VAdd ιA ιB] [SMul R M] {A : ιA → S} {B : ιB → N}
     [SetLike.GradedSMul A B] {a : R} {b : M} :
-    SetLike.Homogeneous A a → SetLike.Homogeneous B b → SetLike.Homogeneous B (a • b)
+    SetLike.IsHomogeneousElem A a → SetLike.IsHomogeneousElem B b →
+    SetLike.IsHomogeneousElem B (a • b)
   | ⟨i, hi⟩, ⟨j, hj⟩ => ⟨i +ᵥ j, SetLike.GradedSMul.smul_mem hi hj⟩
 
+@[deprecated (since := "2025-01-31")] alias SetLike.Homogeneous.graded_smul :=
+  SetLike.IsHomogeneousElem.graded_smul
+
 end HomogeneousElements

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Johan Commelin
 -/
-import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
+import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
 import Mathlib.Topology.Category.TopCat.Basic
 import Mathlib.Topology.Sets.Opens
 import Mathlib.Data.Set.Subsingleton
@@ -56,6 +56,8 @@ attribute [instance] ProjectiveSpectrum.isPrime
 
 namespace ProjectiveSpectrum
 
+instance (x : ProjectiveSpectrum 𝒜) : Ideal.IsPrime x.asHomogeneousIdeal.toIdeal := x.isPrime
+
 /-- The zero locus of a set `s` of elements of a commutative ring `A` is the set of all relevant
 homogeneous prime ideals of the ring that contain the set `s`.
 

Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean renamed to Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean

@@ -8,6 +8,7 @@ import Mathlib.RingTheory.GradedAlgebra.Basic
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Ideal.BigOperators
 import Mathlib.RingTheory.Ideal.Maps
+import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
 
 /-!
 # Homogeneous ideals of a graded algebra
@@ -56,49 +57,39 @@ variable (I : Ideal A)
 
 /-- An `I : Ideal A` is homogeneous if for every `r ∈ I`, all homogeneous components
   of `r` are in `I`. -/
-def Ideal.IsHomogeneous : Prop :=
-  ∀ (i : ι) ⦃r : A⦄, r ∈ I → (DirectSum.decompose 𝒜 r i : A) ∈ I
+abbrev Ideal.IsHomogeneous : Prop := Submodule.IsHomogeneous I 𝒜
 
 theorem Ideal.IsHomogeneous.mem_iff {I} (hI : Ideal.IsHomogeneous 𝒜 I) {x} :
-    x ∈ I ↔ ∀ i, (decompose 𝒜 x i : A) ∈ I := by
-  classical
-  refine ⟨fun hx i ↦ hI i hx, fun hx ↦ ?_⟩
-  rw [← DirectSum.sum_support_decompose 𝒜 x]
-  exact Ideal.sum_mem _ (fun i _ ↦ hx i)
+    x ∈ I ↔ ∀ i, (decompose 𝒜 x i : A) ∈ I :=
+  AddSubmonoidClass.IsHomogeneous.mem_iff 𝒜 _ hI
 
 /-- For any `Semiring A`, we collect the homogeneous ideals of `A` into a type. -/
-structure HomogeneousIdeal extends Submodule A A where
-  is_homogeneous' : Ideal.IsHomogeneous 𝒜 toSubmodule
+abbrev HomogeneousIdeal := HomogeneousSubmodule 𝒜 𝒜
 
 variable {𝒜}
 
 /-- Converting a homogeneous ideal to an ideal. -/
-def HomogeneousIdeal.toIdeal (I : HomogeneousIdeal 𝒜) : Ideal A :=
+abbrev HomogeneousIdeal.toIdeal (I : HomogeneousIdeal 𝒜) : Ideal A :=
   I.toSubmodule
 
-theorem HomogeneousIdeal.isHomogeneous (I : HomogeneousIdeal 𝒜) : I.toIdeal.IsHomogeneous 𝒜 :=
-  I.is_homogeneous'
+theorem HomogeneousIdeal.isHomogeneous (I : HomogeneousIdeal 𝒜) :
+    I.toIdeal.IsHomogeneous 𝒜 := I.is_homogeneous'
 
 theorem HomogeneousIdeal.toIdeal_injective :
     Function.Injective (HomogeneousIdeal.toIdeal : HomogeneousIdeal 𝒜 → Ideal A) :=
-  fun ⟨x, hx⟩ ⟨y, hy⟩ => fun (h : x = y) => by simp [h]
+  HomogeneousSubmodule.toSubmodule_injective 𝒜 𝒜
 
-instance HomogeneousIdeal.setLike : SetLike (HomogeneousIdeal 𝒜) A where
-  coe I := I.toIdeal
-  coe_injective' _ _ h := HomogeneousIdeal.toIdeal_injective <| SetLike.coe_injective h
+instance HomogeneousIdeal.setLike : SetLike (HomogeneousIdeal 𝒜) A :=
+  HomogeneousSubmodule.setLike 𝒜 𝒜
 
 @[ext]
 theorem HomogeneousIdeal.ext {I J : HomogeneousIdeal 𝒜} (h : I.toIdeal = J.toIdeal) : I = J :=
   HomogeneousIdeal.toIdeal_injective h
 
 theorem HomogeneousIdeal.ext' {I J : HomogeneousIdeal 𝒜} (h : ∀ i, ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J) :
-    I = J := by
-  ext
-  rw [I.isHomogeneous.mem_iff, J.isHomogeneous.mem_iff]
-  apply forall_congr'
-  exact fun i ↦ h i _ (decompose 𝒜 _ i).2
+    I = J := HomogeneousSubmodule.ext' 𝒜 𝒜 h
 
-@[simp]
+@[simp high]
 theorem HomogeneousIdeal.mem_iff {I : HomogeneousIdeal 𝒜} {x : A} : x ∈ I.toIdeal ↔ x ∈ I :=
   Iff.rfl
 
@@ -113,7 +104,7 @@ variable (I : Ideal A)
 /-- For any `I : Ideal A`, not necessarily homogeneous, `I.homogeneousCore' 𝒜`
 is the largest homogeneous ideal of `A` contained in `I`, as an ideal. -/
 def Ideal.homogeneousCore' (I : Ideal A) : Ideal A :=
-  Ideal.span ((↑) '' (((↑) : Subtype (Homogeneous 𝒜) → A) ⁻¹' I))
+  Ideal.span ((↑) '' (((↑) : Subtype (SetLike.IsHomogeneousElem 𝒜) → A) ⁻¹' I))
 
 theorem Ideal.homogeneousCore'_mono : Monotone (Ideal.homogeneousCore' 𝒜) :=
   fun _ _ I_le_J => Ideal.span_mono <| Set.image_subset _ fun _ => @I_le_J _
@@ -138,7 +129,8 @@ theorem Ideal.isHomogeneous_iff_subset_iInter :
     I.IsHomogeneous 𝒜 ↔ (I : Set A) ⊆ ⋂ i, GradedRing.proj 𝒜 i ⁻¹' ↑I :=
   subset_iInter_iff.symm
 
-theorem Ideal.mul_homogeneous_element_mem_of_mem {I : Ideal A} (r x : A) (hx₁ : Homogeneous 𝒜 x)
+theorem Ideal.mul_homogeneous_element_mem_of_mem
+    {I : Ideal A} (r x : A) (hx₁ : SetLike.IsHomogeneousElem 𝒜 x)
     (hx₂ : x ∈ I) (j : ι) : GradedRing.proj 𝒜 j (r * x) ∈ I := by
   classical
   rw [← DirectSum.sum_support_decompose 𝒜 r, Finset.sum_mul, map_sum]
@@ -152,7 +144,7 @@ theorem Ideal.mul_homogeneous_element_mem_of_mem {I : Ideal A} (r x : A) (hx₁
   · exact I.mul_mem_left _ hx₂
   · exact I.zero_mem
 
-theorem Ideal.homogeneous_span (s : Set A) (h : ∀ x ∈ s, Homogeneous 𝒜 x) :
+theorem Ideal.homogeneous_span (s : Set A) (h : ∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x) :
     (Ideal.span s).IsHomogeneous 𝒜 := by
   rintro i r hr
   rw [Ideal.span, Finsupp.span_eq_range_linearCombination] at hr
@@ -173,7 +165,7 @@ is the largest homogeneous ideal of `A` contained in `I`. -/
 def Ideal.homogeneousCore : HomogeneousIdeal 𝒜 :=
   ⟨Ideal.homogeneousCore' 𝒜 I,
     Ideal.homogeneous_span _ _ fun _ h => by
-      have := Subtype.image_preimage_coe (setOf (Homogeneous 𝒜)) (I : Set A)
+      have := Subtype.image_preimage_coe (setOf (SetLike.IsHomogeneousElem 𝒜)) (I : Set A)
       exact (cast congr(_ ∈ $this) h).1⟩
 
 theorem Ideal.homogeneousCore_mono : Monotone (Ideal.homogeneousCore 𝒜) :=
@@ -184,7 +176,7 @@ theorem Ideal.toIdeal_homogeneousCore_le : (I.homogeneousCore 𝒜).toIdeal ≤
 
 variable {𝒜 I}
 
-theorem Ideal.mem_homogeneousCore_of_homogeneous_of_mem {x : A} (h : SetLike.Homogeneous 𝒜 x)
+theorem Ideal.mem_homogeneousCore_of_homogeneous_of_mem {x : A} (h : SetLike.IsHomogeneousElem 𝒜 x)
     (hmem : x ∈ I) : x ∈ I.homogeneousCore 𝒜 :=
   Ideal.subset_span ⟨⟨x, h⟩, hmem, rfl⟩
 
@@ -194,7 +186,7 @@ theorem Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self (h : I.IsHomogeneous
   intro x hx
   classical
   rw [← DirectSum.sum_support_decompose 𝒜 x]
-  exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, homogeneous_coe _⟩, h _ hx, rfl⟩
+  exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, rfl⟩
 
 @[simp]
 theorem HomogeneousIdeal.toIdeal_homogeneousCore_eq_self (I : HomogeneousIdeal 𝒜) :
@@ -481,7 +473,7 @@ def Ideal.homogeneousHull : HomogeneousIdeal 𝒜 :=
   ⟨Ideal.span { r : A | ∃ (i : ι) (x : I), (DirectSum.decompose 𝒜 (x : A) i : A) = r }, by
     refine Ideal.homogeneous_span _ _ fun x hx => ?_
     obtain ⟨i, x, rfl⟩ := hx
-    apply SetLike.homogeneous_coe⟩
+    apply SetLike.isHomogeneousElem_coe⟩
 
 theorem Ideal.le_toIdeal_homogeneousHull : I ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal := by
   intro r hr
@@ -526,10 +518,9 @@ theorem Ideal.homogeneousHull_eq_iSup :
     I.homogeneousHull 𝒜 =
       ⨆ i, ⟨Ideal.span (GradedRing.proj 𝒜 i '' I), Ideal.homogeneous_span 𝒜 _ (by
         rintro _ ⟨x, -, rfl⟩
-        apply SetLike.homogeneous_coe)⟩ := by
+        apply SetLike.isHomogeneousElem_coe)⟩ := by
   ext1
   rw [Ideal.toIdeal_homogeneousHull_eq_iSup, toIdeal_iSup]
-  rfl
 
 end HomogeneousHull