SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

add statements

Browse source
This commit is contained in:
chelseaandmadrid 2023-06-14 09:14:47 -07:00
parent 4299cafebc
commit 3e4a8a5fca
2 changed files with 15 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
HilbertFunction.lean
View file

@ -106,7 +106,7 @@ end
-- @[BH, 4.1.3] when d ≥ 1 -- @[BH, 4.1.3] when d ≥ 1
theorem hilbert_polynomial (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] theorem hilbert_polynomial_ge1 (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.GCommRing 𝒜]
[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
@ -118,26 +118,31 @@ theorem hilbert_polynomial (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (
-- @[BH, 4.1.3] when d = 0 -- @[BH, 4.1.3] when d = 0
theorem hilbert_polynomial (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] theorem hilbert_polynomial_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.GCommRing 𝒜]
[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0) (hilb : ℤ → ℤ) (findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0) (hilb : ℤ → ℤ)
: true := by
sorry
-- @[BH, 1.5.6 (b)(ii)] -- @[BH, 1.5.6 (b)(ii)]
-- An associated prime of a graded R-Mod M is graded -- An associated prime of a graded R-Mod M is graded
lemma Associated_prime_of_graded_is_graded (𝒜 : ℤ → Type _) lemma Associated_prime_of_graded_is_graded
(𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _)
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
: true := by : true := by
-- Ideal.IsHomogeneous 𝒜 p
sorry sorry
-- Ideal.IsHomogeneous 𝒜 p
-- @Existence of a chain of submodules of graded submoduels of f.g graded R-mod M -- @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)] lemma Exist_chain_of_graded_submodules (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _)
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
: true := by : true := by
sorry sorry

2
PolyType.lean
View file

@ -128,7 +128,7 @@ def f (n : ℤ) := n
end section end section
-- 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