mirror of
https://github.com/GTBarkley/comm_alg.git
synced 2024-10-16 11:37:05 -05:00
Merge branch 'main' of github.com:GTBarkley/comm_alg into main
This commit is contained in:
leopoldmayer
commit
a2f28b85f8
5 changed files with 372 additions and 112 deletions
|
|
@ -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
|
|||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
285
CommAlg/final_poly_type.lean
Normal file
285
CommAlg/final_poly_type.lean
Normal 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
|
||||
|
|
@ -54,9 +54,20 @@ def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where
|
|||
rw [←mul_assoc, mul_comm s, mul_assoc]
|
||||
exact Ideal.mul_mem_left _ _ hs2
|
||||
|
||||
|
||||
theorem WF_interval_le_prime (I : Ideal R) (P : Ideal R) [P.IsPrime]
|
||||
(h : ∀ J ∈ (Set.Icc I P), J.IsPrime → J = P ):
|
||||
WellFounded ((· < ·) : (Set.Icc I P) → (Set.Icc I P) → Prop ) := sorry
|
||||
|
||||
protected lemma LocalRing.height_le_one_of_minimal_over_principle
|
||||
[LocalRing R] (q : PrimeSpectrum R) {x : R}
|
||||
[LocalRing R] {x : R}
|
||||
(h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :
|
||||
q = closedPoint R ∨ Ideal.height q = 0 := by
|
||||
|
||||
Ideal.height (closedPoint R) ≤ 1 := by
|
||||
-- by_contra hcont
|
||||
-- push_neg at hcont
|
||||
-- rw [Ideal.lt_height_iff'] at hcont
|
||||
-- rcases hcont with ⟨c, hc1, hc2, hc3⟩
|
||||
apply height_le_of_gt_height_lt
|
||||
intro p hp
|
||||
|
||||
sorry
|
||||
|
|
@ -43,7 +43,6 @@ class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop :=
|
|||
#check Ideal.IsLocallyNilpotent
|
||||
end Ideal
|
||||
|
||||
|
||||
-- Repeats the definition of the length of a module by Monalisa
|
||||
variable (R : Type _) [CommRing R] (I J : Ideal R)
|
||||
variable (M : Type _) [AddCommMonoid M] [Module R M]
|
||||
|
|
@ -71,7 +70,7 @@ lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R
|
|||
sorry
|
||||
-- how do I apply an instance to prove one direction?
|
||||
|
||||
|
||||
-- Stacks Lemma 5.9.2:
|
||||
-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
|
||||
-- Every closed subset of a noetherian space is a finite union
|
||||
-- of irreducible closed subsets.
|
||||
|
|
@ -169,7 +168,7 @@ abbrev Prod_of_localization :=
|
|||
|
||||
def foo : Prod_of_localization R →+* R where
|
||||
toFun := sorry
|
||||
invFun := sorry
|
||||
-- invFun := sorry
|
||||
left_inv := sorry
|
||||
right_inv := sorry
|
||||
map_mul' := sorry
|
||||
|
|
@ -198,6 +197,13 @@ lemma primes_of_Artinian_are_maximal
|
|||
lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
|
||||
IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 ↔ IsArtinianRing R := by
|
||||
constructor
|
||||
rintro ⟨RisNoetherian, dimzero⟩
|
||||
rw [ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
|
||||
let Z := irreducibleComponents (PrimeSpectrum R)
|
||||
have Zfinite : Set.Finite Z := by
|
||||
-- apply TopologicalSpace.NoetherianSpace.finite_irreducibleComponents ?_
|
||||
sorry
|
||||
|
||||
sorry
|
||||
intro RisArtinian
|
||||
constructor
|
||||
|
|
@ -207,81 +213,7 @@ lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
|
|||
intro I
|
||||
apply primes_of_Artinian_are_maximal
|
||||
|
||||
|
||||
|
||||
|
||||
-- Trash bin
|
||||
-- lemma Artinian_has_finite_max_ideal
|
||||
-- [IsArtinianRing R] : Finite (MaximalSpectrum R) := by
|
||||
-- by_contra infinite
|
||||
-- simp only [not_finite_iff_infinite] at infinite
|
||||
-- let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R)
|
||||
-- have m'inj := m'.injective
|
||||
-- let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal
|
||||
-- let f : ℕ → Ideal R := fun n : ℕ ↦ (m' n).asIdeal
|
||||
-- have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by
|
||||
-- apply IsArtinian.monotone_stabilizes {
|
||||
-- toFun := m''
|
||||
-- monotone' := sorry
|
||||
-- }
|
||||
-- cases' DCC with n DCCn
|
||||
-- specialize DCCn (n+1)
|
||||
-- specialize DCCn (Nat.le_succ n)
|
||||
-- let F : Fin (n + 1) → MaximalSpectrum R := fun k ↦ m' k
|
||||
-- have comaximal : ∀ (i j : Fin (n + 1)), (i ≠ j) → (F i).asIdeal ⊔ (F j).asIdeal =
|
||||
-- (⊤ : Ideal R) := by
|
||||
-- intro i j distinct
|
||||
-- apply Ideal.IsMaximal.coprime_of_ne
|
||||
-- exact (F i).IsMaximal
|
||||
-- exact (F j).IsMaximal
|
||||
-- have : (F i) ≠ (F j) := by
|
||||
-- apply Function.Injective.ne m'inj
|
||||
-- contrapose! distinct
|
||||
-- exact Fin.ext distinct
|
||||
-- intro h
|
||||
-- apply this
|
||||
-- exact MaximalSpectrum.ext _ _ h
|
||||
-- let CRT1 : (R ⧸ ⨅ (i : Fin (n + 1)), ((F i).asIdeal))
|
||||
-- ≃+* ((i : Fin (n + 1)) → R ⧸ (F i).asIdeal) :=
|
||||
-- Ideal.quotientInfRingEquivPiQuotient
|
||||
-- (fun i ↦ (F i).asIdeal) comaximal
|
||||
-- let CRT2 : (R ⧸ ⨅ (i : Fin (n + 1)), ((F i).asIdeal))
|
||||
-- ≃+* ((i : Fin (n + 1)) → R ⧸ (F i).asIdeal) :=
|
||||
-- Ideal.quotientInfRingEquivPiQuotient
|
||||
-- (fun i ↦ (F i).asIdeal) comaximal
|
||||
|
||||
|
||||
|
||||
|
||||
-- have comaximal : ∀ (n : ℕ) (i j : Fin n), (i ≠ j) → ((F n) i).asIdeal ⊔ ((F n) j).asIdeal =
|
||||
-- (⊤ : Ideal R) := by
|
||||
-- intro n i j distinct
|
||||
-- apply Ideal.IsMaximal.coprime_of_ne
|
||||
-- exact (F n i).IsMaximal
|
||||
-- exact (F n j).IsMaximal
|
||||
-- have : (F n i) ≠ (F n j) := by
|
||||
-- apply Function.Injective.ne m'inj
|
||||
-- contrapose! distinct
|
||||
-- exact Fin.ext distinct
|
||||
-- intro h
|
||||
-- apply this
|
||||
-- exact MaximalSpectrum.ext _ _ h
|
||||
-- let CRT : (n : ℕ) → (R ⧸ ⨅ (i : Fin n), ((F n) i).asIdeal)
|
||||
-- ≃+* ((i : Fin n) → R ⧸ ((F n) i).asIdeal) :=
|
||||
-- fun n ↦ Ideal.quotientInfRingEquivPiQuotient
|
||||
-- (fun i ↦ (F n i).asIdeal) (comaximal n)
|
||||
-- have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by
|
||||
-- apply IsArtinian.monotone_stabilizes {
|
||||
-- toFun := m''
|
||||
-- monotone' := sorry
|
||||
-- }
|
||||
-- cases' DCC with n DCCn
|
||||
-- specialize DCCn (n+1)
|
||||
-- specialize DCCn (Nat.le_succ n)
|
||||
-- let CRT1 := CRT n
|
||||
-- let CRT2 := CRT (n + 1)
|
||||
|
||||
|
||||
-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -112,31 +112,32 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
|
|||
/-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭`
|
||||
with length `n + 1`. -/
|
||||
lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
|
||||
height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
|
||||
rcases n with _ | n
|
||||
. constructor <;> intro h <;> exfalso
|
||||
n < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
|
||||
match n with
|
||||
| ⊤ =>
|
||||
constructor <;> intro h <;> exfalso
|
||||
. exact (not_le.mpr h) le_top
|
||||
. tauto
|
||||
have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
|
||||
symm
|
||||
show (n + 1 ≤ m ↔ _ )
|
||||
apply ENat.add_one_le_iff
|
||||
exact ENat.coe_ne_top _
|
||||
rw [this]
|
||||
unfold Ideal.height
|
||||
show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
|
||||
rw [{J | J < 𝔭}.le_chainHeight_iff]
|
||||
show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
|
||||
constructor <;> rintro ⟨c, hc⟩ <;> use c
|
||||
. tauto
|
||||
. change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
|
||||
norm_cast at hc
|
||||
tauto
|
||||
| (n : ℕ) =>
|
||||
have (m : ℕ∞) : n < m ↔ (n + 1 : ℕ∞) ≤ m := by
|
||||
symm
|
||||
show (n + 1 ≤ m ↔ _ )
|
||||
apply ENat.add_one_le_iff
|
||||
exact ENat.coe_ne_top _
|
||||
rw [this]
|
||||
unfold Ideal.height
|
||||
show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
|
||||
rw [{J | J < 𝔭}.le_chainHeight_iff]
|
||||
show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
|
||||
constructor <;> rintro ⟨c, hc⟩ <;> use c
|
||||
. tauto
|
||||
. change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
|
||||
norm_cast at hc
|
||||
tauto
|
||||
|
||||
/-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/
|
||||
lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
|
||||
height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
|
||||
show (_ < _) ↔ _
|
||||
(n : WithBot ℕ∞) < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
|
||||
rw [WithBot.coe_lt_coe]
|
||||
exact lt_height_iff'
|
||||
|
||||
|
|
@ -198,7 +199,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
|
|||
rw [hcontr] at h
|
||||
exact h h𝔪.1
|
||||
use 𝔪p
|
||||
show (_ : WithBot ℕ∞) > (0 : ℕ∞)
|
||||
show (0 : ℕ∞) < (_ : WithBot ℕ∞)
|
||||
rw [lt_height_iff'']
|
||||
use [I]
|
||||
constructor
|
||||
|
|
@ -209,7 +210,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
|
|||
rwa [hI']
|
||||
. simp
|
||||
. contrapose! h
|
||||
change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h
|
||||
change (0 : ℕ∞) < (_ : WithBot ℕ∞) at h
|
||||
rw [lt_height_iff''] at h
|
||||
obtain ⟨c, _, hc2, hc3⟩ := h
|
||||
norm_cast at hc3
|
||||
|
|
|
|||
Loading…
Reference in a new issue