commit 8e5293c0d74d288b11b6b5932eaf874e73c78fab
parent 92379316f0d3fb3929a117863c6282a5a53fd827
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Sat, 27 Jul 2024 15:13:23 -0700
Separate MulCommX from MulX
In preparation for generalizing Fields/VectorSpaces to Rings/Modules, which we need in order to do symbolic calculation by taking scalars in a polynomial ring.
Diffstat:
| M | Main.lean | | | 78 | ++++++++++++++++++++++++++++++++++++++++++++++++++++-------------------------- |
1 file changed, 52 insertions(+), 26 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -77,7 +77,7 @@ class Inv (α : Type) where
inv : α -> α
--------------------------------------------------------------------------------
--- Single additive operator algebraic structures
+-- Single additive operator algebraic structures, all implicitly commutative
class AddSemigroup (A : Type) where
add : A -> A -> A
@@ -123,47 +123,73 @@ instance [AddMonoid A] {n : Nat} : AddMonoid (A ^ n) := AddMonoid.instFun
instance [AddGroup A] {n : Nat} : AddGroup (A ^ n) := AddGroup.instFun
--------------------------------------------------------------------------------
--- Single multiplicative operator algebraic structures
+-- Multiplicative semigroups, non-commutative or commutative
-class MulSemigroup (M : Type) where
- mul : M -> M -> M
-class MulMonoid (M : Type) extends MulSemigroup M where
- one : M
-class MulGroup (M : Type) extends MulMonoid M where
- div : M -> M -> M
- inv : M -> M := fun x => div one x
+class MulSemigroup (A : Type) where
+ mul : A -> A -> A
+class MulCommSemigroup (A : Type) extends MulSemigroup A where
--- Notation type class instances
-instance [MulMonoid M] : OfNat M 1 where
- ofNat := MulMonoid.one
-instance [MulSemigroup M] : Mul M where
+instance [MulSemigroup A] : Mul A where
mul := MulSemigroup.mul
-instance [MulGroup M] : Div M where
- div := MulGroup.div
-instance [MulGroup M] : Inv M where
- inv := MulGroup.inv
instance [MulSemigroup A] [MulSemigroup B] : MulSemigroup (A × B) where
mul x y := (x.1 * y.1, x.2 * y.2)
+instance [MulCommSemigroup A] [MulCommSemigroup B] : MulCommSemigroup (A × B) where
+
+instance MulSemigroup.instFun {X : Type} [MulSemigroup A] : MulSemigroup (X -> A) where
+ mul f g := fun x => f x * g x
+instance MulCommSemigroup.instFun {X : Type} [MulCommSemigroup A] : MulCommSemigroup (X -> A) where
+
+instance [MulSemigroup A] {n : Nat} : MulSemigroup (A ^ n) := MulSemigroup.instFun
+instance [MulCommSemigroup A] {n : Nat} : MulCommSemigroup (A ^ n) := MulCommSemigroup.instFun
+
+--------------------------------------------------------------------------------
+-- Multiplicative monoids, non-commutative or commutative
+
+class MulMonoid (A : Type) extends MulSemigroup A where
+ one : A
+class MulCommMonoid (A : Type) extends MulMonoid A, MulCommSemigroup A where
+
+instance [MulMonoid A] : OfNat A 1 where
+ ofNat := MulMonoid.one
+
instance [MulMonoid A] [MulMonoid B] : MulMonoid (A × B) where
one := (1, 1)
+instance [MulCommMonoid A] [MulCommMonoid B] : MulCommMonoid (A × B) where
+
+instance MulMonoid.instFun {X : Type} [MulMonoid A] : MulMonoid (X -> A) where
+ one := fun _ => 1
+instance MulCommMonoid.instFun {X : Type} [MulCommMonoid A] : MulCommMonoid (X -> A) where
+
+instance [MulMonoid A] {n : Nat} : MulMonoid (A ^ n) := MulMonoid.instFun
+instance [MulCommMonoid A] {n : Nat} : MulCommMonoid (A ^ n) := MulCommMonoid.instFun
+
+--------------------------------------------------------------------------------
+-- Multiplicative groups, non-commutative or commutative
+
+class MulGroup (A : Type) extends MulMonoid A where
+ div : A -> A -> A
+ inv : A -> A := fun x => div one x
+class MulCommGroup (A : Type) extends MulGroup A, MulCommMonoid A where
+
+instance [MulGroup A] : Div A where
+ div := MulGroup.div
+instance [MulGroup A] : Inv A where
+ inv := MulGroup.inv
+
instance [MulGroup A] [MulGroup B] : MulGroup (A × B) where
div x y := (x.1 / y.1, x.2 / y.2)
+instance [MulCommGroup A] [MulCommGroup B] : MulCommGroup (A × B) where
-instance MulSemigroup.instFun {X : Type} [MulSemigroup M] : MulSemigroup (X -> M) where
- mul f g := fun x => f x * g x
-instance MulMonoid.instFun {X : Type} [MulMonoid M] : MulMonoid (X -> M) where
- one := fun _ => 1
-instance MulGroup.instFun {X : Type} [MulGroup M] : MulGroup (X -> M) where
+instance MulGroup.instFun {X : Type} [MulGroup A] : MulGroup (X -> A) where
div f g := fun x => f x / g x
+instance MulCommGroup.instFun {X : Type} [MulCommGroup A] : MulCommGroup (X -> A) where
-instance [MulSemigroup M] {n : Nat} : MulSemigroup (M ^ n) := MulSemigroup.instFun
-instance [MulMonoid M] {n : Nat} : MulMonoid (M ^ n) := MulMonoid.instFun
-instance [MulGroup M] {n : Nat} : MulGroup (M ^ n) := MulGroup.instFun
+instance [MulGroup A] {n : Nat} : MulGroup (A ^ n) := MulGroup.instFun
+instance [MulCommGroup A] {n : Nat} : MulCommGroup (A ^ n) := MulCommGroup.instFun
--------------------------------------------------------------------------------
-- Fields
--- TODO: Generalize Field/VectorSpace to Ring/Module?
-- Convention: (∀a. div a 0 = 0) and (inv 0 = 0).
class Field (F : Type) extends AddGroup F, MulGroup F
