From 3b415f232fadd167576b900c9b4a6a5026617d3b Mon Sep 17 00:00:00 2001 From: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Mon, 22 May 2023 17:42:43 +0000 Subject: [PATCH] feat: port RingTheory.GradedAlgebra.Radical (#4223) There is a long proof in this file that needs `maxHeartbeats 300000` to complete --- Mathlib.lean | 1 + Mathlib/RingTheory/GradedAlgebra/Radical.lean | 196 ++++++++++++++++++ 2 files changed, 197 insertions(+) create mode 100644 Mathlib/RingTheory/GradedAlgebra/Radical.lean diff --git a/Mathlib.lean b/Mathlib.lean index d64376b0961f5..0af00223fd709 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1903,6 +1903,7 @@ import Mathlib.RingTheory.FreeRing import Mathlib.RingTheory.GradedAlgebra.Basic import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal import Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization +import Mathlib.RingTheory.GradedAlgebra.Radical import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Ideal.IdempotentFG diff --git a/Mathlib/RingTheory/GradedAlgebra/Radical.lean b/Mathlib/RingTheory/GradedAlgebra/Radical.lean new file mode 100644 index 0000000000000..8c5bb85ad97b1 --- /dev/null +++ b/Mathlib/RingTheory/GradedAlgebra/Radical.lean @@ -0,0 +1,196 @@ +/- +Copyright (c) 2022 Jujian Zhang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jujian Zhang, Eric Wieser + +! This file was ported from Lean 3 source module ring_theory.graded_algebra.radical +! leanprover-community/mathlib commit f1944b30c97c5eb626e498307dec8b022a05bd0a +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal + +/-! + +This file contains a proof that the radical of any homogeneous ideal is a homogeneous ideal + +## Main statements + +* `Ideal.IsHomogeneous.isPrime_iff`: for any `I : Ideal A`, if `I` is homogeneous, then + `I` is prime if and only if `I` is homogeneously prime, i.e. `I ≠ ⊤` and if `x, y` are + homogeneous elements such that `x * y ∈ I`, then at least one of `x,y` is in `I`. +* `Ideal.IsPrime.homogeneousCore`: for any `I : Ideal A`, if `I` is prime, then + `I.homogeneous_core 𝒜` (i.e. the largest homogeneous ideal contained in `I`) is also prime. +* `Ideal.IsHomogeneous.radical`: for any `I : Ideal A`, if `I` is homogeneous, then the + radical of `I` is homogeneous as well. +* `HomogeneousIdeal.radical`: for any `I : HomogeneousIdeal 𝒜`, `I.radical` is the the + radical of `I` as a `HomogeneousIdeal 𝒜` + +## Implementation details + +Throughout this file, the indexing type `ι` of grading is assumed to be a +`LinearOrderedCancelAddCommMonoid`. This might be stronger than necessary but cancelling +property is strictly necessary; for a counterexample of how `Ideal.IsHomogeneous.isPrime_iff` +fails for a non-cancellative set see `counterexample/homogeneous_prime_not_prime.lean`. + +## Tags + +homogeneous, radical +-/ + + +open GradedRing DirectSum SetLike Finset + +open BigOperators + +variable {ι σ A : Type _} + +variable [CommRing A] + +variable [LinearOrderedCancelAddCommMonoid ι] + +variable [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] + +set_option maxHeartbeats 300000 in -- Porting note: This proof needs a long time to elaborate +theorem Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem {I : Ideal A} (hI : I.IsHomogeneous 𝒜) + (I_ne_top : I ≠ ⊤) + (homogeneous_mem_or_mem : + ∀ {x y : A}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I) : + Ideal.IsPrime I := + ⟨I_ne_top, by + intro x y hxy + by_contra rid + push_neg at rid + obtain ⟨rid₁, rid₂⟩ := rid + classical + /- + The idea of the proof is the following : + since `x * y ∈ I` and `I` homogeneous, then `proj i (x * y) ∈ I` for any `i : ι`. + Then consider two sets `{i ∈ x.support | xᵢ ∉ I}` and `{j ∈ y.support | yⱼ ∉ J}`; + let `max₁, max₂` be the maximum of the two sets, then `proj (max₁ + max₂) (x * y) ∈ I`. + Then, `proj max₁ x ∉ I` and `proj max₂ j ∉ I` + but `proj i x ∈ I` for all `max₁ < i` and `proj j y ∈ I` for all `max₂ < j`. + ` proj (max₁ + max₂) (x * y)` + `= ∑ {(i, j) ∈ supports | i + j = max₁ + max₂}, xᵢ * yⱼ` + `= proj max₁ x * proj max₂ y` + ` + ∑ {(i, j) ∈ supports \ {(max₁, max₂)} | i + j = max₁ + max₂}, xᵢ * yⱼ`. + This is a contradiction, because both `proj (max₁ + max₂) (x * y) ∈ I` and the sum on the + right hand side is in `I` however `proj max₁ x * proj max₂ y` is not in `I`. + -/ + set set₁ := (decompose 𝒜 x).support.filter (fun i => proj 𝒜 i x ∉ I) with set₁_eq + set set₂ := (decompose 𝒜 y).support.filter (fun i => proj 𝒜 i y ∉ I) with set₂_eq + have nonempty : + ∀ x : A, x ∉ I → ((decompose 𝒜 x).support.filter (fun i => proj 𝒜 i x ∉ I)).Nonempty := by + intro x hx + rw [filter_nonempty_iff] + contrapose! hx + simp_rw [proj_apply] at hx + rw [← sum_support_decompose 𝒜 x] + exact Ideal.sum_mem _ hx + set max₁ := set₁.max' (nonempty x rid₁) + set max₂ := set₂.max' (nonempty y rid₂) + have mem_max₁ : max₁ ∈ set₁ := max'_mem set₁ (nonempty x rid₁) + have mem_max₂ : max₂ ∈ set₂ := max'_mem set₂ (nonempty y rid₂) + replace hxy : proj 𝒜 (max₁ + max₂) (x * y) ∈ I := hI _ hxy + have mem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∈ I := by + set antidiag := + ((decompose 𝒜 x).support ×ᶠ (decompose 𝒜 y).support).filter (fun z : ι × ι => + z.1 + z.2 = max₁ + max₂) with ha + have mem_antidiag : (max₁, max₂) ∈ antidiag := by + simp only [add_sum_erase, mem_filter, mem_product] + exact ⟨⟨mem_of_mem_filter _ mem_max₁, mem_of_mem_filter _ mem_max₂⟩, trivial⟩ + have eq_add_sum := + calc + proj 𝒜 (max₁ + max₂) (x * y) = ∑ ij in antidiag, proj 𝒜 ij.1 x * proj 𝒜 ij.2 y := by + simp_rw [ha, proj_apply, DirectSum.decompose_mul, DirectSum.coe_mul_apply 𝒜] + _ = + proj 𝒜 max₁ x * proj 𝒜 max₂ y + + ∑ ij in antidiag.erase (max₁, max₂), proj 𝒜 ij.1 x * proj 𝒜 ij.2 y := + (add_sum_erase _ _ mem_antidiag).symm + + rw [eq_sub_of_add_eq eq_add_sum.symm] + refine' Ideal.sub_mem _ hxy (Ideal.sum_mem _ fun z H => _) + rcases z with ⟨i, j⟩ + simp only [mem_erase, Prod.mk.inj_iff, Ne.def, mem_filter, mem_product] at H + rcases H with ⟨H₁, ⟨H₂, H₃⟩, H₄⟩ + have max_lt : max₁ < i ∨ max₂ < j := by + rcases lt_trichotomy max₁ i with (h | rfl | h) + · exact Or.inl h + · refine' False.elim (H₁ ⟨rfl, add_left_cancel H₄⟩) + · apply Or.inr + have := add_lt_add_right h j + rw [H₄] at this + exact lt_of_add_lt_add_left this + cases' max_lt with max_lt max_lt + · -- in this case `max₁ < i`, then `xᵢ ∈ I`; for otherwise `i ∈ set₁` then `i ≤ max₁`. + have not_mem : i ∉ set₁ := fun h => + lt_irrefl _ ((max'_lt_iff set₁ (nonempty x rid₁)).mp max_lt i h) + rw [set₁_eq] at not_mem + simp only [not_and, Classical.not_not, Ne.def, mem_filter] at not_mem + exact Ideal.mul_mem_right _ I (not_mem H₂) + · -- in this case `max₂ < j`, then `yⱼ ∈ I`; for otherwise `j ∈ set₂`, then `j ≤ max₂`. + have not_mem : j ∉ set₂ := fun h => + lt_irrefl _ ((max'_lt_iff set₂ (nonempty y rid₂)).mp max_lt j h) + rw [set₂_eq] at not_mem + simp only [not_and, Classical.not_not, Ne.def, mem_filter] at not_mem + exact Ideal.mul_mem_left I _ (not_mem H₃) + have not_mem_I : proj 𝒜 max₁ x * proj 𝒜 max₂ y ∉ I := by + have neither_mem : proj 𝒜 max₁ x ∉ I ∧ proj 𝒜 max₂ y ∉ I := by + rw [mem_filter] at mem_max₁ mem_max₂ + exact ⟨mem_max₁.2, mem_max₂.2⟩ + intro _rid + cases' homogeneous_mem_or_mem ⟨max₁, SetLike.coe_mem _⟩ ⟨max₂, SetLike.coe_mem _⟩ mem_I + with h h + · apply neither_mem.1 h + · apply neither_mem.2 h + exact not_mem_I mem_I⟩ +#align ideal.is_homogeneous.is_prime_of_homogeneous_mem_or_mem Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem + +theorem Ideal.IsHomogeneous.isPrime_iff {I : Ideal A} (h : I.IsHomogeneous 𝒜) : + I.IsPrime ↔ + I ≠ ⊤ ∧ + ∀ {x y : A}, + SetLike.Homogeneous 𝒜 x → SetLike.Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I := + ⟨fun HI => ⟨HI.ne_top, fun _ _ hxy => Ideal.IsPrime.mem_or_mem HI hxy⟩, + fun ⟨I_ne_top, homogeneous_mem_or_mem⟩ => + h.isPrime_of_homogeneous_mem_or_mem I_ne_top @homogeneous_mem_or_mem⟩ +#align ideal.is_homogeneous.is_prime_iff Ideal.IsHomogeneous.isPrime_iff + +theorem Ideal.IsPrime.homogeneousCore {I : Ideal A} (h : I.IsPrime) : + (I.homogeneousCore 𝒜).toIdeal.IsPrime := by + apply (Ideal.homogeneousCore 𝒜 I).is_homogeneous'.isPrime_of_homogeneous_mem_or_mem + · exact ne_top_of_le_ne_top h.ne_top (Ideal.toIdeal_homogeneousCore_le 𝒜 I) + rintro x y hx hy hxy + have H := h.mem_or_mem (Ideal.toIdeal_homogeneousCore_le 𝒜 I hxy) + refine' H.imp _ _ + · exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hx + · exact Ideal.mem_homogeneousCore_of_homogeneous_of_mem hy +#align ideal.is_prime.homogeneous_core Ideal.IsPrime.homogeneousCore + +theorem Ideal.IsHomogeneous.radical_eq {I : Ideal A} (hI : I.IsHomogeneous 𝒜) : + I.radical = InfSet.sInf { J | Ideal.IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime } := by + rw [Ideal.radical_eq_sInf] + apply le_antisymm + · exact sInf_le_sInf fun J => And.right + · refine sInf_le_sInf_of_forall_exists_le ?_ + rintro J ⟨HJ₁, HJ₂⟩ + refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩ + refine ⟨HomogeneousIdeal.isHomogeneous _, ?_, HJ₂.homogeneousCore⟩ + exact hI.toIdeal_homogeneousCore_eq_self.symm.trans_le (Ideal.homogeneousCore_mono _ HJ₁) +#align ideal.is_homogeneous.radical_eq Ideal.IsHomogeneous.radical_eq + +theorem Ideal.IsHomogeneous.radical {I : Ideal A} (h : I.IsHomogeneous 𝒜) : + I.radical.IsHomogeneous 𝒜 := by + rw [h.radical_eq] + exact Ideal.IsHomogeneous.sInf fun _ => And.left +#align ideal.is_homogeneous.radical Ideal.IsHomogeneous.radical + +/-- The radical of a homogenous ideal, as another homogenous ideal. -/ +def HomogeneousIdeal.radical (I : HomogeneousIdeal 𝒜) : HomogeneousIdeal 𝒜 := + ⟨I.toIdeal.radical, I.isHomogeneous.radical⟩ +#align homogeneous_ideal.radical HomogeneousIdeal.radical + +@[simp] +theorem HomogeneousIdeal.coe_radical (I : HomogeneousIdeal 𝒜) : + I.radical.toIdeal = I.toIdeal.radical := rfl +#align homogeneous_ideal.coe_radical HomogeneousIdeal.coe_radical