Updated PolyType

This commit is contained in:
chelseaandmadrid 2023-06-14 20:51:45 -07:00
parent ac0a660641
commit 191e02e984
2 changed files with 52 additions and 23 deletions

View file

@ -29,11 +29,13 @@ macro "obviously" : tactic =>
open GradedMonoid.GSmul
open DirectSum
-- @Definitions (to be classified) -- @Definitions (to be classified)
section section
open GradedMonoid.GSmul
open DirectSum
-- Definition of polynomail of type d -- Definition of polynomail of type d
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
@ -78,7 +80,6 @@ end
-- Definition of homogeneous ideal -- Definition of homogeneous ideal
def Ideal.IsHomogeneous' (𝒜 : → Type _) def Ideal.IsHomogeneous' (𝒜 : → Type _)
[∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
@ -99,10 +100,30 @@ def HomogeneousMax (𝒜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [Direc
end end
-- Each component of a graded ring is an additive subgroup
def Component_of_graded_as_addsubgroup (𝒜 : → Type _)
[∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ) : AddSubgroup (𝒜 i) := by
sorry
-- @Quotient of a graded ring R by a graded ideal p is a graded R-Mod, preserving each component
instance Quotient_of_graded_is_graded
(𝒜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
: DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by
sorry
-- If A_0 is Artinian and local, then A is graded local -- If A_0 is Artinian and local, then A is graded local
lemma Graded_local_if_zero_component_Artinian_and_local (𝒜 : → Type _) (𝓜 : → Type _) lemma Graded_local_if_zero_component_Artinian_and_local (𝒜 : → Type _) (𝓜 : → Type _)
[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := sorry [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := by
sorry
@ -159,25 +180,11 @@ lemma Associated_prime_of_graded_is_graded
sorry sorry
-- instance gyhoiu
-- (𝒜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
-- (p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
-- : (𝒫 : → Type _) [∀ i, AddCommGroup (𝒫 i)] [DirectSum.GCommRing 𝒫] → Gmodule (⊕ i, 𝒜 i) := by
-- sorry
-- Each component of a graded ring is an additive subgroup
def Component_of_graded_as_addsubgroup (𝒜 : → Type _)
[∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ) : AddSubgroup (𝒜 i) := by def Graded_homo : true := by
sorry sorry
-- @Quotient of a graded ring R by a graded ideal p is a graded R-Mod, preserving each component
instance Quotient_of_graded_is_graded
(𝒜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
: DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by
sorry

View file

@ -110,7 +110,7 @@ def f (n : ) := n
end section end section
-- (NO need to prove) Constant polynomial function = constant function -- (NO NEED TO PROVE) Constant polynomial function = constant function
lemma Poly_constant (F : Polynomial ) (c : ) : lemma Poly_constant (F : Polynomial ) (c : ) :
(F = Polynomial.C c) ↔ (∀ r : , (Polynomial.eval r F) = c) := by (F = Polynomial.C c) ↔ (∀ r : , (Polynomial.eval r F) = c) := by
constructor constructor
@ -123,10 +123,20 @@ lemma Poly_constant (F : Polynomial ) (c : ) :
· sorry · sorry
-- Shifting doesn't change the polynomial type -- Shifting doesn't change the polynomial type
lemma Poly_shifting (f : ) (g : ) (hf : PolyType f d) (s : ) (hfg : ∀ (n : ), f (n + s) = g (n)) : PolyType g d := by lemma Poly_shifting (f : ) (g : ) (hf : PolyType f d) (s : ) (hfg : ∀ (n : ), f (n + s) = g (n)) : PolyType g d := by
simp only [PolyType]
rcases hf with ⟨F, hh⟩
rcases hh with ⟨N,ss⟩
sorry sorry
-- PolyType 0 = constant function -- PolyType 0 = constant function
lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N : ), ∀ (n : ), (N ≤ n → f n = c) ∧ c ≠ 0) := by lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N : ), ∀ (n : ), (N ≤ n → f n = c) ∧ c ≠ 0) := by
constructor constructor
@ -188,6 +198,14 @@ lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N :
· sorry · sorry
-- apply Polynomial.degree_C c -- apply Polynomial.degree_C c
-- Δ of 0 times preserve the function
lemma Δ_0 (f : ) : (Δ f 0) = f := by
tauto
-- Δ of d times maps polynomial of degree d to polynomial of degree 0 -- Δ 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 lemma Δ_PolyType_d_to_PolyType_0 (f : ) (d : ): PolyType f d → PolyType (Δ f d) 0 := by
intro h intro h
@ -203,6 +221,10 @@ lemma Δ_PolyType_d_to_PolyType_0 (f : ) (d : ): PolyType f d →
sorry sorry
· sorry · sorry
-- [BH, 4.1.2] (a) => (b) -- [BH, 4.1.2] (a) => (b)
-- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d -- Δ^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 lemma a_to_b (f : ) (d : ) : (∃ (c : ), ∃ (N : ), ∀ (n : ), ((N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0)) → PolyType f d := by