R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
⊢ ∀ (x : PrimeSpectrum R), (∃ x_1, I ≤ x_1.asIdeal ∧ ↑(comap f) x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
⊢ ↑(comap f) '' zeroLocus ↑I = zeroLocus ↑(Ideal.comap f I)
simp only [Set.ext_iff, Set.mem_image, mem_zeroLocus, SetLike.coe_subset_coe]
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
⊢ (∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p) → Ideal.comap f I ≤ p.asIdeal

case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
⊢ ∀ (x : PrimeSpectrum R), (∃ x_1, I ≤ x_1.asIdeal ∧ ↑(comap f) x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal
refine' fun p => ⟨_, fun h_I_p => _⟩
case refine'_1.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum S
hp : I ≤ p.asIdeal
a : R
ha : a ∈ Ideal.comap f I
⊢ a ∈ (↑(comap f) p).asIdeal
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
⊢ (∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p) → Ideal.comap f I ≤ p.asIdeal
rintro ⟨p, hp, rfl⟩ a ha
no goals
case refine'_1.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum S
hp : I ≤ p.asIdeal
a : R
ha : a ∈ Ideal.comap f I
⊢ a ∈ (↑(comap f) p).asIdeal
exact hp ha
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p
have hp : ker f ≤ p.asIdeal := (Ideal.comap_mono bot_le).trans h_I_p
case refine'_2.refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : S
hx : x ∈ I
⊢ x ∈ { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }.asIdeal

case refine'_2.refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ↑(comap f) { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) } = p
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p
refine' ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => _, _⟩
case refine'_2.refine'_1.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x' : R
hx : ↑f x' ∈ I
⊢ ↑f x' ∈ { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }.asIdeal
case refine'_2.refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : S
hx : x ∈ I
⊢ x ∈ { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }.asIdeal
obtain ⟨x', rfl⟩ := hf x
no goals
case refine'_2.refine'_1.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x' : R
hx : ↑f x' ∈ I
⊢ ↑f x' ∈ { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }.asIdeal
exact Ideal.mem_map_of_mem f (h_I_p hx)
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈
      (↑(comap f)
          { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }).asIdeal ↔
    x ∈ p.asIdeal
case refine'_2.refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ↑(comap f) { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) } = p
ext x
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ ↑f x ∈ Ideal.map f p.asIdeal ↔ x ∈ p.asIdeal
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈
      (↑(comap f)
          { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }).asIdeal ↔
    x ∈ p.asIdeal
change f x ∈ p.asIdeal.map f ↔ _
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1, x_1 ∈ p.asIdeal ∧ ↑f x_1 = ↑f x) ↔ x ∈ p.asIdeal
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ ↑f x ∈ Ideal.map f p.asIdeal ↔ x ∈ p.asIdeal
rw [Ideal.mem_map_iff_of_surjective f hf]
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1, x_1 ∈ p.asIdeal ∧ ↑f x_1 = ↑f x) → x ∈ p.asIdeal
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1, x_1 ∈ p.asIdeal ∧ ↑f x_1 = ↑f x) ↔ x ∈ p.asIdeal
refine' ⟨_, fun hx => ⟨x, hx, rfl⟩⟩
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x ∈ p.asIdeal
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1, x_1 ∈ p.asIdeal ∧ ↑f x_1 = ↑f x) → x ∈ p.asIdeal
rintro ⟨x', hx', heq⟩
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x' - (x' - x) ∈ p.asIdeal
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x ∈ p.asIdeal
rw [← sub_sub_cancel x' x]
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x' - x ∈ ker f
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x' - (x' - x) ∈ p.asIdeal
refine' p.asIdeal.sub_mem hx' (hp _)
no goals
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.338029
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x' - x ∈ ker f
rwa [mem_ker, map_sub, sub_eq_zero]