Finished last sorry on dim_le_dim_polynomial!!!

CommAlg/Leo.lean

@@ -1,6 +1,7 @@
 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
@@ -9,6 +10,40 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import CommAlg.krull
 
+section AddToOrder
+
+open List hiding le_antisymm
+open OrderDual
+
+universe u v
+
+variable {α β : Type _}
+variable [LT α] [LT β] (s t : Set α)
+
+namespace Set
+
+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
+
+namespace List
+#check Option
+
+theorem getLast?_map (l : List α) (f : α → β) :
+  (l.map f).getLast? = Option.map f (l.getLast?) := by
+  cases' l with a l
+  . rfl
+  induction' l with b l ih
+  . rfl
+  . simp [List.getLast?_cons_cons, ih]
+  
+
+end List
+end AddToOrder
+
 --trying and failing to prove ht p = dim R_p
 section Localization
 
@@ -102,6 +137,8 @@ section Polynomial
 
 open Ideal Polynomial
 variables {R : Type _} [CommRing R]
+variable (J : Ideal R[X])
+#check Ideal.comap C J
 
 --given ideals I J, I ⊔ J is their sum
 --given a in R, span {a} is the ideal generated by a
@@ -109,48 +146,138 @@ variables {R : Type _} [CommRing R]
 --to show p[x] is prime, show p[x] is the kernel of the map R[x] → R → R/p
 #check RingHom.ker_isPrime
 
-def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp (evalRingHom 0)
+def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp constantCoeff
+--def adj_x_map' (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp (evalRingHom 0)
 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 _
 
+/- This somehow isn't in Mathlib? -/
+@[simp]
+theorem span_singleton_one : span ({0} : Set R) = ⊥ := by simp only [span_singleton_eq_bot]
+
+theorem coeff_C_eq : RingHom.comp constantCoeff C = RingHom.id R := by ext; simp
+
+variable (I : PrimeSpectrum R)
+#check RingHom.ker (C.comp (Ideal.Quotient.mk I.asIdeal))
+--#check Ideal.Quotient.mk I.asIdeal
+
+def map_prime' (I : PrimeSpectrum R) : IsPrime (I.asIdeal.map C) := Ideal.isPrime_map_C_of_isPrime I.IsPrime
+
+def map_prime'' (I : PrimeSpectrum R) : PrimeSpectrum R[X] := ⟨I.asIdeal.map C, map_prime' I⟩
+
 @[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]
 
+-- ideal.mem_quotient_iff_mem_sup
 lemma adjoin_x_eq (I : Ideal R) : adjoin_x I = I.map C ⊔ Ideal.span {X} := by
   apply le_antisymm
-  . sorry
+  . 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]
 
+lemma adjoin_x_inj {I J : Ideal R} (h : adjoin_x I = adjoin_x J) : I = J := by
+  simp [adjoin_x_eq] at h
+  have H : Ideal.map constantCoeff (Ideal.map C I ⊔ span {X}) =
+          Ideal.map constantCoeff (Ideal.map C J ⊔ span {X}) := by rw [h]
+  simp [Ideal.map_sup, Ideal.map_span, Ideal.map_map, coeff_C_eq] at H
+  exact H
+
+
+lemma map_lt_adjoin_x (I : PrimeSpectrum R) : map_prime'' I < adjoin_x' I := by
+  simp [map_prime'', adjoin_x', adjoin_x_eq]
+  show Ideal.map C I.asIdeal < Ideal.map C I.asIdeal ⊔ span {X}
+  simp [Ideal.span_le, mem_map_C_iff]
+  use 1
+  simp
+  intro h
+  apply I.IsPrime.ne_top'
+  rw [Ideal.eq_top_iff_one]
+  exact h
+
+lemma map_inj {I J : Ideal R} (h : I.map C = J.map C) : I = J := by
+  have H : Ideal.map constantCoeff (Ideal.map C I) =
+          Ideal.map constantCoeff (Ideal.map C J) := by rw [h]
+  simp [Ideal.map_map, coeff_C_eq] at H
+  exact H
+
+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 ⊢
+  constructor
+  . apply map_mono h.1
+  . intro H
+    exact h.2 (map_inj H)
+
 lemma adjoin_x_strictmono (I J : Ideal R) (h : I < J) : adjoin_x I < adjoin_x J := by
   rw [lt_iff_le_and_ne] at h ⊢
-  rw [adjoin_x_eq, adjoin_x_eq]
   constructor
-  . apply sup_le_sup_right
+  . rw [adjoin_x_eq, adjoin_x_eq]
+    apply sup_le_sup_right
     apply map_mono h.1
   . intro H
-    have H' : Ideal.comap C (Ideal.map C I ⊔ span {X}) = Ideal.comap C (Ideal.map C J ⊔ span {X})
-    . rw [H]
-    sorry
+    exact h.2 (adjoin_x_inj H)
 
+example (n : ℕ∞) : n + 0 = n := by simp?
+
+#eval List.Chain' (· < ·) [2,3]
+example : [4,5] ++ [2] = [4,5,2] := rfl
+#eval [2,4,5].map (λ n => n + n)
 
 /- Given an ideal p in R, define the ideal p[x] in R[x] -/
-lemma ht_adjoin_x_eq_ht_add_one (I : PrimeSpectrum R) : height I + 1 ≤ height (adjoin_x' I) := by
-  have H : ∀ l ∈ {J : PrimeSpectrum R | J < I}.subchain, ∃
-
-lemma ne_bot_iff_exists (n : WithBot ℕ∞) : n ≠ ⊥ ↔ ∃ m : ℕ∞, n = m := by
-  cases' n with n;
-  simp
-  intro x hx
-  cases hx
-  simp
-  use n
-  rfl
+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])
+  constructor
+  . simp [Set.append_mem_subchain_iff]
+    refine' ⟨_,_,_⟩
+    . show (List.map map_prime'' l).Chain' (· < ·) ∧ ∀ i ∈ _, i ∈ _
+      constructor
+      . apply List.chain'_map_of_chain' map_prime''
+        intro a b hab
+        apply map_strictmono a.asIdeal b.asIdeal
+        exact hab
+        exact hl.1
+      . intro i hi
+        rw [List.mem_map] at hi
+        obtain ⟨a, ha, rfl⟩ := hi
+        show map_prime'' a < adjoin_x' I
+        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
+    . apply map_lt_adjoin_x
+    . intro a ha
+      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
+  . simp
 
 lemma ne_bot_iff_exists' (n : WithBot ℕ∞) : n ≠ ⊥ ↔ ∃ m : ℕ∞, n = m := by
   convert WithBot.ne_bot_iff_exists using 3