diff --git a/CommAlg/Leo.lean b/CommAlg/Leo.lean index ceb6002..10d63de 100644 --- a/CommAlg/Leo.lean +++ b/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 @@ -204,4 +331,4 @@ lemma comap_chain {l : List (PrimeSpectrum (R ⧸ I))} (hl : l.Chain' (· < ·)) lemma dim_quotient_le_dim : krullDim (R ⧸ I) ≤ krullDim R := by -end Quotient \ No newline at end of file +end Quotient