lean-ga / geometric_algebra.from_mathlib.versors

source

def clifford_algebra.versors {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :

algebra.center_submonoid R (clifford_algebra Q)

The versors are the elements made up of products of vectors.

TODO: are scalars ≠1 considered versors?

Equations

clifford_algebra.versors Q = algebra.center_submonoid.closure R (set.range ⇑(clifford_algebra.ι Q))

Instances for ↥clifford_algebra.versors

source

@[simp]

theorem clifford_algebra.versors.ι_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (m : M) :

⇑(clifford_algebra.ι Q) m ∈ clifford_algebra.versors Q

source

theorem clifford_algebra.versors.induction_on {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {C : ↥(clifford_algebra.versors Q) → Prop} (v : ↥(clifford_algebra.versors Q)) (h_grade0 : ∀ (r : R), C ⟨⇑(algebra_map R (clifford_algebra Q)) r, _⟩) (h_grade1 : ∀ (m : M), C ⟨⇑(clifford_algebra.ι Q) m, _⟩) (h_mul : ∀ (a b : ↥(clifford_algebra.versors Q)), C a → C b → C (a * b)) :

C v

An induction process for the versors, proving a statement C about v given proofs that:

It holds for the scalars
It holds for the vectors
It holds for any product of two elements it holds for

source

meta def clifford_algebra.versors.inv_rev_tac :

tactic unit

source

@[simp]

theorem clifford_algebra.versors.involute_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.versors Q)) :

⇑clifford_algebra.involute ↑v ∈ clifford_algebra.versors Q

Involute of a versor is a versor

source

@[simp]

theorem clifford_algebra.versors.reverse_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.versors Q)) :

⇑clifford_algebra.reverse ↑v ∈ clifford_algebra.versors Q

Reverse of a versor is a versor

source

theorem clifford_algebra.versors.mul_self_reverse {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.versors Q)) :

∃ (r : R), ↑v * ⇑clifford_algebra.reverse ↑v = ⇑(algebra_map R (clifford_algebra Q)) r

A versor times its reverse is a scalar

TODO: Can we compute r constructively?

source

theorem clifford_algebra.versors.reverse_mul_self {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.versors Q)) :

∃ (r : R), ⇑clifford_algebra.reverse ↑v * ↑v = ⇑(algebra_map R (clifford_algebra Q)) r

A versor's reverse times itself is a scalar

TODO: Can we compute r constructively?

source

def clifford_algebra.versors.magnitude_aux {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

↥(clifford_algebra.versors Q) →*₀ clifford_algebra Q

The magnitude of a versor.

Equations

clifford_algebra.versors.magnitude_aux = {to_fun := λ (v : ↥(clifford_algebra.versors Q)), ↑v * ⇑clifford_algebra.reverse ↑v, map_zero' := _, map_one' := _, map_mul' := _}

source

@[simp]

theorem clifford_algebra.versors.magnitude_aux_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.versors Q)) :

⇑clifford_algebra.versors.magnitude_aux v = ↑v * ⇑clifford_algebra.reverse ↑v

source

def clifford_algebra.versors.magnitude_aux_exists_scalar {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.versors Q)) :

∃ (r : R), ⇑clifford_algebra.versors.magnitude_aux v = ⇑(algebra_map R (clifford_algebra Q)) r

source

theorem clifford_algebra.versors.magnitude_aux_zero {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.versors Q)) [no_zero_divisors R] (hQ : Q.anisotropic) (h0 : ∀ {r : R}, ⇑(algebra_map R (clifford_algebra Q)) r = 0 → r = 0) :

⇑clifford_algebra.versors.magnitude_aux v = 0 ↔ v = 0

Only zero versors have zero magnitude, assuming:

The metric is anisotropic (hqnz). Note this is a stricter requirement than non-degeneracy; versors in CGA 𝒢(ℝ⁴⋅¹) like n∞ and n∞*no are both counterexamples to this lemma.
0 remains 0 when mapped from R into clifford_algebra Q
R has no zero divisors

It's possible these last two requirements can be relaxed somehow.

source

@[simp]

theorem clifford_algebra.versors.magnitude_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.versors Q)) :

⇑clifford_algebra.versors.magnitude v = ⟨⇑clifford_algebra.versors.magnitude_aux v, _⟩

source

