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

fixed some formatting

Browse source
This commit is contained in:
Andre 2023-06-16 00:28:44 -04:00
parent 85263016c1
commit de995bf2f3
1 changed files with 2 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

74
CommAlg/final_poly_type.lean
View file

@ -139,12 +139,6 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
rcases hh with ⟨N,ss⟩ rcases hh with ⟨N,ss⟩
sorry sorry
-- set_option pp.all true in
-- PolyType 0 = constant function
lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ),
(N ≤ n → f n = c) ∧ c ≠ 0) := by (N ≤ n → f n = c) ∧ c ≠ 0) := by
constructor constructor
@ -172,28 +166,16 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
=> by rw [(hh n).1 Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ)) => by rw [(hh n).1 Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ))
(c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩ (c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩
-- Δ of 0 times preserves the function -- Δ of 0 times preserves the function
lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by tauto lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by tauto
-- Δ of 1 times decreaes the polynomial type by one -- Δ of 1 times decreaes the polynomial type by one
lemma Δ_1 (f : ℤ → ℤ) (d : ℕ): d > 0 → PolyType f d → PolyType (Δ f 1) (d - 1) := by lemma Δ_1 (f : ℤ → ℤ) (d : ℕ): d > 0 → PolyType f d → PolyType (Δ f 1) (d - 1) := by
sorry sorry
lemma foo (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by lemma foo (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by
sorry sorry
-- Δ 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 foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ f d) 0):= by lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ f d) 0):= by
induction' d with d hd induction' d with d hd
@ -214,19 +196,7 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
tauto tauto
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 Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := by
intro h
have this : ∀ (d : ℕ), ∀ (f :ℤ → ℤ), (PolyType f d) → (PolyType (Δ f d) 0) := by
exact foofoo
specialize this d f
tauto
-- [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
@ -248,8 +218,6 @@ lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n
-- Induction step -- Induction step
· sorry · sorry
-- [BH, 4.1.2] (a) <= (b) -- [BH, 4.1.2] (a) <= (b)
-- f is of polynomial type d → Δ^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
lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), ((N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0)) := by lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), ((N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0)) := by
@ -263,41 +231,14 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃
exact this1 exact this1
end end
-- @Additive lemma of length for a SES -- @Additive lemma of length for a SES
-- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 -- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0
section section
-- variable {R M N : Type _} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
-- (f : M →[R] N)
open LinearMap open LinearMap
-- variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
-- noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
-- Definitiion of the length of a module -- 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' < ⊤} noncomputable def length (R M : Type _) [CommRing R] [AddCommGroup M] [Module R M] := Set.chainHeight {M' : Submodule R M | M' < ⊤}
#check length ℤ ℤ #check length ℤ ℤ
-- #eval length ℤ ℤ
-- @[ext]
-- structure SES (R : Type _) [CommRing R] where
-- A : Type _
-- B : Type _
-- C : Type _
-- f : A →ₗ[R] B
-- g : B →ₗ[R] C
-- left_exact : LinearMap.ker f = 0
-- middle_exact : LinearMap.range f = LinearMap.ker g
-- right_exact : LinearMap.range g = C
-- Definition of a SES (Short Exact Sequence) -- Definition of a SES (Short Exact Sequence)
-- @[ext] -- @[ext]
@ -309,10 +250,6 @@ structure SES {R A B C : Type _} [CommRing R] [AddCommGroup A] [AddCommGroup B]
middle_exact : LinearMap.range f = LinearMap.ker g middle_exact : LinearMap.range f = LinearMap.ker g
right_exact : LinearMap.range g = ⊤ right_exact : LinearMap.range g = ⊤
#check SES.right_exact
#check SES
-- Additive lemma -- 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] 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) (f : A →ₗ[R] B) (g : B →ₗ[R] C)
@ -321,11 +258,4 @@ lemma length_Additive (R A B C : Type _) [CommRing R] [AddCommGroup A] [AddCommG
rcases h with ⟨left_exact, middle_exact, right_exact⟩ rcases h with ⟨left_exact, middle_exact, right_exact⟩
sorry sorry
end section end section