feat(algebraic_geometry/is_open_comap_C): add file is_open_comap_C, prove that Spec R[x] \to Spec R is an open map (#5693)

This file is the first part of a proof of Chevalley's Theorem.  It contains a proof that the morphism Spec R[x] \to Spec R is open.  In a later PR, I hope to prove that, under the same morphism, the image of a closed set is constructible.

Author: adomani

src/algebraic_geometry/is_open_comap_C.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2021 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import algebraic_geometry.prime_spectrum
+import ring_theory.polynomial.basic
+/-!
+The morphism `Spec R[x] --> Spec R` induced by the natural inclusion `R --> R[x]` is an open map.
+-/
+
+open ideal polynomial prime_spectrum set
+
+namespace algebraic_geometry
+
+namespace polynomial
+
+variables {R : Type*} [comm_ring R] {f : polynomial R}
+
+/-- Given a polynomial `f ∈ R[x]`, `image_of_Df` is the subset of `Spec R` where at least one
+of the coefficients of `f` does not vanish.  Lemma `image_of_Df_eq_comap_C_compl_zero_locus`
+proves that `image_of_Df` is the image of `(zero_locus {f})ᶜ` under the morphism
+`comap C : Spec R[x] → Spec R`. -/
+def image_of_Df (f) : set (prime_spectrum R) :=
+  {p : prime_spectrum R | ∃ i : ℕ , (coeff f i) ∉ p.as_ideal}
+
+lemma is_open_image_of_Df : is_open (image_of_Df f) :=
+begin
+  rw [image_of_Df, set_of_exists (λ i (x : prime_spectrum R), coeff f i ∉ x.val)],
+  exact is_open_Union (λ i, is_open_basic_open),
+end
+
+/-- 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 set where at least one of the coefficients of `f` is non-zero.
+This lemma is a reformulation of `exists_coeff_not_mem_C_inverse`. -/
+lemma comap_C_mem_image_of_Df {I : prime_spectrum (polynomial R)}
+  (H : I ∈ (zero_locus {f} : set (prime_spectrum (polynomial R)))ᶜ ) :
+  comap (polynomial.C : R →+* polynomial R) I ∈ image_of_Df f :=
+exists_coeff_not_mem_C_inverse (mem_compl_zero_locus_iff_not_mem.mp H)
+
+/-- The open set `image_of_Df f` coincides with the image of `basic_open f` under the
+morphism `C⁺ : Spec R[x] → Spec R`. -/
+lemma image_of_Df_eq_comap_C_compl_zero_locus :
+  image_of_Df f = comap C '' (zero_locus {f})ᶜ :=
+begin
+  refine ext (λ x, ⟨λ hx, ⟨⟨map C x.val, (is_prime_map_C_of_is_prime x.property)⟩, ⟨_, _⟩⟩, _⟩),
+  { 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, subset_span (mem_image_of_mem C.1 h)⟩)),
+    rw ← @coeff_C_zero R x _,
+    exact mem_map_C_iff.mp h 0 },
+  { rintro ⟨xli, complement, rfl⟩,
+    exact comap_C_mem_image_of_Df complement }
+end
+
+/--  The morphism `C⁺ : Spec R[x] → Spec R` is open. -/
+theorem is_open_map_comap_C :
+  is_open_map (comap (C : R →+* polynomial R)) :=
+begin
+  rintros U ⟨s, z⟩,
+  rw [← compl_compl U, ← z, ← Union_of_singleton_coe s, zero_locus_Union, compl_Inter, image_Union],
+  simp_rw [← image_of_Df_eq_comap_C_compl_zero_locus],
+  exact is_open_Union (λ f, is_open_image_of_Df),
+end
+
+end polynomial
+
+end algebraic_geometry

src/algebraic_geometry/prime_spectrum.lean

@@ -146,21 +146,8 @@ by rw [← submodule.mem_coe, coe_vanishing_ideal, set.mem_set_of_eq]
 
 lemma subset_zero_locus_iff_le_vanishing_ideal (t : set (prime_spectrum R)) (I : ideal R) :
   t ⊆ zero_locus I ↔ I ≤ vanishing_ideal t :=
-begin
-  split; intro h,
-  { intros f hf,
-    rw [mem_vanishing_ideal],
-    intros x hx,
-    have hxI := h hx,
-    rw mem_zero_locus at hxI,
-    exact hxI hf },
-  { intros x hx,
-    rw mem_zero_locus,
-    refine le_trans h _,
-    intros f hf,
-    rw [mem_vanishing_ideal] at hf,
-    exact hf x hx }
-end
+⟨λ h f k, (mem_vanishing_ideal _ _).mpr (λ x j, (mem_zero_locus _ _).mpr (h j) k), λ h,
+  λ x j, (mem_zero_locus _ _).mpr (le_trans h (λ f h, ((mem_vanishing_ideal _ _).mp h) x j))⟩
 
 section gc
 variable (R)
