Derived from "A New Formalization of Origami in Geometric Algebra" #

This version is an incorrect but accidentally simpler attempt at translating what is now ida.multivector. It is included for completeness, but not referenced in our paper.

source

def ida'.rvector :

fin 4 → Type

Equations

ida'.rvector ⟨n + 4, _x⟩ = false.rec Type _
ida'.rvector ⟨3, _x⟩ = ℝ
ida'.rvector ⟨2, _x⟩ = (ℝ × ℝ × ℝ)
ida'.rvector ⟨1, _x⟩ = (ℝ × ℝ × ℝ)
ida'.rvector ⟨0, _x⟩ = ℝ

Instances for ida'.rvector

ida'.rvector.add_comm_group

source

@[protected, instance]

def ida'.rvector.add_comm_group (i : fin 4) :

add_comm_group (ida'.rvector i)

Equations

ida'.rvector.add_comm_group ⟨n + 4, _x⟩ = false.rec (add_comm_group (ida'.rvector ⟨n + 4, _x⟩)) _
ida'.rvector.add_comm_group ⟨3, _x⟩ = _.mpr real.add_comm_group
ida'.rvector.add_comm_group ⟨2, _x⟩ = _.mpr prod.add_comm_group
ida'.rvector.add_comm_group ⟨1, _x⟩ = _.mpr prod.add_comm_group
ida'.rvector.add_comm_group ⟨0, _x⟩ = _.mpr real.add_comm_group

source

@[reducible]

def ida'.multivector :

Type

source

def ida'.grade (m : ida'.multivector) (i : fin 4) :

ida'.rvector i

Equations

ida'.grade m i = ⇑m i

source

def ida'.multivector.of (i : fin 4) :

ida'.rvector i →+ direct_sum (fin 4) (λ (i : fin 4), ida'.rvector i)

Equations

ida'.multivector.of i = direct_sum.of ida'.rvector i

source

def ida'.rvector_mul {i j : fin 4} :

ida'.rvector i → ida'.rvector j → ida'.multivector

Equations

ida'.rvector_mul _x_1 _x_2 = sorry
ida'.rvector_mul _x _x_1 = sorry
ida'.rvector_mul (a₁, a₂, a₃) (b₁, b₂, b₃) = ⇑(ida'.multivector.of 0) (a₁ * b₁ + a₂ * b₂ + a₃ * b₃) + ⇑(ida'.multivector.of 2) sorry
ida'.rvector_mul _x _x_1 = sorry
ida'.rvector_mul _x _x_1 = sorry
ida'.rvector_mul a b = ⇑(ida'.multivector.of 0) (a * b)

Note: this declaration is incomplete and uses sorry.

source

@[protected, instance]

def ida'.multivector.has_mul :

has_mul ida'.multivector

Equations

ida'.multivector.has_mul = {mul := λ (a b : ida'.multivector), finset.univ.sum (λ (i : fin 4), finset.univ.sum (λ (j : fin 4), ida'.rvector_mul (ida'.grade a i) (ida'.grade b j)))}

source

@[protected, instance]

def ida'.multivector.ring :

ring ida'.multivector

Equations

ida'.multivector.ring = sorry

Note: this declaration is incomplete and uses sorry.

source

@[protected, instance]

def ida'.multivector.algebra :

algebra ℝ ida'.multivector

Equations

ida'.multivector.algebra = sorry

Note: this declaration is incomplete and uses sorry.