diff --git a/CommAlg/hilbertpolynomial.lean b/CommAlg/hilbertpolynomial.lean new file mode 100644 index 0000000..64650dc --- /dev/null +++ b/CommAlg/hilbertpolynomial.lean @@ -0,0 +1,137 @@ +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Finiteness +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.RingTheory.FiniteType +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Algebra.DirectSum.Ring +import Mathlib.RingTheory.Ideal.LocalRing + +-- Setting for "library_search" +set_option maxHeartbeats 0 +macro "ls" : tactic => `(tactic|library_search) + +-- New tactic "obviously" +macro "obviously" : tactic => + `(tactic| ( + first + | dsimp; simp; done; dbg_trace "it was dsimp simp" + | simp; done; dbg_trace "it was simp" + | tauto; done; dbg_trace "it was tauto" + | simp; tauto; done; dbg_trace "it was simp tauto" + | rfl; done; dbg_trace "it was rfl" + | norm_num; done; dbg_trace "it was norm_num" + | /-change (@Eq ℝ _ _);-/ linarith; done; dbg_trace "it was linarith" + -- | gcongr; done + | ring; done; dbg_trace "it was ring" + | trivial; done; dbg_trace "it was trivial" + -- | nlinarith; done + | fail "No, this is not obvious.")) + +-- @[BH, 1.5.6 (b)(ii)] +lemma ss (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] + [DirectSum.GCommRing π’œ] [DirectSum.Gmodule π’œ π“œ] (p : associatedPrimes (⨁ i, π’œ i) (⨁ i, π“œ i)) : true := by + sorry +-- Ideal.IsHomogeneous π’œ p + + + + +noncomputable def length ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊀} + + +def HomogeneousPrime { A Οƒ : Type _} [CommRing A] [SetLike Οƒ A] [AddSubmonoidClass Οƒ A] (π’œ : β„€ β†’ Οƒ) [GradedRing π’œ] (I : Ideal A):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous π’œ I) +def HomogeneousMax { A Οƒ : Type _} [CommRing A] [SetLike Οƒ A] [AddSubmonoidClass Οƒ A] (π’œ : β„€ β†’ Οƒ) [GradedRing π’œ] (I : Ideal A):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous π’œ I) + +--theorem monotone_stabilizes_iff_noetherian : +-- (βˆ€ f : β„• β†’o Submodule R M, βˆƒ n, βˆ€ m, n ≀ m β†’ f n = f m) ↔ IsNoetherian R M := by +-- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition] + +open GradedMonoid.GSmul +open DirectSum + +instance tada1 (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] + [DirectSum.Gmodule π’œ π“œ] (i : β„€ ) : SMul (π’œ 0) (π“œ i) + where smul x y := @Eq.rec β„€ (0+i) (fun a _ => π“œ a) (GradedMonoid.GSmul.smul x y) i (zero_add i) + +lemma mylem (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] + [h : DirectSum.Gmodule π’œ π“œ] (i : β„€) (a : π’œ 0) (m : π“œ i) : + of _ _ (a β€’ m) = of _ _ a β€’ of _ _ m := by + refine' Eq.trans _ (Gmodule.of_smul_of π’œ π“œ a m).symm + refine' of_eq_of_gradedMonoid_eq _ + exact Sigma.ext (zero_add _).symm <| eq_rec_heq _ _ + +instance tada2 (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] + [h : DirectSum.Gmodule π’œ π“œ] (i : β„€ ) : SMulWithZero (π’œ 0) (π“œ i) := by + letI := SMulWithZero.compHom (⨁ i, π“œ i) (of π’œ 0).toZeroHom + exact Function.Injective.smulWithZero (of π“œ i).toZeroHom Dfinsupp.single_injective (mylem π’œ π“œ i) + +instance tada3 (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] + [h : DirectSum.Gmodule π’œ π“œ] (i : β„€ ): Module (π’œ 0) (π“œ i) := by + letI := Module.compHom (⨁ j, π“œ j) (ofZeroRingHom π’œ) + exact Dfinsupp.single_injective.module (π’œ 0) (of π“œ i) (mylem π’œ π“œ i) + +noncomputable def hilbert_function (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] + [DirectSum.GCommRing π’œ] + [DirectSum.Gmodule π’œ π“œ] (hilb : β„€ β†’ β„€) := βˆ€ i, hilb i = (ENat.toNat (length (π’œ 0) (π“œ i))) + +noncomputable def dimensionring { A: Type _} + [CommRing A] := krullDim (PrimeSpectrum A) + + +noncomputable def dimensionmodule ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A β§Έ ((⊀ : Submodule A M).annihilator)) ) + +-- lemma graded_local (π’œ : β„€ β†’ Type _) [SetLike (⨁ i, π’œ i)] (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] +-- [DirectSum.GCommRing π’œ] +-- [DirectSum.Gmodule π’œ π“œ] (art: IsArtinianRing (π’œ 0)) (loc : LocalRing (π’œ 0)) : βˆƒ ( I : Ideal ((⨁ i, π’œ i))),(HomogeneousMax π’œ I) := sorry + + + + +@[simp] +def PolyType (f : β„€ β†’ β„€) (d : β„•) := βˆƒ Poly : Polynomial β„š, βˆƒ (N : β„€), βˆ€ (n : β„€), N ≀ n β†’ f n = Polynomial.eval (n : β„š) Poly ∧ d = Polynomial.degree Poly + +-- @[BH, 4.1.3] +theorem hilbert_polynomial (d : β„•) (d1 : 1 ≀ d) (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] +[DirectSum.GCommRing π’œ] +[DirectSum.Gmodule π’œ π“œ] (art: IsArtinianRing (π’œ 0)) (loc : LocalRing (π’œ 0)) +(fingen : IsNoetherian (⨁ i, π’œ i) (⨁ i, π“œ i)) +(findim : dimensionmodule (⨁ i, π’œ i) (⨁ i, π“œ i) = d) (hilb : β„€ β†’ β„€) + (Hhilb: hilbert_function π’œ π“œ hilb) +: PolyType hilb (d - 1) := by + sorry + +-- @ +lemma Graded_quotient (π’œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)][DirectSum.GCommRing π’œ] + : true := by + sorry + + +-- @Existence of a chain of submodules of graded submoduels of f.g graded R-mod M +lemma Exist_chain_of_graded_submodules (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] + [DirectSum.GCommRing π’œ] [DirectSum.Gmodule π’œ π“œ] (fingen : IsNoetherian (⨁ i, π’œ i) (⨁ i, π“œ i)) + : true := by + sorry +#print Exist_chain_of_graded_submodules +#print Finset \ No newline at end of file diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 59fd048..2111469 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -63,7 +63,7 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := apply height_le_of_le apply le_maximalIdeal exact I.2.1 - . simp + . simp only [height_le_krullDim] #check height_le_krullDim --some propositions that would be nice to be able to eventually @@ -135,7 +135,7 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim simp [field_prime_height_zero] -lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by +lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by by_contra x rw [Ring.not_isField_iff_exists_prime] at x obtain ⟨P, ⟨h1, primeP⟩⟩ := x @@ -156,9 +156,9 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) aesop contradiction -lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by +lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by constructor - Β· exact isField.dim_zero + Β· exact domain_dim_zero.isField Β· intro fieldD let h : Field D := IsField.toField fieldD exact dim_field_eq_zero diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean new file mode 100644 index 0000000..d3a272e --- /dev/null +++ b/CommAlg/monalisa.lean @@ -0,0 +1,140 @@ +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Finiteness +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.RingTheory.FiniteType +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Algebra.DirectSum.Ring +import Mathlib.RingTheory.Ideal.LocalRing +import Mathlib +import Mathlib.Algebra.MonoidAlgebra.Basic +import Mathlib.Data.Finset.Sort +import Mathlib.Order.Height +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Finiteness +import Mathlib.RingTheory.Ideal.Operations + + + + +noncomputable def length ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊀} + + +def HomogeneousPrime { A Οƒ : Type _} [CommRing A] [SetLike Οƒ A] [AddSubmonoidClass Οƒ A] (π’œ : β„€ β†’ Οƒ) [GradedRing π’œ] (I : Ideal A):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous π’œ I) + + +def HomogeneousMax { A Οƒ : Type _} [CommRing A] [SetLike Οƒ A] [AddSubmonoidClass Οƒ A] (π’œ : β„€ β†’ Οƒ) [GradedRing π’œ] (I : Ideal A):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous π’œ I) + +--theorem monotone_stabilizes_iff_noetherian : +-- (βˆ€ f : β„• β†’o Submodule R M, βˆƒ n, βˆ€ m, n ≀ m β†’ f n = f m) ↔ IsNoetherian R M := by +-- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition] + +open GradedMonoid.GSmul + +open DirectSum + +instance tada1 (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] + [DirectSum.Gmodule π’œ π“œ] (i : β„€ ) : SMul (π’œ 0) (π“œ i) + where smul x y := @Eq.rec β„€ (0+i) (fun a _ => π“œ a) (GradedMonoid.GSmul.smul x y) i (zero_add i) + +lemma mylem (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] + [h : DirectSum.Gmodule π’œ π“œ] (i : β„€) (a : π’œ 0) (m : π“œ i) : + of _ _ (a β€’ m) = of _ _ a β€’ of _ _ m := by + refine' Eq.trans _ (Gmodule.of_smul_of π’œ π“œ a m).symm + refine' of_eq_of_gradedMonoid_eq _ + exact Sigma.ext (zero_add _).symm <| eq_rec_heq _ _ + +instance tada2 (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] + [h : DirectSum.Gmodule π’œ π“œ] (i : β„€ ) : SMulWithZero (π’œ 0) (π“œ i) := by + letI := SMulWithZero.compHom (⨁ i, π“œ i) (of π’œ 0).toZeroHom + exact Function.Injective.smulWithZero (of π“œ i).toZeroHom Dfinsupp.single_injective (mylem π’œ π“œ i) + +instance tada3 (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] + [h : DirectSum.Gmodule π’œ π“œ] (i : β„€ ): Module (π’œ 0) (π“œ i) := by + letI := Module.compHom (⨁ j, π“œ j) (ofZeroRingHom π’œ) + exact Dfinsupp.single_injective.module (π’œ 0) (of π“œ i) (mylem π’œ π“œ i) + + -- (art: IsArtinianRing (π’œ 0)) (loc : LocalRing (π’œ 0)) + +noncomputable def dummyhil_function (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] + [DirectSum.GCommRing π’œ] + [DirectSum.Gmodule π’œ π“œ] (hilb : β„€ β†’ β„•βˆž) := βˆ€ i, hilb i = (length (π’œ 0) (π“œ i)) + + +lemma hilbertz (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] + [DirectSum.GCommRing π’œ] + [DirectSum.Gmodule π’œ π“œ] + (finlen : βˆ€ i, (length (π’œ 0) (π“œ i)) < ⊀ ) : β„€ β†’ β„€ := by + intro i + let h := dummyhil_function π’œ π“œ + simp at h + let n : β„€ β†’ β„• := fun i ↦ WithTop.untop _ (finlen i).ne + have hn : βˆ€ i, (n i : β„•βˆž) = length (π’œ 0) (π“œ i) := fun i ↦ WithTop.coe_untop _ _ + have' := hn i + exact ((n i) : β„€ ) + + +noncomputable def hilbert_function (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] + [DirectSum.GCommRing π’œ] + [DirectSum.Gmodule π’œ π“œ] (hilb : β„€ β†’ β„€) := βˆ€ i, hilb i = (ENat.toNat (length (π’œ 0) (π“œ i))) + + + +noncomputable def dimensionring { A: Type _} + [CommRing A] := krullDim (PrimeSpectrum A) + + +noncomputable def dimensionmodule ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A β§Έ ((⊀ : Submodule A M).annihilator)) ) + +-- lemma graded_local (π’œ : β„€ β†’ Type _) [SetLike (⨁ i, π’œ i)] (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] +-- [DirectSum.GCommRing π’œ] +-- [DirectSum.Gmodule π’œ π“œ] (art: IsArtinianRing (π’œ 0)) (loc : LocalRing (π’œ 0)) : βˆƒ ( I : Ideal ((⨁ i, π’œ i))),(HomogeneousMax π’œ I) := sorry + + +def PolyType (f : β„€ β†’ β„€) (d : β„•) := βˆƒ Poly : Polynomial β„š, βˆƒ (N : β„€), βˆ€ (n : β„€), N ≀ n β†’ f n = Polynomial.eval (n : β„š) Poly ∧ d = Polynomial.degree Poly + + + +theorem hilbert_polynomial (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] +[DirectSum.GCommRing π’œ] +[DirectSum.Gmodule π’œ π“œ] (art: IsArtinianRing (π’œ 0)) (loc : LocalRing (π’œ 0)) (fingen : IsNoetherian (⨁ i, π’œ i) (⨁ i, π“œ i)) +(findim : βˆƒ d : β„• , dimensionmodule (⨁ i, π’œ i) (⨁ i, π“œ i) = d):True := sorry + +-- Semiring A] + +-- variable [SetLike Οƒ A] \ No newline at end of file diff --git a/CommAlg/sameer(artinian-rings).lean b/CommAlg/sameer(artinian-rings).lean index e6bb667..417cc96 100644 --- a/CommAlg/sameer(artinian-rings).lean +++ b/CommAlg/sameer(artinian-rings).lean @@ -6,7 +6,9 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.RingTheory.DedekindDomain.DVR -lemma FieldisArtinian (R : Type _) [CommRing R] (IsField : ):= by sorry +lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) : + IsArtinianRing R := by sorry + lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R] @@ -47,8 +49,7 @@ lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R] lemma IsPrimeMaximal (R : Type _) [CommRing R] (P : Ideal R) (IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime P) : Ideal.IsMaximal P := by --- if R is Artinian and P is prime then R/P is Integral Domain --- which is Artinian Domain +-- if R is Artinian and P is prime then R/P is Artinian Domain -- Rβ§ΈP is a field by the above lemma -- P is maximal @@ -56,13 +57,13 @@ by have artRP : IsArtinianRing (Rβ§ΈP) := by exact isArtinianRing_of_quotient_of_artinian R P IsArt - + have artRPField : IsField (Rβ§ΈP) := by + exact ArtinianDomainIsField (Rβ§ΈP) artRP + + have h := Ideal.Quotient.maximal_of_isField P artRPField + exact h + -- Then R/I is Artinian -- have' : IsArtinianRing R ∧ Ideal.IsPrime I β†’ IsDomain (Rβ§ΈI) := by -- Rβ§ΈI.IsArtinian β†’ monotone_stabilizes_iff_artinian.Rβ§ΈI - - - - --- Use Stacks project proof since it's broken into lemmas diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index a9269a2..089c4b5 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -22,11 +22,7 @@ noncomputable instance : CompleteLattice (WithBot (β„•βˆž)) := WithBot.WithTop.c lemma dim_le_dim_polynomial_add_one [Nontrivial R] : krullDim R + 1 ≀ krullDim (Polynomial R) := sorry -- Others are working on it --- private lemma sum_succ_of_succ_sum {ΞΉ : Type} (a : β„•βˆž) [inst : Nonempty ΞΉ] : --- (⨆ (x : ΞΉ), a + 1) = (⨆ (x : ΞΉ), a) + 1 := by --- have : a + 1 = (⨆ (x : ΞΉ), a) + 1 := by rw [ciSup_const] --- have : a + 1 = (⨆ (x : ΞΉ), a + 1) := Eq.symm ciSup_const --- simp +lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≀ J) : height I ≀ height J := sorry -- Already done in main file lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : krullDim R + 1 = krullDim (Polynomial R) := by @@ -34,13 +30,33 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : constructor Β· exact dim_le_dim_polynomial_add_one Β· unfold krullDim - have htPBdd : βˆ€ (P : PrimeSpectrum (Polynomial R)), (height P: WithBot β„•βˆž) ≀ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by + have htPBdd : βˆ€ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot β„•βˆž) ≀ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by intro P - unfold height - sorry - have : (⨆ (I : PrimeSpectrum R), ↑(height I) + 1) ≀ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by - have : βˆ€ P : PrimeSpectrum R, ↑(height P) + 1 ≀ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := - fun _ ↦ add_le_add_right (le_iSup height _) 1 + have : βˆƒ (I : PrimeSpectrum R), (height P : WithBot β„•βˆž) ≀ ↑(height I + 1) := by + have : βˆƒ M, Ideal.IsMaximal M ∧ P.asIdeal ≀ M := by + apply exists_le_maximal + apply IsPrime.ne_top + apply P.IsPrime + obtain ⟨M, maxM, PleM⟩ := this + let P' : PrimeSpectrum (Polynomial R) := PrimeSpectrum.mk M (IsMaximal.isPrime maxM) + have PleP' : P ≀ P' := PleM + have : height P ≀ height P' := height_le_of_le PleP' + simp only [WithBot.coe_le_coe] + have : βˆƒ (I : PrimeSpectrum R), height P' ≀ height I + 1 := by + + sorry + obtain ⟨I, h⟩ := this + use I + exact ge_trans h this + obtain ⟨I, IP⟩ := this + have : (↑(height I + 1) : WithBot β„•βˆž) ≀ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by + apply @le_iSup (WithBot β„•βˆž) _ _ _ I + exact ge_trans this IP + have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot β„•βˆž) + 1) ≀ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by + have : βˆ€ P : PrimeSpectrum R, (height P : WithBot β„•βˆž) + 1 ≀ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := + fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot β„•βˆž) _ _ _ P) 1) apply iSup_le - exact this - sorry \ No newline at end of file + apply this + simp only [iSup_le_iff] + intro P + exact ge_trans oneOut (htPBdd P)