lean-ga / geometric_algebra.nursery.graded

source

@[class]

structure graded_module_components (A : ℤ → Type u) :

Type u

zc : comm_ring (A 0)
b : Π (r : ℤ), add_comm_monoid (A r)
c : Π (r : ℤ), module (A 0) (A r)

Instances for graded_module_components

graded_module_components.has_sizeof_inst

source

@[class]

structure has_grade_select (A : ℤ → Type u) (G : Type u) [graded_module_components A] [add_comm_group G] [module (A 0) G] :

Type u

select : G →ₗ[A 0] Π₀ (r : ℤ), A r

Grade selection maps from objects in G to a finite set of components of substituent grades

Instances of this typeclass

graded_module.to_has_grade_select

Instances of other typeclasses for has_grade_select

has_grade_select.has_sizeof_inst

source

@[class]

structure graded_module (A : ℤ → Type u) (G : Type u) [graded_module_components A] [add_comm_group G] [module (A 0) G] :

Type u

to_has_grade_select : has_grade_select A G
to_fun : Π {r : ℤ}, A r →ₗ[A 0] G
is_complete : ∀ (g : G) (f : Π₀ (r : ℤ), A r), f = ⇑has_grade_select.select g ↔ g = f.sum (λ (r : ℤ), ⇑graded_module.to_fun)

A module divisible into disjoint graded modules, where the grade selectio operator is a complete and independent set of projections

Instances for graded_module

graded_module.has_sizeof_inst

source

@[protected, instance]

def graded_module.has_coe {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] (r : ℤ) :

has_coe (A r) G

convert from r-vectors to multi-vectors

Equations

graded_module.has_coe r = {coe := ⇑graded_module.to_fun}

source

@[simp]

theorem graded_module.coe_def {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] {r : ℤ} (v : A r) :

↑v = ⇑graded_module.to_fun v

source

theorem graded_module.select_coe_is_single {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] {r : ℤ} (v : A r) :

⇑has_grade_select.select ↑v = dfinsupp.single r v

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

source

def graded_module.is_r_vector {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] (r : ℤ) (a : G) :

Prop

Equations

graded_module.is_r_vector r a = (↑(⇑(⇑has_grade_select.select a) r) = a)

source

theorem graded_module.r_grade_of_coe {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] {r : ℤ} (v : A r) :

⇑(⇑has_grade_select.select ↑v) r = v

Chisholm 6a, ish. This says A = ⟨A}_r for r-vectors. Chisholm aditionally wants proof that A != ⟨A}_r for non-rvectors

source

theorem graded_module.to_fun_inj {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] (r : ℤ) :

function.injective ⇑graded_module.to_fun

to_fun is injective

source

theorem graded_module.grade_of_sum {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] (r : ℤ) (a b : G) :

⇑(⇑has_grade_select.select (a + b)) r = ⇑(⇑has_grade_select.select a) r + ⇑(⇑has_grade_select.select b) r

Chisholm 6b

source

theorem graded_module.grade_smul {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] (r : ℤ) (k : A 0) (a : G) :

⇑(⇑has_grade_select.select (k • a)) r = k • ⇑(⇑has_grade_select.select a) r

Chisholm 6c

source

theorem graded_module.grade_grade {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] (r s : ℤ) (a : G) :

⇑(⇑has_grade_select.select ↑(⇑(⇑has_grade_select.select a) r)) s = ite (r = s) (⇑(⇑has_grade_select.select a) s) 0

chisholm 6d. Modifid to use _s instead of _r on the right, to keep the statement cast-free

source

theorem graded_module.grade_sum {A : ℤ → Type u} {G : Type u} [graded_module_components A] [add_comm_group G] [module (A 0) G] [graded_module A G] (g : G) :

g = (⇑has_grade_select.select g).sum (λ (r : ℤ), ⇑graded_module.to_fun)

chisholm 6e. The phrasing is made a little awkward by the construction of the finite decomposition of select -