diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean index 591c6cc..eff9302 100644 --- a/CommAlg/final_hil_pol.lean +++ b/CommAlg/final_hil_pol.lean @@ -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) @@ -44,7 +43,7 @@ noncomputable def length ( A : Type _) (M : Type _) [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊀} -- Make instance of M_i being an R_0-module -instance tada1 (π’œ : β„€ β†’ Type _) (π“œ : β„€ β†’ Type _) [βˆ€ i, AddCommGroup (π’œ i)] [βˆ€ i, AddCommGroup (π“œ i)] [DirectSum.GCommRing π’œ] +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) @@ -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 + + + + + + diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean new file mode 100644 index 0000000..dcb0e70 --- /dev/null +++ b/CommAlg/final_poly_type.lean @@ -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 \ No newline at end of file