commit c92b4c4730f59cbf9df1bc394394a5668d82d9bc
parent 524507dfa2a332f8f52718c7527f1ed74a15f504
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Thu, 25 Jul 2024 17:40:19 -0700
Add Coordinates and FiniteBasis, and remove old BitVec stuff
Diffstat:
| M | Main.lean | | | 48 | +++++++++++++++++++----------------------------- |
1 file changed, 19 insertions(+), 29 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -4,18 +4,6 @@ class SMul (α β : Type) where
smul : α -> β -> β
infixr:75 " ⋅ " => SMul.smul
-def BitVec.foldl (b : BitVec n) (f : α -> Bool -> α) (init : α) :=
- let rec loop (acc : α) (i : Nat) : α :=
- if i < n then
- let acc' := f acc (BitVec.getLsb b i)
- loop acc' (i + 1)
- else
- acc
- loop init 0
-
-def BitVec.popCount (b : BitVec n) : Nat :=
- b.foldl (fun acc bit => acc + Bool.toNat bit) 0
-
class AddSemigroup (A : Type) where
add : A -> A -> A
class AddMonoid (A : Type) extends AddSemigroup A where
@@ -83,12 +71,26 @@ instance [Field F] [AddGroup V] [VectorSpace F V] : VectorSpace F (FunctionSpace
-- Function spaces with finite domain.
abbrev NSpace (n : Nat) (V : Type) : Type := FunctionSpace (Fin n) V
-instance [ToString V] : ToString (NSpace n V) where
- toString f :=
- let coordToString i acc := toString (f i) :: acc
- s!"({String.intercalate ", " $ Fin.foldr n coordToString []})"
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
+
+instance [Field F] [ToString F] : ToString (Coordinates F 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).
+ coords : V -> Coordinates F n
+
def QuadraticForm (F : Type) [Field F] (n : Nat) := Fin n -> F
structure Blade (n : Nat) : Type where
@@ -111,18 +113,6 @@ instance : ToString (Blade n) where
else
""
-/-
-def Blade.mulSign (x y : Blade n) : Int :=
- let rec countInversions (y : BitVec n) (count : Nat) (i : Nat) : Nat :=
- if i < n then
- let y' := y >>> 1
- let count' := count + BitVec.popCount (x.bits &&& y')
- countInversions y' count' (i + 1)
- else
- count
- if countInversions y.bits 0 0 % 2 = 0 then 1 else -1
--/
-
structure GeometricAlgebra (F : Type) [Field F] (n : Nat) (q : QuadraticForm F n) : Type where
fn : FunctionSpace (Blade n) F
@@ -189,5 +179,5 @@ def main : IO Unit :=
| 1 => 1
| 2 => 1
let u : GeometricAlgebra F n q := ⟨fun _ => 1⟩
- let w : GeometricAlgebra F n q := u + u
+ let w : GeometricAlgebra F n q := u * u
IO.println w
