From bbaf7e66447e3d38c8df4b8181002c54c459106e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 2 Jul 2020 18:44:19 +0100 Subject: [PATCH] =?UTF-8?q?Replace=20=E2=84=A4=20with=20an=20extra=20type?= =?UTF-8?q?=20parameter.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For now, we probably want to build on top of this limited to ℕ anyway. --- src/geometric_algebra/nursery/graded.lean | 41 +++++++++++++---------- 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/src/geometric_algebra/nursery/graded.lean b/src/geometric_algebra/nursery/graded.lean index 1fd9f44ee..9c478ffa1 100644 --- a/src/geometric_algebra/nursery/graded.lean +++ b/src/geometric_algebra/nursery/graded.lean @@ -3,15 +3,17 @@ import algebra.group import linear_algebra.tensor_product import tactic.ring -universes u +universes u v open_locale big_operators open_locale classical open finset class graded_module_components + -- the indices of the grades, typically ℕ + {ι : Type u} [has_zero ι] -- a type for each grade. - (A : ℤ → Type u) + (A : ι → Type u) := -- (A 0) is the scalar type [zc: comm_ring (A 0)] @@ -25,9 +27,9 @@ attribute [instance] graded_module_components.b attribute [instance] graded_module_components.c namespace graded_module_components - variables {A : ℤ → Type u} + variables {ι : Type u} [has_zero ι] {A : ι → Type u} /-- objects are coercible only if they have the same grade-/ - instance has_coe (r s : ℕ) (h: r = s) : has_coe (A r) (A s) := { coe := by {subst h, exact id}} + instance has_coe (r s : ι) (h: r = s) : has_coe (A r) (A s) := { coe := by {subst h, exact id}} end graded_module_components -- needed for the definition of `select` @@ -35,11 +37,13 @@ attribute [instance] dfinsupp.to_semimodule /-- Grade selection maps from objects in G to a finite set of components of substituent grades -/ class has_grade_select - (A : ℤ → Type u) (G: Type u) + {ι : Type u} [has_zero ι] + (A : ι → Type u) (G: Type u) [graded_module_components A] [add_comm_group G] + [ring (A 0)] [module (A 0) G] := -(select : G →ₗ[A 0] (Π₀ r, A r)) +(select : linear_map (A 0) G (Π₀ r, A r)) /- TODO: check precedence -/ notation `⟨`:0 g`⟩_`:0 r:100 := has_grade_select.select g r @@ -51,7 +55,8 @@ notation `⟨`:0 g`⟩_`:0 r:100 := has_grade_select.select g r /-- A module divisible into disjoint graded modules, where the grade selectio operator is a complete and independent set of projections -/ class graded_module - (A : ℤ → Type u) (G: Type u) + {ι : Type v} [has_zero ι] + (A : ι → Type u) (G: Type u) [graded_module_components A] [add_comm_group G] [module (A 0) G] @@ -61,22 +66,22 @@ class graded_module namespace graded_module - variables {A : ℤ → Type u} {G: Type u} + variables {ι : Type v} [has_zero ι] {A : ι → Type u} {G: Type u} variables [graded_module_components A] [add_comm_group G] [module (A 0) G] variables [graded_module A G] /-- locally bind the notation above to our A and G-/ - local notation `⟨`:0 g`⟩_`:0 r:100 := @has_grade_select.select A G _ _ _ _ g r + local notation `⟨`:0 g`⟩_`:0 r:100 := @has_grade_select.select ι A G _ _ _ _ g r /-- convert from r-vectors to multi-vectors -/ - instance has_coe (r : ℤ) : has_coe (A r) G := { coe := to_fun } + instance has_coe (r : ι) : has_coe (A r) G := { coe := to_fun } @[simp] - lemma coe_def {r : ℤ} (v : A r) : (v : G) = to_fun v := rfl + lemma coe_def {r : ι} (v : A r) : (v : G) = to_fun v := rfl /-- An r-vector has only a single grade Discussed at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Expressing.20a.20sum.20with.20finitely.20many.20nonzero.20terms/near/202657281-/ - lemma select_coe_is_single {r : ℤ} (v : A r) : has_grade_select.select (v : G) = dfinsupp.single r v := begin + lemma select_coe_is_single {r : ι} (v : A r) : has_grade_select.select (v : G) = dfinsupp.single r v := begin symmetry, rw is_complete (v : G) (dfinsupp.single r v), symmetry, @@ -84,19 +89,19 @@ namespace graded_module exact linear_map.map_zero _, end - def is_r_vector (r : ℤ) (a : G) := (⟨a⟩_r : G) = a + def is_r_vector (r : ι) (a : G) := (⟨a⟩_r : G) = a /-- Chisholm 6a, ish. This says A = ⟨A}_r for r-vectors. Chisholm aditionally wants proof that A != ⟨A}_r for non-rvectors -/ - lemma r_grade_of_coe {r : ℤ} (v : A r) : ⟨v⟩_r = v := begin + lemma r_grade_of_coe {r : ι} (v : A r) : ⟨v⟩_r = v := begin rw select_coe_is_single, rw dfinsupp.single_apply, simp, end /-- to_fun is injective -/ - lemma to_fun_inj (r : ℤ) : function.injective (to_fun : A r → G) := begin + lemma to_fun_inj (r : ι) : function.injective (to_fun : A r → G) := begin intros a b h, rw ← r_grade_of_coe a, rw ← r_grade_of_coe b, @@ -106,13 +111,13 @@ namespace graded_module end /-- Chisholm 6b -/ - lemma grade_of_sum (r : ℤ) (a b : G) : ⟨a + b⟩_r = ⟨a⟩_r + ⟨b⟩_r := by simp + lemma grade_of_sum (r : ι) (a b : G) : ⟨a + b⟩_r = ⟨a⟩_r + ⟨b⟩_r := by simp /-- Chisholm 6c -/ - lemma grade_smul (r : ℤ) (k : A 0) (a : G) : ⟨k • a⟩_r = k • ⟨a⟩_r := by simp + lemma grade_smul (r : ι) (k : A 0) (a : G) : ⟨k • a⟩_r = k • ⟨a⟩_r := by simp /-- chisholm 6d. Modifid to use `_s` instead of `_r` on the right, to keep the statement cast-free -/ - lemma grade_grade (r s : ℤ) (a : G) : ⟨⟨a⟩_r⟩_s = if r = s then ⟨a⟩_s else 0 + lemma grade_grade (r s : ι) (a : G) : ⟨⟨a⟩_r⟩_s = if r = s then ⟨a⟩_s else 0 := begin rw select_coe_is_single, rw dfinsupp.single_apply,