import Mathlib.RingTheory.Ideal.Operations import Mathlib.RingTheory.FiniteType import Mathlib.Order.Height import Mathlib.RingTheory.Polynomial.Quotient import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Ideal.Quotient import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.Order.ConditionallyCompleteLattice.Basic import CommAlg.krull section ChainLemma variable {α β : Type _} variable [LT α] [LT β] (s t : Set α) namespace Set open List /- Sorry for using aesop, but it doesn't take that long -/ theorem append_mem_subchain_iff : l ++ l' ∈ s.subchain ↔ l ∈ s.subchain ∧ l' ∈ s.subchain ∧ ∀ a ∈ l.getLast?, ∀ b ∈ l'.head?, a < b := by simp [subchain, chain'_append] aesop end Set end ChainLemma variable {R : Type _} [CommRing R] open Ideal Polynomial namespace Polynomial /- The composition R → R[X] → R is the identity -/ theorem coeff_C_eq : RingHom.comp constantCoeff C = RingHom.id R := by ext; simp end Polynomial /- Given an ideal I in R, we define the ideal adjoin_x' I to be the kernel of R[X] → R → R/I -/ def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp constantCoeff def adjoin_x' (I : Ideal R) : Ideal (Polynomial R) := RingHom.ker (adj_x_map I) def adjoin_x (I : PrimeSpectrum R) : PrimeSpectrum (Polynomial R) where asIdeal := adjoin_x' I.asIdeal IsPrime := RingHom.ker_isPrime _ @[simp] lemma adj_x_comp_C (I : Ideal R) : RingHom.comp (adj_x_map I) C = Ideal.Quotient.mk I := by ext x; simp [adj_x_map] lemma adjoin_x_eq (I : Ideal R) : adjoin_x' I = I.map C ⊔ Ideal.span {X} := by apply le_antisymm . rintro p hp have h : ∃ q r, p = C r + X * q := ⟨p.divX, p.coeff 0, p.divX_mul_X_add.symm.trans $ by ring⟩ obtain ⟨q, r, rfl⟩ := h suffices : r ∈ I . simp only [Submodule.mem_sup, Ideal.mem_span_singleton] refine' ⟨C r, Ideal.mem_map_of_mem C this, X * q, ⟨q, rfl⟩, rfl⟩ rw [adjoin_x', adj_x_map, RingHom.mem_ker, RingHom.comp_apply] at hp rw [constantCoeff_apply, coeff_add, coeff_C_zero, coeff_X_mul_zero, add_zero] at hp rwa [←RingHom.mem_ker, Ideal.mk_ker] at hp . rw [sup_le_iff] constructor . simp [adjoin_x', RingHom.ker, ←map_le_iff_le_comap, Ideal.map_map] . simp [span_le, adjoin_x', RingHom.mem_ker, adj_x_map] /- If I is prime in R, the pushforward I*R[X] is prime in R[X] -/ def map_prime (I : PrimeSpectrum R) : PrimeSpectrum R[X] := ⟨I.asIdeal.map C, isPrime_map_C_of_isPrime I.IsPrime⟩ /- The pushforward map (Ideal R) → (Ideal R[X]) is injective -/ lemma map_inj {I J : Ideal R} (h : I.map C = J.map C) : I = J := by have H : map constantCoeff (I.map C) = map constantCoeff (J.map C) := by rw [h] simp [Ideal.map_map, coeff_C_eq] at H exact H /- The pushforward map (Ideal R) → (Ideal R[X]) is strictly monotone -/ lemma map_strictmono {I J : Ideal R} (h : I < J) : I.map C < J.map C := by rw [lt_iff_le_and_ne] at h ⊢ exact ⟨map_mono h.1, fun H => h.2 (map_inj H)⟩ lemma map_lt_adjoin_x (I : PrimeSpectrum R) : map_prime I < adjoin_x I := by simp [adjoin_x, adjoin_x_eq] show I.asIdeal.map C < I.asIdeal.map C ⊔ span {X} simp [Ideal.span_le, mem_map_C_iff] use 1 simp rw [←Ideal.eq_top_iff_one] exact I.IsPrime.ne_top' lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I + 1 ≤ height (adjoin_x I) := by suffices H : height I + (1 : ℕ) ≤ height (adjoin_x I) + (0 : ℕ) . norm_cast at H; rw [add_zero] at H; exact H rw [height, height, Set.chainHeight_add_le_chainHeight_add {J | J < I} _ 1 0] intro l hl use ((l.map map_prime) ++ [map_prime I]) refine' ⟨_, by simp⟩ . simp [Set.append_mem_subchain_iff] refine' ⟨_, map_lt_adjoin_x I, fun a ha => _⟩ . refine' ⟨_, fun i hi => _⟩ . apply List.chain'_map_of_chain' map_prime (fun a b hab => map_strictmono hab) hl.1 . rw [List.mem_map] at hi obtain ⟨a, ha, rfl⟩ := hi calc map_prime a < map_prime I := by apply map_strictmono; apply hl.2; apply ha _ < adjoin_x I := by apply map_lt_adjoin_x . have H : ∃ b : PrimeSpectrum R, b ∈ l ∧ map_prime b = a . have H2 : l ≠ [] . intro h rw [h] at ha tauto use l.getLast H2 refine' ⟨List.getLast_mem H2, _⟩ have H3 : l.map map_prime ≠ [] . intro hl apply H2 apply List.eq_nil_of_map_eq_nil hl rw [List.getLast?_eq_getLast _ H3, Option.some_inj] at ha simp [←ha, List.getLast_map _ H2] obtain ⟨b, hb, rfl⟩ := H apply map_strictmono apply hl.2 exact hb #check (⊤ : ℕ∞) /- dim R + 1 ≤ dim R[X] -/ lemma dim_le_dim_polynomial_add_one [Nontrivial R] : krullDim R + (1 : ℕ∞) ≤ krullDim R[X] := by obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R rw [hn] change ↑(n + 1) ≤ krullDim R[X] have := le_of_eq hn.symm induction' n using ENat.recTopCoe with n . change krullDim R = ⊤ at hn change ⊤ ≤ krullDim R[X] rw [krullDim_eq_top_iff] at hn rw [top_le_iff, krullDim_eq_top_iff] intro n obtain ⟨I, hI⟩ := hn n use adjoin_x I calc n ≤ height I := hI _ ≤ height I + 1 := le_self_add _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I change n ≤ krullDim R at this change (n + 1 : ℕ) ≤ krullDim R[X] rw [le_krullDim_iff] at this ⊢ obtain ⟨I, hI⟩ := this use adjoin_x I apply WithBot.coe_mono calc n + 1 ≤ height I + 1 := by apply add_le_add_right change ((n : ℕ∞) : WithBot ℕ∞) ≤ (height I) at hI rw [WithBot.coe_le_coe] at hI exact hI _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I