The morphism Spec R[x] --> Spec R, induced by the natural inclusion C : R --> R[x], is an open map.

2020-08-24-OpenMapRx2R.lean

import algebraic_geometry.prime_spectrum
import ring_theory.polynomial.basic

open ideal polynomial prime_spectrum set
/--
The morphism `Spec R[x] --> Spec R` induced by the natural inclusion `R --> R[x]`
is an open map.
-/

local attribute [instance] classical.prop_decidable

variables {R : Type*} [comm_ring R] {P : ideal R}

/-- `quoisintdomain` shows that if `P` is a prime ideal of `R`,
then `R[x]/(P)` satisfies is_integral_domain. -/
lemma quoisintdomain (H : is_prime P) :
  is_integral_domain (quotient (map C P : ideal (polynomial R))) :=
ring_equiv.is_integral_domain (polynomial (quotient P))
  (integral_domain.to_is_integral_domain (polynomial (quotient P)))
  (polynomial_quotient_equiv_quotient_polynomial P).symm

/-- `liftprime` shows that if `P` is a prime ideal of `R`,
then `P.R[x]` is a prime ideal of `R[x]`. -/
lemma liftprime (H : is_prime P) : is_prime (map C P : ideal (polynomial R)) :=
(quotient.is_integral_domain_iff_prime (map C P : ideal (polynomial R))).mp (quoisintdomain H)

/-- `image_of_Df` is the subset of `Spec R[x]` that we will prove is the image of
the non-vanishing set of `f`. -/
def image_of_Df (f : polynomial R) :=
  {p : prime_spectrum R | ∃ i : ℕ , (coeff f i) ∉ p.1}

lemma std_aff_is_open (a : R) : is_open ({p : prime_spectrum R | a ∉ p.1 }) :=
begin
  refine ⟨{a} , ext (λ x, ⟨λ xh, _,λ xh,  _⟩)⟩;
  simpa only [mem_zero_locus, not_not, mem_set_of_eq, singleton_subset_iff, mem_compl_eq] using xh,
end

lemma total_image (f : polynomial R) :
  is_open ({p : prime_spectrum R | ∃ i : ℕ , coeff f i ∉ p.1 }) :=
begin
  rw set_of_exists (λ i (x : prime_spectrum R), coeff f i ∉ x.val),
  exact is_open_Union (λ i, std_aff_is_open (coeff f i)),
end

lemma fincN (f : polynomial R) :
  f ∈ ideal.span {tt : polynomial R | ∃ i : ℕ ,tt = (C (coeff f i))} :=
begin
  conv_lhs {rw as_sum_support f},
  refine submodule.sum_mem _ (λ i hi, _),
  rw [← C_mul_X_pow_eq_monomial, mul_comm],
  refine submodule.smul_mem _ _ (submodule.subset_span ⟨i, rfl⟩),
end

/-- `imma_f2ind` shows that the image of `Df` is contained in an open set
(with which it actually coincides). -/
lemma imma_f2ind (f : polynomial R) (I : prime_spectrum (polynomial R)) :
  f ∉ I.1 → ∃ i : ℕ , coeff f i ∉ (prime_spectrum.comap (polynomial.C : R →+* polynomial R) I).1 :=
begin
  contrapose!,
  intros cini,
  have anc1 : {tt : polynomial R | ∃ (i : ℕ), tt = C (f.coeff i)} ⊆ I.val,
  { rintros tt ⟨i, rfl⟩,
    exact (submodule.mem_coe I.val).mpr (cini i) },
  have anc3 : (span {tt : polynomial R | ∃ (i : ℕ), tt = C (f.coeff i)}).1 ⊆ I.val :=
    bInter_subset_of_mem anc1,
  { refine (anc3) (fincN f), },
end

/-- `imma_spec` shows that if a point of `Spec R[x]` is not contained in the vanishing set of `f`,
then its image in `Spec R` is contained in the open where at least one of the coefficients
of `f` is non-zero. This lemma is a reformulation of `imma_f2ind`. -/
lemma imma_spec {f : polynomial R} {I : prime_spectrum (polynomial R)}
  (H : I ∈ (prime_spectrum.zero_locus {f} : set (prime_spectrum (polynomial R)))ᶜ ) :
  prime_spectrum.comap (polynomial.C : R →+* polynomial R) I ∈ image_of_Df f :=
begin
  refine imma_f2ind f I _,
  rw [mem_compl_eq, mem_zero_locus, singleton_subset_iff] at H,
  exact H,
end

theorem Rx2Ropen :
  is_open_map (prime_spectrum.comap (polynomial.C : R →+* polynomial R)) :=
begin
  rintros U ⟨fs, cl⟩,
  have funis : fs = (⋃ i : fs , {i.1}),
  { refine ext (λ x, ⟨λ hf, mem_Union.mpr (Exists.intro ⟨x, hf⟩ (mem_singleton x)), _⟩),
    rintro ⟨-, ⟨⟨-, xfs⟩, rfl⟩, ⟨⟩⟩,
    exact xfs },
  rw [funis, zero_locus_Union] at cl,
  have uuni : U = (⋂ (i : ↥fs), zero_locus {i.val})ᶜ,
  { obtain F := (congr_arg compl cl).symm,
    rwa compl_compl at F },
  rw [uuni, compl_Inter, image_Union],
  refine is_open_Union (λ f, _),
  convert total_image f.1,
  refine ext (λ x, ⟨_, λ hx, ⟨⟨map C x.1, (liftprime x.2)⟩, ⟨_, _⟩⟩⟩),
  { rintro ⟨xli, complement, rfl⟩,
    exact imma_spec complement },
  { rw [mem_compl_eq, mem_zero_locus, singleton_subset_iff],
    cases hx with i hi,
    exact λ a, hi (mem_map_C_iff.mp a i) },
  { refine subtype.ext (ext (λ x, ⟨λ h, _, λ h, submodule.subset_span (mem_image_of_mem C.1 h)⟩)),
    rw ← @coeff_C_zero _ x,
    exact mem_map_C_iff.mp h 0}
end