diff --git a/CommAlg/poly_type.lean b/CommAlg/poly_type.lean index 357578b..ab3b4c1 100644 --- a/CommAlg/poly_type.lean +++ b/CommAlg/poly_type.lean @@ -1,105 +1,299 @@ +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.Order.Height +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' < ⊀} +-- Setting for "library_search" +set_option maxHeartbeats 0 +macro "ls" : tactic => `(tactic|library_search) - def Ideal.IsHomogeneous' (π’œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] - [DirectSum.GCommRing π’œ] (I : Ideal (⨁ i, π’œ i)) := βˆ€ (i : β„€ ) ⦃r : (⨁ i, π’œ i)⦄, r ∈ I β†’ DirectSum.of _ i ( r i : π’œ i) ∈ I +-- 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.")) -def HomogeneousPrime (π’œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [DirectSum.GCommRing π’œ] (I : Ideal (⨁ i, π’œ i)):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous' π’œ I) +-- Testing of Polynomial +section Polynomial +variable [Semiring β„•] +variable [Semiring β„€] +variable [Semiring β„š] +noncomputable section +#check Polynomial +#check Polynomial (β„š) +#check Polynomial.eval -def HomogeneousMax (π’œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [DirectSum.GCommRing π’œ] (I : Ideal (⨁ i, π’œ i)):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous' π’œ I) +example (f : Polynomial β„š) (hf : f = Polynomial.C (1 : β„š)) : Polynomial.eval 2 f = 1 := by + have : βˆ€ (q : β„š), Polynomial.eval q f = 1 := by + sorry + obviously ---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] +-- example (f : β„€ β†’ β„€) (hf : βˆ€ x, f x = x ^ 2) : Polynomial.eval 2 f = 4 := by +-- sorry -open GradedMonoid.GSmul +-- degree of a constant function is βŠ₯ (is this same as -1 ???) +#print Polynomial.degree_zero -open DirectSum +def F : Polynomial β„š := Polynomial.C (2 : β„š) +#print F +#check F +#check Polynomial.degree F +#check Polynomial.degree 0 +#check WithBot β„• +-- #eval Polynomial.degree F +#check Polynomial.eval 1 F +example : Polynomial.eval (100 : β„š) F = (2 : β„š) := by + refine Iff.mpr (Rat.ext_iff (Polynomial.eval 100 F) 2) ?_ + simp only [Rat.ofNat_num, Rat.ofNat_den] + rw [F] + simp - -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)) ) - --- (βˆƒ (i : β„€ ), βˆƒ (x : π’œ i), p = (Submodule.span (⨁ i, π’œ i) {x}).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 +-- Treat polynomial f ∈ β„š[X] as a function f : β„š β†’ β„š +#check CoeFun -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 + +end section + +-- @[BH, 4.1.2] +-- All the polynomials are in β„š[X], all the functions are considered as β„€ β†’ β„€ +noncomputable section +-- Polynomial type of degree d +@[simp] +def PolyType (f : β„€ β†’ β„€) (d : β„•) := βˆƒ Poly : Polynomial β„š, βˆƒ (N : β„€), βˆ€ (n : β„€), N ≀ n β†’ f n = Polynomial.eval (n : β„š) Poly ∧ d = Polynomial.degree Poly +section +-- structure PolyType (f : β„€ β†’ β„€) where +-- Poly : Polynomial β„€ +-- d : +-- N : β„€ +-- Poly_equal : βˆ€ n ∈ β„€ β†’ f n = Polynomial.eval n : β„€ Poly + +#check PolyType + +example (f : β„€ β†’ β„€) (hf : βˆ€ x, f x = x ^ 2) : PolyType f 2 := by + unfold PolyType + sorry + -- use Polynomial.monomial (2 : β„€) (1 : β„€) + -- have' := hf 0; ring_nf at this + -- exact this + +end section + +-- Ξ” operator (of d times) +@[simp] +def Ξ” : (β„€ β†’ β„€) β†’ β„• β†’ (β„€ β†’ β„€) + | f, 0 => f + | f, d + 1 => fun (n : β„€) ↦ (Ξ” f d) (n + 1) - (Ξ” f d) (n) +section +-- def Ξ” (f : β„€ β†’ β„€) (d : β„•) := fun (n : β„€) ↦ f (n + 1) - f n +-- def add' : β„• β†’ β„• β†’ β„• +-- | 0, m => m +-- | n+1, m => (add' n m) + 1 +-- #eval add' 5 10 +#check Ξ” +def f (n : β„€) := n +#eval (Ξ” f 1) 100 +-- #check (by (show_term unfold Ξ”) : Ξ” f 0=0) +end section + + +-- (NO need to prove) Constant polynomial function = constant function +lemma Poly_constant (F : Polynomial β„š) (c : β„š) : + (F = Polynomial.C c) ↔ (βˆ€ r : β„š, (Polynomial.eval r F) = c) := by + constructor + Β· intro h + rintro r + refine Iff.mpr (Rat.ext_iff (Polynomial.eval r F) c) ?_ + simp only [Rat.ofNat_num, Rat.ofNat_den] + rw [h] + simp + Β· sorry + +-- PolyType 0 = constant function +lemma PolyType_0 (f : β„€ β†’ β„€) : (PolyType f 0) ↔ (βˆƒ (c : β„€), βˆƒ (N : β„€), βˆ€ (n : β„€), (N ≀ n β†’ f n = c) ∧ c β‰  0) := by + constructor + Β· intro h + rcases h with ⟨Poly, hN⟩ + rcases hN with ⟨N, hh⟩ + have H1 := Ξ» n hn => (hh n hn).left + have H2 := Ξ» n hn => (hh n hn).right + clear hh + specialize H2 (N + 1) + have this1 : Polynomial.degree Poly = 0 := by + have : N ≀ N + 1 := by + dsimp + simp + tauto + have this2 : βˆƒ (c : β„€), Poly = Polynomial.C (c : β„š) := by + have HH : βˆƒ (c : β„š), Poly = Polynomial.C (c : β„š) := by + use Poly.coeff 0 + apply Polynomial.eq_C_of_degree_eq_zero + exact this1 + cases' HH with c HHH + have HHHH : βˆƒ (d : β„€), d = c := by + sorry + cases' HHHH with d H5 + use d + rw [H5] + exact HHH + clear this1 + rcases this2 with ⟨c, hthis2⟩ + use c + use N + intro n + specialize H1 n + constructor + Β· intro HH1 + have this3 : f n = Polynomial.eval (n : β„š) Poly := by + tauto + have this4 : Polynomial.eval (n : β„š) Poly = c := by + rw [hthis2] + dsimp + simp + have this5 : f n = (c : β„š) := by + rw [←this4, this3] + exact Iff.mp (Rat.coe_int_inj (f n) c) this5 + Β· sorry + + + Β· intro h + rcases h with ⟨c, N, aaa⟩ + let (Poly : Polynomial β„š) := Polynomial.C (c : β„š) + use Poly + use N + intro n Nn + specialize aaa n + have this1 : c β‰  0 β†’ f n = c := by + tauto + constructor + Β· sorry + Β· sorry + -- apply Polynomial.degree_C c + +-- Ξ” of d times maps polynomial of degree d to polynomial of degree 0 +lemma Ξ”_PolyType_d_to_PolyType_0 (f : β„€ β†’ β„€) (d : β„•): PolyType f d β†’ PolyType (Ξ” f d) 0 := by + intro h + rcases h with ⟨Poly, hN⟩ + rcases hN with ⟨N, hh⟩ + have H1 := Ξ» n hn => (hh n hn).left + have H2 := Ξ» n hn => (hh n hn).right + clear hh + have HH2 : d = Polynomial.degree Poly := by + sorry + induction' d with d hd + Β· rw [PolyType_0] + sorry + Β· sorry + +-- [BH, 4.1.2] (a) => (b) +-- Ξ”^d f (n) = c for some nonzero integer c for n >> 0 β†’ f is of polynomial type d +lemma a_to_b (f : β„€ β†’ β„€) (d : β„•) : (βˆƒ (c : β„€), βˆƒ (N : β„€), βˆ€ (n : β„€), ((N ≀ n β†’ (Ξ” f d) (n) = c) ∧ c β‰  0)) β†’ PolyType f d := by + intro h + rcases h with ⟨c, N, hh⟩ + have H1 := Ξ» n => (hh n).left + have H2 := Ξ» n => (hh n).right + clear hh + have H2 : c β‰  0 := by + tauto + induction' d with d hd + Β· rw [PolyType_0] + use c + use N + tauto + Β· sorry + +-- [BH, 4.1.2] (a) <= (b) +-- f is of polynomial type d β†’ Ξ”^d f (n) = c for some nonzero integer c for n >> 0 +lemma b_to_a (f : β„€ β†’ β„€) (d : β„•) : PolyType f d β†’ (βˆƒ (c : β„€), βˆƒ (N : β„€), βˆ€ (n : β„€), ((N ≀ n β†’ (Ξ” f d) (n) = c) ∧ c β‰  0)) := by + intro h + have : PolyType (Ξ” f d) 0 := by + apply Ξ”_PolyType_d_to_PolyType_0 + exact h + have this1 : (βˆƒ (c : β„€), βˆƒ (N : β„€), βˆ€ (n : β„€), ((N ≀ n β†’ (Ξ” f d) n = c) ∧ c β‰  0)) := by + rw [←PolyType_0] + exact this + exact this1 +end + +-- @Additive lemma of length for a SES +section +-- variable {R M N : Type _} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] +-- (f : M β†’[R] N) +open LinearMap +-- variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M] +-- noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊀} + + +-- Definitiion of the length of a module +noncomputable def length (R M : Type _) [CommRing R] [AddCommGroup M] [Module R M] := Set.chainHeight {M' : Submodule R M | M' < ⊀} +#check length β„€ β„€ +-- #eval length β„€ β„€ + + +-- @[ext] +-- structure SES (R : Type _) [CommRing R] where +-- A : Type _ +-- B : Type _ +-- C : Type _ +-- f : A β†’β‚—[R] B +-- g : B β†’β‚—[R] C +-- left_exact : LinearMap.ker f = 0 +-- middle_exact : LinearMap.range f = LinearMap.ker g +-- right_exact : LinearMap.range g = C + + + +-- Definition of a SES (Short Exact Sequence) +-- @[ext] +structure SES {R A B C : Type _} [CommRing R] [AddCommGroup A] [AddCommGroup B] + [AddCommGroup C] [Module R A] [Module R B] [Module R C] + (f : A β†’β‚—[R] B) (g : B β†’β‚—[R] C) + where + left_exact : LinearMap.ker f = βŠ₯ + middle_exact : LinearMap.range f = LinearMap.ker g + right_exact : LinearMap.range g = ⊀ + +#check SES.right_exact +#check SES + + +-- Additive lemma +lemma length_Additive (R A B C : Type _) [CommRing R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] + (f : A β†’β‚—[R] B) (g : B β†’β‚—[R] C) + : (SES f g) β†’ ((length R A) + (length R C) = (length R B)) := by + intro h + rcases h with ⟨left_exact, middle_exact, right_exact⟩ sorry - -theorem hilbert_polynomial_0 (π’œ : β„€ β†’ 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) = 0) (hilb : β„€ β†’ β„€) -: true := by - sorry - -lemma ass_graded (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) -[βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] -[DirectSum.GCommRing π’œ] [DirectSum.Gmodule π’œ π“œ] -(p : associatedPrimes (⨁ i, π’œ i) (⨁ i, π“œ i)) : (HomogeneousMax π’œ p) := by -sorry - -lemma Associated_prime_of_graded_is_graded -(π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) -[βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] -[DirectSum.GCommRing π’œ] [DirectSum.Gmodule π’œ π“œ] -(p : associatedPrimes (⨁ i, π’œ i) (⨁ i, π“œ i)) - : (Ideal.IsHomogeneous' π’œ p) ∧ ((βˆƒ (i : β„€ ), βˆƒ (x : π’œ i), p = (Submodule.span (⨁ i, π’œ i) {DirectSum.of x i}).annihilator)) := by - sorry - - -def standard_graded (π’œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [DirectSum.GCommRing π’œ] (I : Ideal (⨁ i, π’œ i)) := (⨁ i, π’œ i) +end section