[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)
[PROOFSTEP]
rw [imageOfDf, setOf_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]
[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ (i : ℕ), {x | ¬coeff f i ∈ x.asIdeal})
[PROOFSTEP]
exact isOpen_iUnion fun i => isOpen_basicOpen
[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ imageOfDf f = ↑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ imageOfDf f ↔ x ∈ ↑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ
[PROOFSTEP]
refine' ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime x.IsPrime⟩, ⟨_, _⟩⟩, _⟩
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ { asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) } ∈ (zeroLocus {f})ᶜ
[PROOFSTEP]
rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ ¬f ∈ ↑{ asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) }.asIdeal
[PROOFSTEP]
cases' hx with i hi
[GOAL]
case h.refine'_1.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : ¬coeff f i ∈ x.asIdeal
⊢ ¬f ∈ ↑{ asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) }.asIdeal
[PROOFSTEP]
exact fun a => hi (mem_map_C_iff.mp a i)
[GOAL]
case h.refine'_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ ↑(PrimeSpectrum.comap C)
      { asIdeal := Ideal.map C x.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x.asIdeal)) } =
    x
[PROOFSTEP]
ext x
[GOAL]
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
⊢ x ∈
      (↑(PrimeSpectrum.comap C)
          { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal ↔
    x ∈ x✝.asIdeal
[PROOFSTEP]
refine' ⟨fun h => _, fun h => subset_span (mem_image_of_mem C.1 h)⟩
[GOAL]
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h :
  x ∈
    (↑(PrimeSpectrum.comap C)
        { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal
⊢ x ∈ x✝.asIdeal
[PROOFSTEP]
rw [← @coeff_C_zero R x _]
[GOAL]
case h.refine'_2.asIdeal.h
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h :
  x ∈
    (↑(PrimeSpectrum.comap C)
        { asIdeal := Ideal.map C x✝.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map C x✝.asIdeal)) }).asIdeal
⊢ coeff (↑C x) 0 ∈ x✝.asIdeal
[PROOFSTEP]
exact mem_map_C_iff.mp h 0
[GOAL]
case h.refine'_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ ↑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ → x ∈ imageOfDf f
[PROOFSTEP]
rintro ⟨xli, complement, rfl⟩
[GOAL]
case h.refine'_3.intro.intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
xli : PrimeSpectrum R[X]
complement : xli ∈ (zeroLocus {f})ᶜ
⊢ ↑(PrimeSpectrum.comap C) xli ∈ imageOfDf f
[PROOFSTEP]
exact comap_C_mem_imageOfDf complement
[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpenMap ↑(PrimeSpectrum.comap C)
[PROOFSTEP]
rintro U ⟨s, z⟩
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (↑(PrimeSpectrum.comap C) '' U)
[PROOFSTEP]
rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter, image_iUnion]
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ (i : ↑s), ↑(PrimeSpectrum.comap C) '' (zeroLocus {↑i})ᶜ)
[PROOFSTEP]
simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
f : R[X]
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ (i : ↑s), imageOfDf ↑i)
[PROOFSTEP]
exact isOpen_iUnion fun f => isOpen_imageOfDf
