mathlib3 documentation

lean-ga / geometric_algebra.from_mathlib.concrete.pga

Plane-based Geometric algebra #

This files defines the projectivized vector space projectivize V, and its associated geometric algebra CGA.

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

This file is underdeveloped compared to one for conformalize, but is included as a skeleton of how to proceed.

source
@[protected, instance]
noncomputable def projectivize.module (V : Type u_1) [normed_add_comm_group V] [inner_product_space ℝ V] :
module ℝ (projectivize V)
source
def projectivize (V : Type u_1) [normed_add_comm_group V] [inner_product_space ℝ V] :
Type u_1

A projectivized vector has additional e0 component

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

Define linear maps to extract the new components

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

The metric is the metric of V with the n0 term ignored.

source
noncomputable def projectivize.Q {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :
quadratic_form ℝ (projectivize V)
Equations
source
@[simp]
theorem projectivize.Q_apply {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] (x : projectivize V) :
⇑projectivize.Q x = ‖⇑projectivize.v x‖ ^ 2

Show the definition is what we expect.

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

Define the Plane-based Geometric Algebra over V.

source
noncomputable def projectivize.up (V : Type u_1) [normed_add_comm_group V] [inner_product_space ℝ V] (x : V) :
projectivize.PGA V

And the embedding of the vector space into it. Note that often the dual of this result is used instead, but we do not have that in our formalization yet!

Equations