comm_alg/CommAlg/Leo.lean
2023-06-15 18:05:33 -07:00

334 lines
11 KiB
Text
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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 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
variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
variable {S : Type _} [CommRing S] [Algebra R S] [IsLocalization.AtPrime S I.asIdeal]
open Ideal
open LocalRing
open PrimeSpectrum
#check algebraMap R (Localization.AtPrime I.asIdeal)
#check PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal))
#check krullDim
#check dim_eq_bot_iff
#check height_le_krullDim
variable (J₁ J₂ : PrimeSpectrum (Localization.AtPrime I.asIdeal))
example (h : J₁ ≤ J₂) : PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) J₁ ≤
PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) J₂ := by
intro x hx
exact h hx
def gadslfasd' : Ideal S := (IsLocalization.AtPrime.localRing S I.asIdeal).maximalIdeal
-- instance gadslfasd : LocalRing S := IsLocalization.AtPrime.localRing S I.asIdeal
example (f : α → β) (hf : Function.Injective f) (h : a₁ ≠ a₂) : f a₁ ≠ f a₂ := by library_search
instance map_prime (J : PrimeSpectrum R) (hJ : J ≤ I) :
(Ideal.map (algebraMap R S) J.asIdeal : Ideal S).IsPrime where
ne_top' := by
intro h
rw [eq_top_iff_one, map, mem_span] at h
mem_or_mem' := sorry
lemma comap_lt_of_lt (J₁ J₂ : PrimeSpectrum S) (J_lt : J₁ < J₂) :
PrimeSpectrum.comap (algebraMap R S) J₁ < PrimeSpectrum.comap (algebraMap R S) J₂ := by
apply lt_of_le_of_ne
apply comap_mono (le_of_lt J_lt)
sorry
lemma lt_of_comap_lt (J₁ J₂ : PrimeSpectrum S)
(hJ : PrimeSpectrum.comap (algebraMap R S) J₁ < PrimeSpectrum.comap (algebraMap R S) J₂) :
J₁ < J₂ := by
apply lt_of_le_of_ne
sorry
/- If S = R_p, then height p = dim S -/
lemma height_eq_height_comap (J : PrimeSpectrum S) :
height (PrimeSpectrum.comap (algebraMap R S) J) = height J := by
simp [height]
have H : {J_1 | J_1 < (PrimeSpectrum.comap (algebraMap R S)) J} =
(PrimeSpectrum.comap (algebraMap R S))'' {J_2 | J_2 < J}
. sorry
rw [H]
apply Set.chainHeight_image
intro x y
constructor
apply comap_lt_of_lt
apply lt_of_comap_lt
lemma disjoint_primeCompl (I : PrimeSpectrum R) :
{ p | Disjoint (I.asIdeal.primeCompl : Set R) p.asIdeal} = {p | p ≤ I} := by
ext p; apply Set.disjoint_compl_left_iff_subset
theorem localizationPrime_comap_range [Algebra R S] (I : PrimeSpectrum R) [IsLocalization.AtPrime S I.asIdeal] :
Set.range (PrimeSpectrum.comap (algebraMap R S)) = { p | p ≤ I} := by
rw [← disjoint_primeCompl]
apply localization_comap_range
#check Set.chainHeight_image
lemma height_eq_dim_localization : height I = krullDim S := by
--first show height I = height gadslfasd'
simp [@krullDim_eq_height _ _ (IsLocalization.AtPrime.localRing S I.asIdeal)]
simp [height]
let f := (PrimeSpectrum.comap (algebraMap R S))
have H : {J | J < I} = f '' {J | J < closedPoint S}
lemma height_eq_dim_localization' :
height I = krullDim (Localization.AtPrime I.asIdeal) := Ideal.height_eq_dim_localization I
end Localization
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
--the map R → R[X] is C →+*
--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 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
. 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 ⊢
constructor
. rw [adjoin_x_eq, adjoin_x_eq]
apply sup_le_sup_right
apply map_mono h.1
. intro H
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 [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
exact comm
lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
krullDim R + (1 : ℕ∞) ≤ krullDim (Polynomial R) := by
cases' krullDim_nonneg_of_nontrivial R with n hn
rw [hn]
change ↑(n + 1) ≤ krullDim R[X]
have hn' := le_of_eq hn.symm
rw [le_krullDim_iff'] at hn' ⊢
cases' hn' with I hI
use adjoin_x' I
apply WithBot.coe_mono
calc n + 1 ≤ height I + 1 := by
apply add_le_add_right
rw [WithBot.coe_le_coe] at hI
exact hI
_ ≤ height (adjoin_x' I) := ht_adjoin_x_eq_ht_add_one I
end Polynomial
open Ideal
variable {R : Type _} [CommRing R]
lemma height_le_top_iff_exists {I : PrimeSpectrum R} (hI : height I ≤ ) :
∃ n : , true := by
sorry
lemma eq_of_height_eq_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) (hJ : height J < )
(ht_eq : height I = height J) : I = J := by
by_cases h : I = J
. exact h
. have I_lt_J := lt_of_le_of_ne I_le_J h
exfalso
sorry
section Quotient
variables {R : Type _} [CommRing R] (I : Ideal R)
#check List.map <| PrimeSpectrum.comap <| Ideal.Quotient.mk I
lemma comap_chain {l : List (PrimeSpectrum (R I))} (hl : l.Chain' (· < ·)) :
List.Chain' (. < .) ((List.map <| PrimeSpectrum.comap <| Ideal.Quotient.mk I) l) := by
lemma dim_quotient_le_dim : krullDim (R I) ≤ krullDim R := by
end Quotient