commit 884f33c2c9174935dfa5e258bdba4accb40c7d10
parent 46dd895a67dabea8178d8849a2f7a76e3aed31be
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Thu, 25 Jul 2024 23:13:33 -0700
Move stuff around; add cool repeatBasis function
Diffstat:
| M | Main.lean | | | 111 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++---------------------- |
1 file changed, 80 insertions(+), 31 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -53,14 +53,8 @@ def inv := @MulGroup.inv
-- Convention: (∀a. div a 0 = 0) and (inv 0 = 0).
class Field (F : Type) extends AddGroup F, MulGroup F
-instance : Field Rat where
- zero := 0
- add := Rat.add
- sub := Rat.sub
- one := 1
- mul := Rat.mul
- div := Rat.div
-
+-- 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
@@ -72,20 +66,6 @@ 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.
-def FunctionSpace (X V : Type) : Type := X -> V
-instance [AddGroup V] : AddGroup (FunctionSpace X V) where
- zero := fun _ => 0
- add f g := fun x => f x + g x
- sub f g := fun x => f x - g x
-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
-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 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,
@@ -96,24 +76,30 @@ def Coordinates [Field F] (V : Type) [AddGroup V] [VectorSpace F V] (n : Nat) :
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 []})"
+ match n with
+ | 1 => toString (coords 0)
+ | n =>
+ 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 F n
+ coords : V -> Coordinates V n
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
+def fieldBasis [Field F] : FiniteBasis F 1 :=
+ ⟨fun 0 => 1, fun a 0 => a⟩
+
-- 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
+structure OrthoQuadraticForm [Field F] [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 :=
+ {b : FiniteBasis V n} (q : OrthoQuadraticForm 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)
@@ -123,6 +109,7 @@ def OrthoQuadraticForm.eval [Field F] [AddGroup V] [VectorSpace F V]
--class Algebra (F : Type) [Field F] (A : Type) [AddGroup A] [MulMonoid A] extends VectorSpace F A
+-- TODO: Rename to FiniteBasisSet? Usually "Blade" means something more general.
structure Blade (n : Nat) : Type where
bits : BitVec n
@@ -143,19 +130,21 @@ instance : ToString (Blade n) where
else
""
-structure GeometricAlgebra (F : Type) [Field F] (n : Nat) (q : OrthoQuadraticForm F V n) : Type where
+structure GeometricAlgebra [Field F] [AddGroup V] [VectorSpace F V]
+ {b : FiniteBasis V n} (q : OrthoQuadraticForm b) : Type where
fn : FunctionSpace (Blade n) F
-instance [Field F] {q : QuadraticForm F n} : AddGroup (GeometricAlgebra F n q) where
+instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
+ {q : OrthoQuadraticForm b} : AddGroup (GeometricAlgebra q) where
zero := ⟨0⟩
add u v := ⟨u.fn + v.fn⟩
sub u v := ⟨u.fn - v.fn⟩
-instance [Field F] {q : QuadraticForm F n} : VectorSpace F (GeometricAlgebra F n q) where
+instance [Field F] [AddGroup V] [VectorSpace F V] {b : FiniteBasis V n}
+ {q : OrthoQuadraticForm b} : VectorSpace F (GeometricAlgebra q) where
smul a v := ⟨a ⋅ v.fn⟩
-- 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
@@ -200,6 +189,66 @@ instance [Field F] [ToString F] {q : QuadraticForm F n} : ToString (GeometricAlg
toString (v.fn b) ++ if b.bits != 0 then s!" * {toString b}" else ""
String.intercalate " + " (termToString <$> Blade.enum n)
+--------------------------------------------------------------------------------
+
+-- TODO: Remaining instances for products.
+instance [AddSemigroup A] [AddSemigroup B] : AddSemigroup (A × B) where
+ add x y := (x.1 + y.1, x.2 + y.2)
+instance [AddMonoid A] [AddMonoid B] : AddMonoid (A × B) where
+ zero := (0, 0)
+instance [AddGroup A] [AddGroup B] : AddGroup (A × B) where
+ sub x y := (x.1 - y.1, x.2 - y.2)
+
+instance : Field Rat where
+ zero := 0
+ add := Rat.add
+ sub := Rat.sub
+ one := 1
+ mul := Rat.mul
+ div := Rat.div
+
+-- 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
+ add f g := fun x => f x + g x
+ sub f g := fun x => f x - g x
+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
+abbrev NSpace (n : Nat) (V : Type) : Type := FunctionSpace (Fin n) V
+
+def divmod (i : Fin (m * n)) : Fin m × Fin n :=
+ let mul_gt_zero_imp_gt_zero {m n : Nat} : (m * n > 0) -> (m > 0) := by
+ intro
+ rw [<-Nat.zero_div n]
+ apply Nat.div_lt_of_lt_mul
+ rw [Nat.mul_comm]
+ assumption
+ have mn_gt_zero : m * n > 0 := Fin.pos i
+ have m_gt_zero : m > 0 := mul_gt_zero_imp_gt_zero mn_gt_zero
+ have nm_gt_zero : n * m > 0 := by rw [Nat.mul_comm]; exact mn_gt_zero
+ have n_gt_zero : n > 0 := mul_gt_zero_imp_gt_zero nm_gt_zero
+ let q := Fin.ofNat' (i.val / n) m_gt_zero
+ let r := Fin.ofNat' (i.val % n) n_gt_zero
+ (q, r)
+
+def repeatBasis [Field F] [AddGroup V] [VectorSpace F V] (b : FiniteBasis V m)
+ (n : Nat) : FiniteBasis (NSpace n V) (m * n) :=
+ let basis i :=
+ let ⟨iq, ir⟩ := divmod i
+ fun j => if j = ir then b.basis iq else 0
+ let coords v i :=
+ let ⟨iq, ir⟩ := divmod i
+ b.coords (v ir) iq
+ ⟨basis, coords⟩
+
+def vec (coords : List V) : NSpace coords.length V := coords.get
+
+--------------------------------------------------------------------------------
+
def main : IO Unit :=
let F : Type := Rat
let n : Nat := 3