@@ -306,6 +293,10 @@ begin
   apply submodule.add_mem; solve_by_elim
 end
 
+lemma mem_compl_zero_locus_iff_not_mem {f : R} {I : prime_spectrum R} :
+  I ∈ (zero_locus {f} : set (prime_spectrum R))ᶜ ↔ f ∉ I.as_ideal :=
+by rw [set.mem_compl_eq, mem_zero_locus, set.singleton_subset_iff]; refl
+
 /-- The Zariski topology on the prime spectrum of a commutative ring
 is defined via the closed sets of the topology:
 they are exactly those sets that are the zero locus of a subset of the ring. -/
@@ -415,6 +406,9 @@ def basic_open (r : R) : topological_space.opens (prime_spectrum R) :=
 { val := { x | r ∉ x.as_ideal },
   property := ⟨{r}, set.ext $ λ x, set.singleton_subset_iff.trans $ not_not.symm⟩ }
 
+lemma is_open_basic_open {a : R} : is_open ((basic_open a) : set (prime_spectrum R)) :=
+(basic_open a).property
+
 end basic_open
 
 end prime_spectrum

src/data/polynomial/coeff.lean

@@ -140,4 +140,33 @@ end
 
 end coeff
 
+open submodule polynomial set
+
+variables {f : polynomial R} {I : submodule (polynomial R) (polynomial R)}
+
+/--  If the coefficients of a polynomial belong to n ideal contains the submodule span of the
+coefficients of a polynomial. -/
+lemma span_le_of_coeff_mem_C_inverse (cf : ∀ (i : ℕ), f.coeff i ∈ (C ⁻¹' I.carrier)) :
+  (span (polynomial R) {g | ∃ i, g = C (f.coeff i)}) ≤ I :=
+begin
+  refine bInter_subset_of_mem _,
+  rintros _ ⟨i, rfl⟩,
+  exact (mem_coe _).mpr (cf i),
+end
+
+lemma mem_span_C_coeff :
+  f ∈ span (polynomial R) {g : polynomial R | ∃ i : ℕ, g = (C (coeff f i))} :=
+begin
+  rw [← f.sum_single] {occs := occurrences.pos [1]},
+  refine sum_mem _ (λ i hi, _),
+  change monomial i _ ∈ span _ _,
+  rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul],
+  exact smul_mem _ _ (subset_span ⟨i, rfl⟩),
+end
+
+lemma exists_coeff_not_mem_C_inverse :
+  f ∉ I → ∃ i : ℕ , coeff f i ∉ (C ⁻¹'  I.carrier) :=
+imp_of_not_imp_not _ _
+  (λ cf, not_not.mpr ((span_le_of_coeff_mem_C_inverse (not_exists_not.mp cf)) mem_span_C_coeff))
+
 end polynomial

src/ring_theory/polynomial/basic.lean

@@ -306,6 +306,19 @@ def polynomial_quotient_equiv_quotient_polynomial (I : ideal R) :
   end,
 }
 
+/-- If `P` is a prime ideal of `R`, then `R[x]/(P)` is an integral domain. -/
+lemma is_integral_domain_map_C_quotient {P : ideal R} (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
+
+/-- If `P` is a prime ideal of `R`, then `P.R[x]` is a prime ideal of `R[x]`. -/
+lemma is_prime_map_C_of_is_prime {P : ideal R} (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
+  (is_integral_domain_map_C_quotient H)
+
 /-- Given any ring `R` and an ideal `I` of `polynomial R`, we get a map `R → R[x] → R[x]/I`.
   If we let `R` be the image of `R` in `R[x]/I` then we also have a map `R[x] → R'[x]`.
   In particular we can map `I` across this map, to get `I'` and a new map `R' → R'[x] → R'[x]/I`.
@@ -388,7 +401,8 @@ def leading_coeff_nth (n : ℕ) : ideal R :=
 theorem mem_leading_coeff_nth (n : ℕ) (x) :
   x ∈ I.leading_coeff_nth n ↔ ∃ p ∈ I, degree p ≤ n ∧ leading_coeff p = x :=
 begin
-  simp only [leading_coeff_nth, degree_le, submodule.mem_map, lcoeff_apply, submodule.mem_inf, mem_degree_le],
+  simp only [leading_coeff_nth, degree_le, submodule.mem_map, lcoeff_apply, submodule.mem_inf,
+    mem_degree_le],
   split,
   { rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩,
     cases lt_or_eq_of_le hpdeg with hpdeg hpdeg,