def clifford_algebra.versors.magnitude {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

↥(clifford_algebra.versors Q) →*₀ ↥⊥

The magnitude of a versor, as a member of the subalgebra of scalars

Note we can't put this in R unless we know algebra_map is injective. This is kind of annoying, because it means that even if we have field R, we can't invert the magnitude

Equations

clifford_algebra.versors.magnitude = {to_fun := λ (v : ↥(clifford_algebra.versors Q)), ⟨⇑clifford_algebra.versors.magnitude_aux v, _⟩, map_zero' := _, map_one' := _, map_mul' := _}

source

noncomputable def clifford_algebra.versors.magnitude_R {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (hi : function.injective ⇑(algebra_map R (clifford_algebra Q))) :

↥(clifford_algebra.versors Q) →*₀ R

Equations

clifford_algebra.versors.magnitude_R hi = {to_fun := λ (v : ↥(clifford_algebra.versors Q)), classical.some _, map_zero' := _, map_one' := _, map_mul' := _}

source

@[simp]

theorem clifford_algebra.versors.magnitude_R_eq {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (hi : function.injective ⇑(algebra_map R (clifford_algebra Q))) (v : ↥(clifford_algebra.versors Q)) :

⇑(algebra_map R (clifford_algebra Q)) (⇑(clifford_algebra.versors.magnitude_R hi) v) = ↑(⇑clifford_algebra.versors.magnitude v)

source

@[simp]

theorem clifford_algebra.versors.has_inv_inv {R' : Type u_3} [field R'] {M' : Type u_4} [add_comm_group M'] [module R' M'] {Q' : quadratic_form R' M'} [nontrivial (clifford_algebra Q')] (v : ↥(clifford_algebra.versors Q')) :

v⁻¹ = (⇑(clifford_algebra.versors.magnitude_R clifford_algebra.versors.has_inv._proof_1) v)⁻¹ • ⟨⇑clifford_algebra.reverse ↑v, _⟩

source

@[protected, instance]

noncomputable def clifford_algebra.versors.has_inv {R' : Type u_3} [field R'] {M' : Type u_4} [add_comm_group M'] [module R' M'] {Q' : quadratic_form R' M'} [nontrivial (clifford_algebra Q')] :

has_inv ↥(clifford_algebra.versors Q')

When R' is a field, we can define the inverse as ~V / (V * ~V).

Until we resolve the problems above about getting r constructively, we are forced to use the axiom of choice here

Equations

clifford_algebra.versors.has_inv = {inv := λ (v : ↥(clifford_algebra.versors Q')), (⇑(clifford_algebra.versors.magnitude_R clifford_algebra.versors.has_inv._proof_1) v)⁻¹ • ⟨⇑clifford_algebra.reverse ↑v, _⟩}

source

theorem clifford_algebra.versors.inv_zero {R' : Type u_3} [field R'] {M' : Type u_4} [add_comm_group M'] [module R' M'] {Q' : quadratic_form R' M'} [nontrivial (clifford_algebra Q')] :

0⁻¹ = 0

source

theorem clifford_algebra.versors.mul_inv_cancel' {R' : Type u_3} [field R'] {M' : Type u_4} [add_comm_group M'] [module R' M'] {Q' : quadratic_form R' M'} [nontrivial (clifford_algebra Q')] (v : ↥(clifford_algebra.versors Q')) (h : ⇑clifford_algebra.versors.magnitude v ≠ 0) :

v * v⁻¹ = 1

Versors with a non-zero magnitude have an inverse

source

@[protected, instance]

noncomputable def clifford_algebra.versors.group_with_zero {R' : Type u_3} [field R'] {M' : Type u_4} [add_comm_group M'] [module R' M'] {Q' : quadratic_form R' M'} [nontrivial (clifford_algebra Q')] [f : fact Q'.anisotropic] :

group_with_zero ↥(clifford_algebra.versors Q')

If additionally the metric is anisotropic, then the inverse imparts a group_with_zero structure.

Equations

clifford_algebra.versors.group_with_zero = {mul := monoid_with_zero.mul infer_instance, mul_assoc := _, one := monoid_with_zero.one infer_instance, one_mul := _, mul_one := _, npow := monoid_with_zero.npow infer_instance, npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero infer_instance, zero_mul := _, mul_zero := _, inv := has_inv.inv infer_instance, div := div_inv_monoid.div._default monoid_with_zero.mul clifford_algebra.versors.group_with_zero._proof_8 monoid_with_zero.one clifford_algebra.versors.group_with_zero._proof_9 clifford_algebra.versors.group_with_zero._proof_10 monoid_with_zero.npow clifford_algebra.versors.group_with_zero._proof_11 clifford_algebra.versors.group_with_zero._proof_12 has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid_with_zero.mul clifford_algebra.versors.group_with_zero._proof_14 monoid_with_zero.one clifford_algebra.versors.group_with_zero._proof_15 clifford_algebra.versors.group_with_zero._proof_16 monoid_with_zero.npow clifford_algebra.versors.group_with_zero._proof_17 clifford_algebra.versors.group_with_zero._proof_18 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

def clifford_algebra.spinors {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :

algebra.center_submonoid R (clifford_algebra Q)

The spinors are the versors with an even number of factors

Equations

clifford_algebra.spinors Q = algebra.center_submonoid.closure R (set.range ⇑(clifford_algebra.ι Q) * set.range ⇑(clifford_algebra.ι Q))

Instances for ↥clifford_algebra.spinors

source

theorem clifford_algebra.spinors.subset_versors {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

(clifford_algebra.spinors Q).to_submonoid ≤ (clifford_algebra.versors Q).to_submonoid

The spinors are versors

source

@[simp]

theorem clifford_algebra.spinors.ι_mul_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (m n : M) :

⇑(clifford_algebra.ι Q) m * ⇑(clifford_algebra.ι Q) n ∈ clifford_algebra.spinors Q

source

@[simp]

theorem clifford_algebra.spinors.algebra_map_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (r : R) :

⇑(algebra_map R (clifford_algebra Q)) r ∈ clifford_algebra.spinors Q

source

@[simp]

theorem clifford_algebra.spinors.smul_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (k : R) {v : clifford_algebra Q} (h : v ∈ clifford_algebra.spinors Q) :

k • v ∈ clifford_algebra.spinors Q

source

@[simp]

theorem clifford_algebra.spinors.neg_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {v : clifford_algebra Q} (h : v ∈ clifford_algebra.spinors Q) :

-v ∈ clifford_algebra.spinors Q

source

@[protected, instance]

def clifford_algebra.spinors.mul_action {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

mul_action R ↥(clifford_algebra.spinors Q)

Equations

clifford_algebra.spinors.mul_action = {to_has_smul := {smul := λ (k : R) (v : ↥(clifford_algebra.spinors Q)), ⟨k • ↑v, _⟩}, one_smul := _, mul_smul := _}

source

@[protected, instance]

def clifford_algebra.spinors.has_neg {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

has_neg ↥(clifford_algebra.spinors Q)

Equations

clifford_algebra.spinors.has_neg = {neg := λ (v : ↥(clifford_algebra.spinors Q)), ⟨-↑v, _⟩}

source

theorem clifford_algebra.spinors.induction_on {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {C : ↥(clifford_algebra.spinors Q) → Prop} (v : ↥(clifford_algebra.spinors Q)) (h_grade0 : ∀ (r : R), C ⟨⇑(algebra_map R (clifford_algebra Q)) r, _⟩) (h_grade2 : ∀ (m n : M), C ⟨⇑(clifford_algebra.ι Q) m * ⇑(clifford_algebra.ι Q) n, _⟩) (h_mul : ∀ (a b : ↥(clifford_algebra.spinors Q)), C a → C b → C (a * b)) :

C v

An induction process for the spinors, proving a statement C about v given proofs that:

It holds for the scalars
It holds for products of two vectors
It holds for any product of two elements it holds for

source

@[simp]

theorem clifford_algebra.spinors.involute_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.spinors Q)) :

⇑clifford_algebra.involute ↑v ∈ clifford_algebra.spinors Q

Involute of a spinor is a spinor

source

@[simp]

theorem clifford_algebra.spinors.reverse_mem {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (v : ↥(clifford_algebra.spinors Q)) :

⇑clifford_algebra.reverse ↑v ∈ clifford_algebra.spinors Q

Reverse of a spinor is a spinor

source

@[simp]

theorem clifford_algebra.involute_spinor {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (r : ↥(clifford_algebra.spinors Q)) :

⇑clifford_algebra.involute ↑r = ↑r

source

def clifford_algebra.r_multivectors {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :

algebra.filtration R (clifford_algebra Q) ℕ

The elements of at most grade n are a filtration

Equations

clifford_algebra.r_multivectors Q = {to_fun := r_multivectors.def Q, mono' := _, complete' := _, map_add' := _}

source

@[simp]

theorem clifford_algebra.r_multivectors.map_zero {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

⇑(clifford_algebra.r_multivectors Q) 0 = 1

source

@[simp]

theorem clifford_algebra.r_multivectors.map_succ {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (n : ℕ) :

⇑(clifford_algebra.r_multivectors Q) (n + 1) = ⇑(clifford_algebra.r_multivectors Q) n * linear_map.range (clifford_algebra.ι Q) ⊔ ⇑(clifford_algebra.r_multivectors Q) n

source

@[protected, instance]

def clifford_algebra.r_multivectors.has_coe_t {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (n r : ℕ) :

has_coe_t ↥(⇑(clifford_algebra.r_multivectors Q) n) ↥(⇑(clifford_algebra.r_multivectors Q) (n + r))

Since the sets are monotonic, we can coerce up to a larger submodule

Equations

clifford_algebra.r_multivectors.has_coe_t n r = {coe := λ (x : ↥(⇑(clifford_algebra.r_multivectors Q) n)), ⟨↑x, _⟩}

mathlib3 documentation

Versors, spinors, Multivectors, and other subspaces #