Merge pull request #100 from GTBarkley/leo

Leo

CommAlg/krull.lean

@@ -442,8 +442,6 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
     have : {J | J < P}.Nonempty := Set.nonempty_of_mem this
     rwa [←Set.one_le_chainHeight_iff, ←WithBot.one_le_coe] at this
 
-lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
-  krullDim R + 1 ≤ krullDim (Polynomial R) := sorry
 
 -- lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
 --   krullDim R + 1 = krullDim (Polynomial R) := sorry
@@ -457,6 +455,4 @@ lemma dim_mvPolynomial [Field K] (n : ℕ) : krullDim (MvPolynomial (Fin n) K) =
 lemma height_eq_dim_localization :
   height I = krullDim (Localization.AtPrime I.asIdeal) := sorry
 
-lemma dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry
-
 lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry

CommAlg/quotient.lean

@@ -0,0 +1,52 @@
+import CommAlg.krull
+
+variable {R : Type _} [CommRing R] (I : Ideal R)
+
+open Ideal
+open PrimeSpectrum
+
+lemma comap_strictmono {𝔭 𝔮 : PrimeSpectrum (R ⧸ I)} (h : 𝔭 < 𝔮) :
+  PrimeSpectrum.comap (Ideal.Quotient.mk I) 𝔭 < PrimeSpectrum.comap (Ideal.Quotient.mk I) 𝔮 := by
+  rw [lt_iff_le_and_ne] at h ⊢
+  refine' ⟨Ideal.comap_mono h.1, fun H => h.2 _⟩
+  . apply PrimeSpectrum.comap_injective_of_surjective (Ideal.Quotient.mk I)
+    . exact Quotient.mk_surjective
+    . exact H
+
+lemma ht_comap_eq_ht (𝔭 : PrimeSpectrum (R ⧸ I)) :
+  height 𝔭 ≤ height (comap (Ideal.Quotient.mk I) 𝔭) := by
+  rw [height, height, Set.chainHeight_le_chainHeight_iff]
+  rintro l ⟨l_ch, l_lt⟩
+  use l.map (comap <| Ideal.Quotient.mk I)
+  refine' ⟨⟨_, _⟩, by simp⟩
+  . apply List.chain'_map_of_chain' (PrimeSpectrum.comap (Ideal.Quotient.mk I)) _ l_ch
+    intro a b hab; apply comap_strictmono; apply hab
+  . rintro i hi
+    rw [List.mem_map] at hi
+    obtain ⟨a, a_mem, rfl⟩ := hi
+    apply comap_strictmono
+    apply l_lt a a_mem
+
+/- TODO: find a better lemma to avoid repeated code -/
+lemma dim_quotient_le_dim : krullDim (R ⧸ I) ≤ krullDim R := by
+  by_cases H : Nontrivial (R ⧸ I)
+  . obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial (R ⧸ I)
+    rw [hn]
+    induction' n using ENat.recTopCoe with n
+    . have H := (krullDim_eq_top_iff _).mp hn
+      show ⊤ ≤ _
+      rw [top_le_iff, krullDim_eq_top_iff] 
+      intro n
+      obtain ⟨𝔭, hI⟩ := H n
+      use comap (Ideal.Quotient.mk I) 𝔭
+      apply le_trans hI (ht_comap_eq_ht I _)
+    . show n ≤ krullDim _
+      rw [le_krullDim_iff]
+      obtain ⟨𝔭, hI⟩ := le_krullDim_iff.mp <| le_of_eq hn.symm
+      use comap (Ideal.Quotient.mk I) 𝔭
+      norm_cast at hI ⊢
+      apply le_trans hI (ht_comap_eq_ht I _)
+  . suffices : krullDim (R ⧸ I) = ⊥
+    . rw [this]; apply bot_le
+    rw [dim_eq_bot_iff, ←not_nontrivial_iff_subsingleton]
+    exact H