mathlib3 documentation

lean-ga / geometric_algebra.from_mathlib.concrete.cga

Conformal Geometric algebra #

This files defines the conformalized vector space conformalize V, and its associated geometric algebra CGA.

A typical usage would use CGA (euclidean_space ℝ 3).

The conformalized space conformalize V #

source
def conformalize (V : Type u_1) [normed_add_comm_group V] [inner_product_space ℝ V] :
Type u_1

A conformalized vector has additional $n_0$ and $n_\infty$ components

Equations
Instances for conformalize
source
@[protected, instance]
def conformalize.add_comm_group (V : Type u_1) [normed_add_comm_group V] [inner_product_space ℝ V] :
add_comm_group (conformalize V)
source
@[protected, instance]
noncomputable def conformalize.module (V : Type u_1) [normed_add_comm_group V] [inner_product_space ℝ V] :
module ℝ (conformalize V)

Linear maps which extract the three components, with c_ abbreviating "coefficient of".

source
noncomputable def conformalize.v {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
conformalize V →ₗ[ℝ] V
Equations
source
noncomputable def conformalize.c_n0 {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
conformalize V →ₗ[ℝ] ℝ
Equations
source
noncomputable def conformalize.c_ni {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
conformalize V →ₗ[ℝ] ℝ
Equations

The embedding of directions from V into conformalize V, and the two basis vectors.

source
noncomputable def conformalize.of_v {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
V →ₗ[ℝ] conformalize V
Equations
source
def conformalize.n0 {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
conformalize V
Equations
source
def conformalize.ni {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
conformalize V
Equations

Lemmas to train the simplifier about trivial compositions of the above.

source
@[simp]
theorem conformalize.v_of_v {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
⇑conformalize.v (⇑conformalize.of_v x) = x
source
@[simp]
theorem conformalize.c_n0_of_v {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
⇑conformalize.c_n0 (⇑conformalize.of_v x) = 0
source
@[simp]
theorem conformalize.c_ni_of_v {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
⇑conformalize.c_ni (⇑conformalize.of_v x) = 0
source
@[simp]
theorem conformalize.v_n0 {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
⇑conformalize.v conformalize.n0 = 0
source
@[simp]
theorem conformalize.c_n0_n0 {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
⇑conformalize.c_n0 conformalize.n0 = 1
source
@[simp]
theorem conformalize.c_ni_n0 {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
⇑conformalize.c_ni conformalize.n0 = 0
source
@[simp]
theorem conformalize.v_ni {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
⇑conformalize.v conformalize.ni = 0
source
@[simp]
theorem conformalize.c_n0_ni {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
⇑conformalize.c_n0 conformalize.ni = 0
source
@[simp]
theorem conformalize.c_ni_ni {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
⇑conformalize.c_ni conformalize.ni = 1
source
noncomputable def conformalize.up {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
conformalize V

The embedding of points from V to conformalize V.

Equations

The metric on the conformalized space #

source
noncomputable def conformalize.Q {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
quadratic_form ℝ (conformalize V)

The metric is the metric of V plus an extra term about n0 and ni.

Equations
source
@[simp]
theorem conformalize.Q_apply {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : conformalize V) :
⇑conformalize.Q x = ‖⇑conformalize.v x‖ ^ 2 - 2 * (⇑conformalize.c_n0 x * ⇑conformalize.c_ni x)

Show the definition is what we expect.

source
@[simp]
theorem conformalize.Q_up {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
⇑conformalize.Q (conformalize.up x) = 0

Train the simplifier how to act on components

source
@[simp]
theorem conformalize.Q_polar_n0_of_v {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
quadratic_form.polar ⇑conformalize.Q conformalize.n0 (⇑conformalize.of_v x) = 0
source
@[simp]
theorem conformalize.Q_polar_n0_n0 {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
quadratic_form.polar ⇑conformalize.Q conformalize.n0 conformalize.n0 = 0
source
@[simp]
theorem conformalize.Q_polar_n0_ni {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
quadratic_form.polar ⇑conformalize.Q conformalize.n0 conformalize.ni = -2
source
@[simp]
theorem conformalize.Q_polar_ni_of_v {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
quadratic_form.polar ⇑conformalize.Q conformalize.ni (⇑conformalize.of_v x) = 0
source
@[simp]
theorem conformalize.Q_polar_ni_ni {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
quadratic_form.polar ⇑conformalize.Q conformalize.ni conformalize.n0 = -2
source
@[simp]
theorem conformalize.Q_polar_ni_n0 {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
quadratic_form.polar ⇑conformalize.Q conformalize.ni conformalize.ni = 0
source
@[simp]
theorem conformalize.Q_polar_of_v_ni {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
quadratic_form.polar ⇑conformalize.Q (⇑conformalize.of_v x) conformalize.n0 = 0
source
@[simp]
theorem conformalize.Q_polar_of_v_n0 {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
quadratic_form.polar ⇑conformalize.Q (⇑conformalize.of_v x) conformalize.ni = 0
source
@[simp]
theorem conformalize.Q_polar_of_v_of_v {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x y : V) :
quadratic_form.polar ⇑conformalize.Q (⇑conformalize.of_v x) (⇑conformalize.of_v y) = 2 * has_inner.inner x y
source
@[simp]
theorem conformalize.Q_polar_up {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x y : V) :
quadratic_form.polar ⇑conformalize.Q (conformalize.up x) (conformalize.up y) = -has_dist.dist x y ^ 2

The c_n0 and c_ni terms cancel to give the (negated) distance

The geometric algebra over that space #

source
@[reducible]
def conformalize.CGA (V : Type u_1) [normed_add_comm_group V] [inner_product_space ℝ V] :
Type u_1

Define the Conformal Geometric Algebra over V .

source
theorem conformalize.ι_up_mul_ι_up_add_swap {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x y : V) :
⇑(clifford_algebra.ι conformalize.Q) (conformalize.up x) * ⇑(clifford_algebra.ι conformalize.Q) (conformalize.up y) + ⇑(clifford_algebra.ι conformalize.Q) (conformalize.up y) * ⇑(clifford_algebra.ι conformalize.Q) (conformalize.up x) = ⇑(algebra_map ℝ (clifford_algebra conformalize.Q)) (-has_dist.dist x y ^ 2)