symgeoalg

commit ac23319ad43c3fc9ba4faca00e030df81e5c7d2c
parent b0c224155a3dd9e82dc3d20ed3ba51d4771b1549
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Sat, 27 Jul 2024 15:45:27 -0700

Reorganize additive structures

Diffstat:
M
Main.lean
 | 
55
+++++++++++++++++++++++++++++++------------------------

1 file changed, 31 insertions(+), 24 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -77,50 +77,57 @@ class Inv (α : Type) where
   inv : α -> α
 
 --------------------------------------------------------------------------------
--- Single additive operator algebraic structures, all implicitly commutative
--- TODO: separate these like MulX
+-- Additive (commutative) semigroups
 
 class AddSemigroup (A : Type) where
   add : A -> A -> A
+
+instance [AddSemigroup A] : Add A where
+  add := AddSemigroup.add
+
+instance [AddSemigroup A] [AddSemigroup B] : AddSemigroup (A × B) where
+  add x y := (x.1 + y.1, x.2 + y.2)
+
+instance AddSemigroup.instFun {X : Type} [AddSemigroup A] : AddSemigroup (X -> A) where
+  add f g := fun x => f x + g x
+
+instance [AddSemigroup A] {n : Nat} : AddSemigroup (A ^ n) := AddSemigroup.instFun
+
+--------------------------------------------------------------------------------
+-- Additive (commutative) monoids
+
 class AddMonoid (A : Type) extends AddSemigroup A where
   zero : A
+
+instance [AddMonoid A] : OfNat A 0 where
+  ofNat := AddMonoid.zero
+
+instance [AddMonoid A] [AddMonoid B] : AddMonoid (A × B) where
+  zero := (0, 0)
+
+instance AddMonoid.instFun {X : Type} [AddMonoid A] : AddMonoid (X -> A) where
+  zero := fun _ => 0
+
+instance [AddMonoid A] {n : Nat} : AddMonoid (A ^ n) := AddMonoid.instFun
+
+--------------------------------------------------------------------------------
+-- Additive (commutative) groups
+
 class AddGroup (A : Type) extends AddMonoid A where
   sub : A -> A -> A
   neg : A -> A := fun x => sub zero x
 
--- Notation type class instances
--- 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
-  add := AddSemigroup.add
 instance [AddGroup A] : Sub A where
   sub := AddGroup.sub
 instance [AddGroup A] : Neg A where
   neg := AddGroup.neg
 
-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 AddSemigroup.instFun {X : Type} [AddSemigroup A] : AddSemigroup (X -> A) where
-  add f g := fun x => f x + g x
-instance AddMonoid.instFun {X : Type} [AddMonoid A] : AddMonoid (X -> A) where
-  zero := fun _ => 0
 instance AddGroup.instFun {X : Type} [AddGroup A] : AddGroup (X -> A) where
   sub f g := fun x => f x - g x
 
-instance [AddSemigroup A] {n : Nat} : AddSemigroup (A ^ n) := AddSemigroup.instFun
-instance [AddMonoid A] {n : Nat} : AddMonoid (A ^ n) := AddMonoid.instFun
 instance [AddGroup A] {n : Nat} : AddGroup (A ^ n) := AddGroup.instFun
 
 --------------------------------------------------------------------------------