commit b0c224155a3dd9e82dc3d20ed3ba51d4771b1549
parent 1bdb5df974c44722752b02bc33bfd6ff6f790552
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Sat, 27 Jul 2024 15:33:04 -0700
Replace Field and VectorSpace with Ring and Module
Diffstat:
| M | Main.lean | | | 117 | ++++++++++++++++++++++++++++++++++++++----------------------------------------- |
1 file changed, 56 insertions(+), 61 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -78,6 +78,7 @@ class Inv (α : Type) where
--------------------------------------------------------------------------------
-- Single additive operator algebraic structures, all implicitly commutative
+-- TODO: separate these like MulX
class AddSemigroup (A : Type) where
add : A -> A -> A
@@ -189,9 +190,9 @@ instance [MulGroup A] {n : Nat} : MulGroup (A ^ n) := MulGroup.instFun
instance [MulCommGroup A] {n : Nat} : MulCommGroup (A ^ n) := MulCommGroup.instFun
--------------------------------------------------------------------------------
--- Rings, implicitly commutative and unital
+-- Commutative and unital rings
-class Ring (R : Type) extends AddGroup R, MulMonoid R
+class Ring (R : Type) extends AddGroup R, MulCommMonoid R
instance : Ring Rat where
zero := 0
@@ -200,41 +201,34 @@ instance : Ring Rat where
one := 1
mul := Rat.mul
---------------------------------------------------------------------------------
--- Fields, where ∀a. div a = 0 and inv 0 = a
-
-class Field (F : Type) extends Ring F, MulGroup F
-
-instance : Field Rat where
- div := Rat.div
- inv := Rat.inv
+-- TODO: PolyRing
--------------------------------------------------------------------------------
--- Vector spaces
+-- Modules
--- F is an outParam, because usually V will only be a vector space over one
--- field, and this allows us to leave F implicit in many cases.
-class VectorSpace (F : outParam Type) [Field F] (V : Type) [AddGroup V] where
- smul : F -> V -> V
+-- R is an outParam, because usually V will only be a module over one ring, and
+-- this allows us to leave R implicit in many cases.
+class Module (R : outParam Type) [Ring R] (M : Type) [AddGroup M] where
+ smul : R -> M -> M
-instance [Field F] [AddGroup V] [VectorSpace F V] : SMul F V where
- smul := VectorSpace.smul
+instance [Ring R] [AddGroup M] [Module R M] : SMul R M where
+ smul := Module.smul
-instance [Field F] : VectorSpace F F where
+instance [Ring R] : Module R R where
smul := MulSemigroup.mul
-instance [Field F] [AddGroup V] [VectorSpace F V] [AddGroup W] [VectorSpace F W] : VectorSpace F (V × W) where
+instance [Ring R] [AddGroup M] [Module R M] [AddGroup N] [Module R N] : Module R (M × N) where
smul a p := (a ⋅ p.1, a ⋅ p.2)
-instance VectorSpace.instFun [Field F] [AddGroup V] [VectorSpace F V] : VectorSpace F (X -> V) where
+instance Module.instFun [Ring R] [AddGroup M] [Module R M] : Module R (X -> M) where
smul a f := fun x => a ⋅ f x
-instance [Field F] [AddGroup V] [VectorSpace F V] {n : Nat} : VectorSpace F (V ^ n) := VectorSpace.instFun
+instance [Ring R] [AddGroup M] [Module R M] {n : Nat} : Module R (M ^ n) := Module.instFun
-def Coordinates [Field F] (V : Type) [AddGroup V] [VectorSpace F V] (n : Nat) : Type :=
- Fin n -> F
+def Coordinates [Ring R] (M : Type) [AddGroup M] [Module R M] (n : Nat) : Type :=
+ Fin n -> R
-instance [Field F] [ToString F] [AddGroup V] [VectorSpace F V] : ToString (Coordinates V n) where
+instance [Ring R] [ToString R] [AddGroup M] [Module R M] : ToString (Coordinates M n) where
toString coords :=
match n with
| 1 => toString (coords 0)
@@ -242,19 +236,20 @@ instance [Field F] [ToString F] [AddGroup V] [VectorSpace F V] : ToString (Coord
let consCoordString i acc := toString (coords i) :: acc
s!"({String.intercalate ", " $ Fin.foldr n consCoordString []})"
-structure FiniteBasis [Field F] (V : Type) [AddGroup V] [VectorSpace F V] (n : Nat) where
- basis : Fin n -> V
- coords : V -> Coordinates V n
+structure FiniteBasis [Ring R] (M : Type) [AddGroup M] [Module R M] (n : Nat) where
+ basis : Fin n -> M
+ coords : M -> Coordinates M n
-def FiniteBasis.vector [Field F] [AddGroup V] [VectorSpace F V]
- (b : FiniteBasis V n) (coords : Coordinates V n) : V :=
+-- XXX: Calling this "vector" is maybe a bit weird.
+def FiniteBasis.vector [Ring R] [AddGroup M] [Module R M]
+ (b : FiniteBasis M n) (coords : Coordinates M n) : M :=
Fin.foldl n (fun acc i => acc + coords i ⋅ b.basis i) 0
-def FiniteBasis.field (F : Type) [Field F] : FiniteBasis F 1 :=
+def FiniteBasis.ring (R : Type) [Ring R] : FiniteBasis R 1 :=
⟨fun 0 => 1, fun a 0 => a⟩
-def FiniteBasis.mul [Field F] [AddGroup V] [VectorSpace F V] (b : FiniteBasis V m)
- [AddGroup W] [VectorSpace F W] (c : FiniteBasis W n) : FiniteBasis (V × W) (m + n) :=
+def FiniteBasis.mul [Ring R] [AddGroup M] [Module R M] (b : FiniteBasis M m)
+ [AddGroup N] [Module R N] (c : FiniteBasis N n) : FiniteBasis (M × N) (m + n) :=
let basis i :=
match finSum i with
| .inl i => (b.basis i, 0)
@@ -265,8 +260,8 @@ def FiniteBasis.mul [Field F] [AddGroup V] [VectorSpace F V] (b : FiniteBasis V
| .inr i => c.coords v.2 i
⟨basis, coords⟩
-def FiniteBasis.pow [Field F] [AddGroup V] [VectorSpace F V] (b : FiniteBasis V m)
- (n : Nat) : FiniteBasis (V ^ n) (m * n) :=
+def FiniteBasis.pow [Ring R] [AddGroup M] [Module R M] (b : FiniteBasis M m)
+ (n : Nat) : FiniteBasis (M ^ n) (m * n) :=
let basis i :=
let ⟨iq, ir⟩ := finProd i
fun j => if j = ir then b.basis iq else 0
@@ -277,11 +272,11 @@ def FiniteBasis.pow [Field F] [AddGroup V] [VectorSpace F V] (b : FiniteBasis V
-- OrthoQuadraticForm b is a quadratic form with respect to which the finite
-- basis b is orthogonal.
-structure OrthoQuadraticForm [Field F] [AddGroup V] [VectorSpace F V] (_ : FiniteBasis V n) where
- evalBasis : Fin n -> F
+structure OrthoQuadraticForm [Ring R] [AddGroup M] [Module R M] (_ : FiniteBasis M n) where
+ evalBasis : Fin n -> R
-def OrthoQuadraticForm.eval [Field F] [AddGroup V] [VectorSpace F V]
- {b : FiniteBasis V n} (q : OrthoQuadraticForm b) (v : V) : F :=
+def OrthoQuadraticForm.eval [Ring R] [AddGroup M] [Module R M]
+ {b : FiniteBasis M n} (q : OrthoQuadraticForm b) (v : M) : R :=
let vCoords := b.coords v
-- q v = q (∑ vCoords i ⋅ b.basis i)
-- = ∑ q (vCoords i ⋅ b.basis i) (orthogonality of b wrt q)
@@ -290,11 +285,11 @@ def OrthoQuadraticForm.eval [Field F] [AddGroup V] [VectorSpace F V]
Fin.foldl n (fun acc i => acc + vCoords i * vCoords i * q.evalBasis i) 0
--------------------------------------------------------------------------------
--- Algebras (over a field)
+-- Algebras
-class Algebra (F : outParam Type) [Field F] (A : Type) [AddGroup A] [MulMonoid A] extends VectorSpace F A
+class Algebra (R : outParam Type) [Ring R] (A : Type) [AddGroup A] [MulMonoid A] extends Module R A
-instance [Field F] : Algebra F F where
+instance [Ring R] : Algebra R R where
-- TODO: More Algebra instances
@@ -302,14 +297,14 @@ instance [Field F] : Algebra F F where
-- Geometric algebra generation from vector spaces with a quadratic form and
-- an orthogonal finite basis
-structure GeometricAlgebra [Field F] [AddGroup V] [VectorSpace F V]
- {b : FiniteBasis V n} (q : OrthoQuadraticForm b) : Type where
- coords : BitVec n -> F
+structure GeometricAlgebra [Ring R] [AddGroup M] [Module R M]
+ {b : FiniteBasis M n} (q : OrthoQuadraticForm b) : Type where
+ coords : BitVec n -> R
-instance [Field F] [DecidableEq F] [ToString F] [AddGroup V] [VectorSpace F V]
- {b : FiniteBasis V n} {q : OrthoQuadraticForm b} : ToString (GeometricAlgebra q) where
+instance [Ring R] [DecidableEq R] [ToString R] [AddGroup M] [Module R M]
+ {b : FiniteBasis M n} {q : OrthoQuadraticForm b} : ToString (GeometricAlgebra q) where
toString v :=
- let bldToString (bld : BitVec n) :=
+ let bldToString (bld : BitVec n) : String :=
let indexToString (i : Fin n) acc :=
if bld.getLsb i then toString i :: acc else acc
let indexStrings := Fin.foldr n indexToString []
@@ -335,14 +330,14 @@ instance [Field F] [DecidableEq F] [ToString F] [AddGroup V] [VectorSpace F V]
else
"0"
-instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
+instance [Ring R] [AddGroup M] [Module R M] {b : FiniteBasis M n}
{q : OrthoQuadraticForm b} : AddGroup (GeometricAlgebra q) where
zero := ⟨0⟩
add v w := ⟨v.coords + w.coords⟩
sub v w := ⟨v.coords - w.coords⟩
-instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
- {q : OrthoQuadraticForm b} : VectorSpace F (GeometricAlgebra q) where
+instance [Ring R] [AddGroup M] [Module R M] {b : FiniteBasis M n}
+ {q : OrthoQuadraticForm b} : Module R (GeometricAlgebra q) where
smul a v := ⟨a ⋅ v.coords⟩
-- Multiplication algorithm:
@@ -373,39 +368,39 @@ instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
-- "squares" of each basis vector shared by vbld and wbld, where "square" means
-- apply the quadratic form.
-instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
+instance [Ring R] [AddGroup M] [Module R M] {b : FiniteBasis M n}
{q : OrthoQuadraticForm b} : MulMonoid (GeometricAlgebra q) where
one := ⟨fun bld => if bld = 0 then 1 else 0⟩
mul v w :=
- let sign (x y : BitVec n) : F :=
+ let sign (x y : BitVec n) : R :=
let addSwaps (acc : Nat) (i : Fin n) : Nat :=
acc + bitVecPopCount (x &&& (y <<< (i.val + 1)))
let nSwaps := Fin.foldl n addSwaps 0
if nSwaps % 2 = 0 then 1 else -1
- let scalar (x y : BitVec n) : F :=
+ let scalar (x y : BitVec n) : R :=
let z := x &&& y
- let mulSquares (acc : F) (i : Fin n) : F :=
+ let mulSquares (acc : R) (i : Fin n) : R :=
if z.getLsb i then acc * q.evalBasis i else acc
Fin.foldl n mulSquares 1
- let coords (bld : BitVec n) : F :=
- let addTerm (acc : F) (vbld : BitVec n) : F :=
+ let coords (bld : BitVec n) : R :=
+ let addTerm (acc : R) (vbld : BitVec n) : R :=
let wbld : BitVec n := vbld ^^^ bld
acc + sign vbld wbld * scalar vbld wbld * v.coords vbld * w.coords wbld
bitVecEnuml n addTerm 0
⟨coords⟩
-instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
- {q : OrthoQuadraticForm b} : Algebra F (GeometricAlgebra q) where
+instance [Ring R] [AddGroup M] [Module R M] {b : FiniteBasis M n}
+ {q : OrthoQuadraticForm b} : Algebra R (GeometricAlgebra q) where
--------------------------------------------------------------------------------
-- Main
-abbrev F : Type := Rat
+abbrev R : Type := Rat
abbrev n : Nat := 3
-abbrev V : Type := F ^ n
-abbrev b : FiniteBasis V n := FiniteBasis.pow (FiniteBasis.field F) n
+abbrev M : Type := R ^ n
+abbrev b : FiniteBasis M n := FiniteBasis.pow (FiniteBasis.ring R) n
abbrev q : OrthoQuadraticForm b := ⟨
fun
| 0 => 1
