commit 46dd895a67dabea8178d8849a2f7a76e3aed31be
parent c92b4c4730f59cbf9df1bc394394a5668d82d9bc
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Thu, 25 Jul 2024 19:05:27 -0700
Rework bases and quadratic forms
Be explicit about the association between quadratic forms and vector spaces and (finite) bases.
Not yet integrated into the rest of the code.
Diffstat:
| M | Main.lean | | | 71 | ++++++++++++++++++++++++++++++++++++++++++++++++++--------------------- |
1 file changed, 50 insertions(+), 21 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -1,7 +1,11 @@
import Batteries.Data.Rat
+-- SMul represents the ability to use "⋅" as an infix operator.
class SMul (α β : Type) where
smul : α -> β -> β
+
+-- TODO: Is 75 an appropriate precedence?
+-- How do I figure out precedences of standard Lean operators?
infixr:75 " ⋅ " => SMul.smul
class AddSemigroup (A : Type) where
@@ -13,6 +17,13 @@ class AddGroup (A : Type) extends AddMonoid A where
neg : A -> A := fun x => sub zero x
-- Notation for AddXXX
+-- We could just, e.g., replace AddSemigroup A with Add A, but I think we ought
+-- to distinguish "notation type classes" from "conceptual type classes". It's
+-- especially important in this case, because these structures should satisfy
+-- some axioms which Add A, Sub A, etc. don't satisfy in general. The
+-- distinction between notation type classes and conceptual type classes would
+-- be clearer if we made axioms part of the conceptual type classes, but I can't
+-- be bothered with that; all I care about here is calculation.
instance [AddMonoid A] : OfNat A 0 where
ofNat := AddMonoid.zero
instance [AddSemigroup A] : Add A where
@@ -37,6 +48,7 @@ instance [MulSemigroup M] : Mul M where
mul := MulSemigroup.mul
instance [MulGroup M] : Div M where
div := MulGroup.div
+def inv := @MulGroup.inv
-- Convention: (∀a. div a 0 = 0) and (inv 0 = 0).
class Field (F : Type) extends AddGroup F, MulGroup F
@@ -49,7 +61,7 @@ instance : Field Rat where
mul := Rat.mul
div := Rat.div
-class VectorSpace (F : Type) [Field F] (V : Type) [AddGroup V] where
+class VectorSpace (F : outParam Type) [Field F] (V : Type) [AddGroup V] where
smul : F -> V -> V
-- Notation for VectorSpace
@@ -60,7 +72,8 @@ instance [Field F] [AddGroup V] [VectorSpace F V] : SMul F V where
instance [Field F] : VectorSpace F F where
smul := MulSemigroup.mul
--- Given a type X and a vector space V over F, the type of functions X -> V is a vector space over F.
+-- Given a type X and a vector space V over F, the type of functions X -> V is a
+-- vector space over F.
def FunctionSpace (X V : Type) : Type := X -> V
instance [AddGroup V] : AddGroup (FunctionSpace X V) where
zero := fun _ => 0
@@ -69,29 +82,46 @@ instance [AddGroup V] : AddGroup (FunctionSpace X V) where
instance [Field F] [AddGroup V] [VectorSpace F V] : VectorSpace F (FunctionSpace X V) where
smul a f := fun x => a ⋅ f x
--- Function spaces with finite domain.
+-- Function spaces with finite domain
abbrev NSpace (n : Nat) (V : Type) : Type := FunctionSpace (Fin n) V
def vec (coords : List V) : NSpace coords.length V := coords.get
--- We could define Coordinates F n = NSpace n F, but I think it's important to recognize the conceptual
--- difference between these two types: Coordinates F n is necessarily a tuple of scalars, with no further
--- inherent structure, whereas NSpace n F is a finite product of vector spaces, which just happens to
--- look like a tuple of scalars.
-def Coordinates (F : Type) [Field F] (n : Nat) := Fin n -> F
+-- We could define Coordinates V n = NSpace n F, but I think it's important to
+-- recognize the conceptual difference between these two types: Coordinates V n
+-- is necessarily a tuple of scalars, with no further inherent structure,
+-- whereas NSpace n F is a finite product of vector spaces, which just happens
+-- to look like a tuple of scalars.
+def Coordinates [Field F] (V : Type) [AddGroup V] [VectorSpace F V] (n : Nat) : Type :=
+ Fin n -> F
-instance [Field F] [ToString F] : ToString (Coordinates F n) where
+instance [Field F] [ToString F] [AddGroup V] [VectorSpace F V] : ToString (Coordinates V n) where
toString coords :=
let coordToString i acc := toString (coords i) :: acc
s!"({String.intercalate ", " $ Fin.foldr n coordToString []})"
-structure FiniteBasis (F : Type) [Field F] (V : Type) [AddGroup V] [VectorSpace F V] (n : Nat) where
- vector : Fin n -> V
-
- -- This should be an isomorphism of vector spaces (when Coordinates F n is regarded as a vector space
- -- with pointwise operations).
+structure FiniteBasis [Field F] (V : Type) [AddGroup V] [VectorSpace F V] (n : Nat) where
+ basis : Fin n -> V
coords : V -> Coordinates F n
-def QuadraticForm (F : Type) [Field F] (n : Nat) := Fin n -> F
+def FiniteBasis.vector [Field F] [AddGroup V] [VectorSpace F V]
+ (b : FiniteBasis V n) (coords : Coordinates V n) : V :=
+ Fin.foldl n (fun acc i => acc + coords i ⋅ b.basis i) 0
+
+-- OrthoQuadraticForm V B is a quadratic form on V with respect to which the
+-- finite basis B is orthogonal.
+structure OrthoQuadraticForm [Field F] (V : Type) [AddGroup V] [VectorSpace F V] (_ : FiniteBasis V n) where
+ evalBasis : Fin n -> F
+
+def OrthoQuadraticForm.eval [Field F] [AddGroup V] [VectorSpace F V]
+ {b : FiniteBasis V n} (q : OrthoQuadraticForm V b) (v : V) : F :=
+ let vCoords := b.coords v
+ -- q v = q (∑ vCoords i ⋅ b.basis i)
+ -- = ∑ q (vCoords i ⋅ b.basis i) (orthogonality of b wrt q)
+ -- = ∑ (vCoords i)^2 * q (b.basis i) (def. of quadratic form)
+ -- = ∑ (vCoords i)^2 * q.evalBasis i
+ Fin.foldl n (fun acc i => acc + vCoords i * vCoords i * q.evalBasis i) 0
+
+--class Algebra (F : Type) [Field F] (A : Type) [AddGroup A] [MulMonoid A] extends VectorSpace F A
structure Blade (n : Nat) : Type where
bits : BitVec n
@@ -113,7 +143,7 @@ instance : ToString (Blade n) where
else
""
-structure GeometricAlgebra (F : Type) [Field F] (n : Nat) (q : QuadraticForm F n) : Type where
+structure GeometricAlgebra (F : Type) [Field F] (n : Nat) (q : OrthoQuadraticForm F V n) : Type where
fn : FunctionSpace (Blade n) F
instance [Field F] {q : QuadraticForm F n} : AddGroup (GeometricAlgebra F n q) where
@@ -124,12 +154,11 @@ instance [Field F] {q : QuadraticForm F n} : AddGroup (GeometricAlgebra F n q) w
instance [Field F] {q : QuadraticForm F n} : VectorSpace F (GeometricAlgebra F n q) where
smul a v := ⟨a ⋅ v.fn⟩
--- TODO: Rename variables. Reorder BitVec.foldl args. Separate notion of basis for which we
--- can print coordinates.
+-- TODO: Rename variables.
--- Given u,v : GeometricAlgebra F n and b : Blade n, the b-th component of the product u * v
--- is a sum of 2^n terms, where each term is the product of the l-th component of u and the
--- r-th component of v, for all l,r : Blade n that multiply to b (modulo a scalar). The type
+-- Given u,v : GeometricAlgebra F n and b : Blade n, the b-th component of the
+-- product u * v is a sum of 2^n terms, where each term is the product of the
+-- l-th component of u and the r-th component of v, for all l,r : Blade n that multiply to b (modulo a scalar). The type
-- PartialTerm F i represents part of such a term, specifically the first i bits of l and r
-- and an associated scalar a. We also keep track of the parity of the l bits seen so far, so
-- that we know if we should flip the sign of a when we get the next r bit. This type should
