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

Merge pull request #82 from GTBarkley/monalisa

Browse source 
Monalisa
This commit is contained in:
ah1112 2023-06-16 00:48:58 -04:00 committed by GitHub
commit c92b111565
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 325 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
CommAlg/final_hil_pol.lean
View file

@ -6,7 +6,6 @@ import Mathlib.RingTheory.Artinian
import Mathlib.Order.Height
-- Setting for "library_search"
set_option maxHeartbeats 0
macro "ls" : tactic => `(tactic|library_search)
@ -109,8 +108,7 @@ instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GComm
sorry)
class StandardGraded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : Prop where
class StandardGraded (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : Prop where
gen_in_first_piece :
Algebra.adjoin (𝒜 0) (DirectSum.of _ 1 : 𝒜 1 →+ ⨁ i, 𝒜 i).range = (⊤ : Subalgebra (𝒜 0) (⨁ i, 𝒜 i))
@ -124,7 +122,25 @@ def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _)
def graded_morphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _)
[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] (f : (⨁ i, 𝓜 i) → (⨁ i, 𝓝 i)) : ∀ i, ∀ (r : 𝓜 i), ∀ j, (j ≠ i → f (DirectSum.of _ i r) j = 0) ∧ (IsLinearMap (⨁ i, 𝒜 i) f) := by sorry
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
(f : (⨁ i, 𝓜 i) →ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i))
: ∀ i, ∀ (r : 𝓜 i), ∀ j, (j ≠ i → f (DirectSum.of _ i r) j = 0)
∧ (IsLinearMap (⨁ i, 𝒜 i) f) := by
sorry
#check graded_morphism
def graded_isomorphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _)
[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
(f : (⨁ i, 𝓜 i) →ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i))
: IsLinearEquiv f := by
sorry
-- f ∈ (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)
-- LinearEquivClass f (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) (⨁ i, 𝓝 i)
-- #print IsLinearEquiv
#check graded_isomorphism
def graded_submodule
@ -143,6 +159,7 @@ end
-- @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 𝒜]
@ -150,6 +167,13 @@ instance Quotient_of_graded_is_graded
: DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by
sorry
--
lemma sss
: true := by
sorry
-- If A_0 is Artinian and local, then A is graded local
lemma Graded_local_if_zero_component_Artinian_and_local (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _)
@ -189,10 +213,11 @@ lemma Associated_prime_of_graded_is_graded
-- If M is a finite graed R-Mod of dimension d ≥ 1, then the Hilbert function H(M, n) is of polynomial type (d - 1)
theorem Hilbert_polynomial_d_ge_1 (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜]
[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (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
@ -203,7 +228,7 @@ theorem Hilbert_polynomial_d_ge_1_reduced
(d : ℕ) (d1 : 1 ≤ d)
(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜]
[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d)
(hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb)
@ -217,7 +242,7 @@ theorem Hilbert_polynomial_d_ge_1_reduced
-- If M is a finite graed R-Mod of dimension zero, then the Hilbert function H(M, n) = 0 for n >> 0
theorem Hilbert_polynomial_d_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜]
[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0)
(hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb)
@ -230,7 +255,7 @@ theorem Hilbert_polynomial_d_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [
theorem Hilbert_polynomial_d_0_reduced
(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜]
[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0)
(hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb)
@ -252,6 +277,12 @@ theorem Hilbert_polynomial_d_0_reduced

285
CommAlg/final_poly_type.lean Normal file
View file

@ -0,0 +1,285 @@
import Mathlib.Order.Height
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
-- 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."))
-- Testing of Polynomial
section Polynomial
noncomputable section
#check Polynomial
#check Polynomial (ℚ)
#check Polynomial.eval
example (f : Polynomial ℚ) (hf : f = Polynomial.C (1 : ℚ)) : Polynomial.eval 2 f = 1 := by
have : ∀ (q : ℚ), Polynomial.eval q f = 1 := by
sorry
obviously
-- example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : Polynomial.eval 2 f = 4 := by
-- sorry
-- degree of a constant function is ⊥ (is this same as -1 ???)
#print Polynomial.degree_zero
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
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 another direction) 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
-- 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
simp only [PolyType]
rcases hf with ⟨F, hh⟩
rcases hh with ⟨N,ss⟩
sorry
-- PolyType 0 = constant function
lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ),
(N ≤ n → f n = c)) ∧ c ≠ 0) := by
constructor
· rintro ⟨Poly, ⟨N, ⟨H1, H2⟩⟩⟩
have this1 : Polynomial.degree Poly = 0 := by rw [← H2]; rfl
have this2 : ∃ (c : ℤ), Poly = Polynomial.C (c : ℚ) := by
have HH : ∃ (c : ℚ), Poly = Polynomial.C (c : ℚ) :=
⟨Poly.coeff 0, Polynomial.eq_C_of_degree_eq_zero (by rw[← H2]; rfl)⟩
cases' HH with c HHH
have HHHH : ∃ (d : ℤ), d = c :=
⟨f N, by simp [(Poly_constant Poly c).mp HHH N, H1 N (le_refl N)]⟩
cases' HHHH with d H5; exact ⟨d, by rw[← H5] at HHH; exact HHH⟩
rcases this2 with ⟨c, hthis2⟩
use c; use N; intro n
constructor
· have this4 : Polynomial.eval (n : ℚ) Poly = c := by
rw [hthis2]; simp only [map_intCast, Polynomial.eval_int_cast]
exact fun HH1 => Iff.mp (Rat.coe_int_inj (f n) c) (by rw [←this4, H1 n HH1])
· intro c0
simp only [hthis2, c0, Int.cast_zero, map_zero, Polynomial.degree_zero]
at this1
· rintro ⟨c, N, hh⟩
have H2 : (c : ℚ) ≠ 0 := by simp only [ne_eq, Int.cast_eq_zero]; exact (hh 0).2
exact ⟨Polynomial.C (c : ℚ), N, fun n Nn
=> by rw [(hh n).1 Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ))
(c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩
-- Δ of 0 times preserves the function
lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by tauto
-- Δ of 1 times decreaes the polynomial type by one
lemma Δ_1 (f : ℤ → ℤ) (d : ℕ): d > 0 → PolyType f d → PolyType (Δ f 1) (d - 1) := by
sorry
-- Δ of d times maps polynomial of degree d to polynomial of degree 0
lemma Δ_1_s_equiv_Δ_s_1 (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by
sorry
lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ f d) 0):= by
induction' d with d hd
· intro f h
rw [Δ_0]
tauto
· intro f hf
have this1 : PolyType f (d + 1) := by tauto
have this2 : PolyType (Δ f (d + 1)) 0 := by
have this3 : PolyType (Δ f 1) d := by
have this4 : d + 1 > 0 := by positivity
have this5 : (d + 1) > 0 → PolyType f (d + 1) → PolyType (Δ f 1) d := Δ_1 f (d + 1)
exact this5 this4 this1
clear hf
specialize hd (Δ f 1)
have this4 : PolyType (Δ (Δ f 1) d) 0 := by tauto
rw [Δ_1_s_equiv_Δ_s_1] at this4
tauto
tauto
lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := fun h => (foofoo d f) h
lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d) := by
induction' d with d hd
-- Base case
· intro f
intro h
rcases h with ⟨c, N, hh⟩
rw [PolyType_0]
use c
use N
tauto
-- Induction step
· intro f
intro h
rcases h with ⟨c, N, h⟩
have this : PolyType f (d + 1) := by
sorry
tauto
-- [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
sorry
-- 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
-- -- Base case
-- · rw [PolyType_0]
-- use c
-- use N
-- tauto
-- -- Induction step
-- · 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 Δ_d_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
-- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0
section
open LinearMap
-- 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 ℤ ℤ
-- 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 = ⊤
-- 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
end section