R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ Set.Nonempty (zeroLocus ↑I) ∧ IsPreirreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ IsIrreducible (zeroLocus ↑I) ↔ Ideal.IsPrime I
rw [Ideal.isPrime_iff, IsIrreducible]
case h₁
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ Set.Nonempty (zeroLocus ↑I) ↔ I ≠ ⊤

case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ Set.Nonempty (zeroLocus ↑I) ∧ IsPreirreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
apply and_congr
no goals
case h₁
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ Set.Nonempty (zeroLocus ↑I) ↔ I ≠ ⊤
rw [Set.nonempty_iff_ne_empty, Ne.def, zeroLocus_empty_iff_eq_top]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ IsPreirreducible (zeroLocus ↑I) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
trans ∀ x y : Ideal R, Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ IsPreirreducible (zeroLocus ↑I) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
simp_rw [isPreirreducible_iff_closed_union_closed, isClosed_iff_zeroLocus_ideal]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) →
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
constructor
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h :
  ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
    (∃ I, z₁ = zeroLocus ↑I) → (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) →
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
rintro h x y
no goals
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h :
  ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
    (∃ I, z₁ = zeroLocus ↑I) → (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
exact h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h :
  ∀ (x y : Ideal R),
    zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂
rintro h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
no goals
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h :
  ∀ (x y : Ideal R),
    zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
exact h x y
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
simp_rw [← zeroLocus_inf, subset_zeroLocus_iff_le_vanishingIdeal,
  vanishingIdeal_zeroLocus_eq_radical, hI.radical]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
constructor
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) →
    ∀ {x y : R}, Ideal.span {x} * Ideal.span {y} ≤ I → Ideal.span {x} ≤ I ∨ Ideal.span {y} ≤ I
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ←
  Ideal.span_singleton_mul_span_singleton]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : Ideal.span {x} * Ideal.span {y} ≤ I
⊢ Ideal.span {x} ⊓ Ideal.span {y} ≤ I
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) →
    ∀ {x y : R}, Ideal.span {x} * Ideal.span {y} ≤ I → Ideal.span {x} ≤ I ∨ Ideal.span {y} ≤ I
refine' fun h x y h' => h _ _ _
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : Ideal.radical (Ideal.span {x} * Ideal.span {y}) ≤ I
⊢ Ideal.radical (Ideal.span {x} ⊓ Ideal.span {y}) ≤ I
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : Ideal.span {x} * Ideal.span {y} ≤ I
⊢ Ideal.span {x} ⊓ Ideal.span {y} ≤ I
rw [← hI.radical_le_iff] at h'⊢
no goals
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : Ideal.radical (Ideal.span {x} * Ideal.span {y}) ≤ I
⊢ Ideal.radical (Ideal.span {x} ⊓ Ideal.span {y}) ≤ I
simpa only [Ideal.radical_inf, Ideal.radical_mul] using h'
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ {x y : R}, x * y ∈ I → ¬x ∈ I → y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → (∃ x_1, x_1 ∈ x ∧ ¬x_1 ∈ I) → y ≤ I
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ {x y : R}, x * y ∈ I → ¬x ∈ I → y ∈ I
s t : Ideal R
h' : s ⊓ t ≤ I
x : R
hx : x ∈ s
hx' : ¬x ∈ I
y : R
hy : y ∈ t
⊢ y ∈ I
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ {x y : R}, x * y ∈ I → ¬x ∈ I → y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → (∃ x_1, x_1 ∈ x ∧ ¬x_1 ∈ I) → y ≤ I
rintro h s t h' ⟨x, hx, hx'⟩ y hy
no goals
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ {x y : R}, x * y ∈ I → ¬x ∈ I → y ∈ I
s t : Ideal R
h' : s ⊓ t ≤ I
x : R
hx : x ∈ s
hx' : ¬x ∈ I
y : R
hy : y ∈ t
⊢ y ∈ I
exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'