Merge pull request #62 from GTBarkley/monalisa

Monalisa
This commit is contained in:
ah1112 2023-06-14 16:22:07 -04:00 committed by GitHub
commit 4e38ef0a73
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -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.KrullDimension
import Mathlib.Order.JordanHolder
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic 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.Algebra.Module.GradedModule
import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Ideal.AssociatedPrime
import Mathlib.RingTheory.Noetherian
import Mathlib.RingTheory.Artinian 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 _) -- Setting for "library_search"
[CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < } set_option maxHeartbeats 0
macro "ls" : tactic => `(tactic|library_search)
def Ideal.IsHomogeneous' (𝒜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] -- New tactic "obviously"
[DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)) := ∀ (i : ) ⦃r : (⨁ i, 𝒜 i)⦄, r ∈ I → DirectSum.of _ i ( r i : 𝒜 i) ∈ I 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 : -- example (f : ) (hf : ∀ x, f x = x ^ 2) : Polynomial.eval 2 f = 4 := by
-- (∀ f : →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by -- sorry
-- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition]
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
-- Treat polynomial f ∈ [X] as a function f :
#check CoeFun
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 _) end section
[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
-- @[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 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
theorem hilbert_polynomial (d : ) (d1 : 1 ≤ d) (𝒜 : → Type _) (𝓜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] -- Definition of a SES (Short Exact Sequence)
[DirectSum.GCommRing 𝒜] -- @[ext]
[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) structure SES {R A B C : Type _} [CommRing R] [AddCommGroup A] [AddCommGroup B]
(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) [AddCommGroup C] [Module R A] [Module R B] [Module R C]
(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d) (hilb : ) (f : A →ₗ[R] B) (g : B →ₗ[R] C)
(Hhilb: hilbert_function 𝒜 𝓜 hilb) where
: PolyType hilb (d - 1) := by 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 sorry
end section
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)