From ff6ef4f1a1d2b50ee54a74a83780b54060fdd5a9 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <smaug451@gmail.com>
Date: Sat, 16 Nov 2019 15:06:57 +0000
Subject: [PATCH] Direct sums: preparing for vector spaces (#74)

---
 Everything/Safe.agda             |  4 ++++
 Groups/Abelian/DirectSum.agda    | 19 +++++++++++++++++
 Groups/Abelian/Lemmas.agda       |  3 ++-
 Groups/Cyclic/Lemmas.agda        |  5 +++--
 Groups/DirectSum/Definition.agda | 22 +++++++++++---------
 Modules/DirectSum.agda           | 28 +++++++++++++++++++++++++
 Rings/DirectSum.agda             | 35 ++++++++++++++++++++++++++++++++
 Setoids/DirectSum.agda           | 21 +++++++++++++++++++
 Setoids/Setoids.agda             |  6 ------
 Vectors/VectorSpace.agda         | 24 ++++++++++++++++++++++
 10 files changed, 148 insertions(+), 19 deletions(-)
 create mode 100644 Groups/Abelian/DirectSum.agda
 create mode 100644 Modules/DirectSum.agda
 create mode 100644 Rings/DirectSum.agda
 create mode 100644 Setoids/DirectSum.agda
 create mode 100644 Vectors/VectorSpace.agda

diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 35eacc6..fc6500e 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -44,8 +44,10 @@ open import Rings.Orders.Partial.Definition
 open import Rings.Orders.Total.Lemmas
 open import Rings.Orders.Partial.Lemmas
 open import Rings.IntegralDomains
+open import Rings.DirectSum
 
 open import Setoids.Setoids
+open import Setoids.DirectSum
 open import Setoids.Lists
 open import Setoids.Orders
 open import Setoids.Functions.Definition
@@ -57,6 +59,7 @@ open import Sets.FinSet
 open import DecidableSet
 
 open import Vectors
+open import Vectors.VectorSpace
 
 open import KeyValue.KeyValue
 open import KeyValue.LinearStore.Definition
@@ -82,5 +85,6 @@ open import Categories.Dual.Definition
 
 open import Modules.Examples
 open import Modules.Lemmas
+open import Modules.DirectSum
 
 module Everything.Safe where
diff --git a/Groups/Abelian/DirectSum.agda b/Groups/Abelian/DirectSum.agda
new file mode 100644
index 0000000..d5d6d81
--- /dev/null
+++ b/Groups/Abelian/DirectSum.agda
@@ -0,0 +1,19 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Functions
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Numbers.Naturals.Naturals
+open import Sets.FinSet
+open import Groups.Definition
+open import Sets.EquivalenceRelations
+open import Groups.Abelian.Definition
+
+module Groups.Abelian.DirectSum {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+1_ : A → A → A} {_+2_ : B → B → B} {G1' : Group S _+1_} {G2' : Group T _+2_} (G1 : AbelianGroup G1') (G2 : AbelianGroup G2') where
+
+open import Groups.DirectSum.Definition G1' G2'
+open import Setoids.DirectSum S T
+
+directSumAbGroup : AbelianGroup directSumGroup
+AbelianGroup.commutative directSumAbGroup = directSumLift (AbelianGroup.commutative G1) (AbelianGroup.commutative G2)
diff --git a/Groups/Abelian/Lemmas.agda b/Groups/Abelian/Lemmas.agda
index d9a0e37..aacc905 100644
--- a/Groups/Abelian/Lemmas.agda
+++ b/Groups/Abelian/Lemmas.agda
@@ -2,6 +2,7 @@
 
 open import LogicalFormulae
 open import Setoids.Setoids
+open import Setoids.DirectSum
 open import Functions
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Numbers.Naturals.Naturals
@@ -16,7 +17,7 @@ open import Groups.Isomorphisms.Definition
 
 module Groups.Abelian.Lemmas where
 
-directSumAbelianGroup : {m n o p : _} → {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} {underG : Group S _·A_} {underH : Group T _·B_} (G : AbelianGroup underG) (h : AbelianGroup underH) → (AbelianGroup (directSum underG underH))
+directSumAbelianGroup : {m n o p : _} → {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} {underG : Group S _·A_} {underH : Group T _·B_} (G : AbelianGroup underG) (h : AbelianGroup underH) → (AbelianGroup (directSumGroup underG underH))
 AbelianGroup.commutative (directSumAbelianGroup {A = A} {B} G H) = AbelianGroup.commutative G ,, AbelianGroup.commutative H
 
 subgroupOfAbelianIsAbelian : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : B → A} {fHom : GroupHom H G f} → Subgroup G H fHom → AbelianGroup G → AbelianGroup H
diff --git a/Groups/Cyclic/Lemmas.agda b/Groups/Cyclic/Lemmas.agda
index 080a00a..2a3d914 100644
--- a/Groups/Cyclic/Lemmas.agda
+++ b/Groups/Cyclic/Lemmas.agda
@@ -30,8 +30,9 @@ GroupHom.wellDefined (elementPowerHom {S = S} G x) {.y} {y} refl = reflexive
     open Equivalence (Setoid.eq S)
 
 subgroupOfCyclicIsCyclic : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : B → A} {fHom : GroupHom H G f} → Subgroup G H fHom → CyclicGroup G → CyclicGroup H
-CyclicGroup.generator (subgroupOfCyclicIsCyclic {f = f} subgrp record { generator = generator ; cyclic = cyclic }) = {!f generator!}
-CyclicGroup.cyclic (subgroupOfCyclicIsCyclic subgrp gCyclic) = {!!}
+CyclicGroup.generator (subgroupOfCyclicIsCyclic {f = f} subgrp record { generator = generator ; cyclic = cyclic }) = {!!}
+CyclicGroup.cyclic (subgroupOfCyclicIsCyclic {f = f} subgrp record { generator = generator ; cyclic = cyclic }) {a} with cyclic {f a}
+CyclicGroup.cyclic (subgroupOfCyclicIsCyclic {f = f} subgrp record { generator = generator ; cyclic = cyclic }) {a} | N , generator^n=fa = N , {!!}
 
 -- Prefer to prove that subgroup of cyclic is cyclic, then deduce this like with abelian groups
 {-
diff --git a/Groups/DirectSum/Definition.agda b/Groups/DirectSum/Definition.agda
index 17a0979..1e677e5 100644
--- a/Groups/DirectSum/Definition.agda
+++ b/Groups/DirectSum/Definition.agda
@@ -9,14 +9,16 @@ open import Sets.FinSet
 open import Groups.Definition
 open import Sets.EquivalenceRelations
 
-module Groups.DirectSum.Definition where
+module Groups.DirectSum.Definition {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) where
 
-directSum : {m n o p : _} → {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} (G : Group S _·A_) (h : Group T _·B_) → Group (directSumSetoid S T) (λ x1 y1 → (((_&&_.fst x1) ·A (_&&_.fst y1)) ,, ((_&&_.snd x1) ·B (_&&_.snd y1))))
-Group.+WellDefined (directSum {A = A} {B} g h) (s ,, t) (u ,, v) = Group.+WellDefined g s u ,, Group.+WellDefined h t v
-Group.0G (directSum {A = A} {B} g h) = (Group.0G g ,, Group.0G h)
-Group.inverse (directSum {A = A} {B} g h) (g1 ,, h1) = (Group.inverse g g1) ,, (Group.inverse h h1)
-Group.+Associative (directSum {A = A} {B} g h) = Group.+Associative g ,, Group.+Associative h
-Group.identRight (directSum {A = A} {B} g h) = Group.identRight g ,, Group.identRight h
-Group.identLeft (directSum {A = A} {B} g h) = Group.identLeft g ,, Group.identLeft h
-Group.invLeft (directSum {A = A} {B} g h) = Group.invLeft g ,, Group.invLeft h
-Group.invRight (directSum {A = A} {B} g h) = Group.invRight g ,, Group.invRight h
+open import Setoids.DirectSum S T
+
+directSumGroup : Group directSumSetoid (λ x1 y1 → (((_&&_.fst x1) ·A (_&&_.fst y1)) ,, ((_&&_.snd x1) ·B (_&&_.snd y1))))
+Group.+WellDefined directSumGroup (s ,, t) (u ,, v) = Group.+WellDefined G s u ,, Group.+WellDefined H t v
+Group.0G directSumGroup = (Group.0G G ,, Group.0G H)
+Group.inverse directSumGroup (g1 ,, H1) = (Group.inverse G g1) ,, (Group.inverse H H1)
+Group.+Associative directSumGroup = Group.+Associative G ,, Group.+Associative H
+Group.identRight directSumGroup = Group.identRight G ,, Group.identRight H
+Group.identLeft directSumGroup = Group.identLeft G ,, Group.identLeft H
+Group.invLeft directSumGroup = Group.invLeft G ,, Group.invLeft H
+Group.invRight directSumGroup = Group.invRight G ,, Group.invRight H
diff --git a/Modules/DirectSum.agda b/Modules/DirectSum.agda
new file mode 100644
index 0000000..e77a551
--- /dev/null
+++ b/Modules/DirectSum.agda
@@ -0,0 +1,28 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Groups.Abelian.Definition
+open import Numbers.Naturals.Naturals
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Modules.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Modules.DirectSum {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*R_ : A → A → A} (R : Ring S _+R_ _*R_) {m n o p : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} {G : AbelianGroup G'} {_·1_ : A → M → M} {N : Set o} {U : Setoid {o} {p} N} {_+'_ : N → N → N} {H' : Group U _+'_} {H : AbelianGroup H'} {_·2_ : A → N → N} (M1 : Module R G _·1_) (M2 : Module R H _·2_) where
+
+open import Groups.Abelian.DirectSum G H
+open import Setoids.DirectSum T U
+
+directSumModule : Module R directSumAbGroup λ r mn → ((r ·1 (_&&_.fst mn)) ,, (r ·2 (_&&_.snd mn)))
+Module.dotWellDefined directSumModule r=s t=u = directSumLift (Module.dotWellDefined M1 r=s (_&&_.fst t=u)) (Module.dotWellDefined M2 r=s (_&&_.snd t=u))
+Module.dotDistributesLeft directSumModule = directSumLift (Module.dotDistributesLeft M1) (Module.dotDistributesLeft M2)
+Module.dotDistributesRight directSumModule = directSumLift (Module.dotDistributesRight M1) (Module.dotDistributesRight M2)
+Module.dotAssociative directSumModule = directSumLift (Module.dotAssociative M1) (Module.dotAssociative M2)
+Module.dotIdentity directSumModule = directSumLift (Module.dotIdentity M1) (Module.dotIdentity M2)
diff --git a/Rings/DirectSum.agda b/Rings/DirectSum.agda
new file mode 100644
index 0000000..559aa28
--- /dev/null
+++ b/Rings/DirectSum.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.DirectSum.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Naturals
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.DirectSum {a b c d : _} {A : Set a} {S : Setoid {a} {b} A} {_+1_ : A → A → A} {_*1_ : A → A → A} {C : Set c} {T : Setoid {c} {d} C} {_+2_ : C → C → C} {_*2_ : C → C → C} (R1 : Ring S _+1_ _*1_) (R2 : Ring T _+2_ _*2_) where
+
+open import Setoids.DirectSum S T
+
+pairPlus : A && C → A && C → A && C
+pairPlus (a ,, b) (c ,, d) = (a +1 c) ,, (b +2 d)
+
+pairTimes : A && C → A && C → A && C
+pairTimes (a ,, b) (c ,, d) = (a *1 c) ,, (b *2 d)
+
+directSumRing : Ring directSumSetoid pairPlus pairTimes
+Ring.additiveGroup directSumRing = directSumGroup (Ring.additiveGroup R1) (Ring.additiveGroup R2)
+Ring.*WellDefined directSumRing r=t s=u = directSumLift (Ring.*WellDefined R1 (_&&_.fst r=t) (_&&_.fst s=u)) (Ring.*WellDefined R2 (_&&_.snd r=t) (_&&_.snd s=u))
+Ring.1R directSumRing = Ring.1R R1 ,, Ring.1R R2
+Ring.groupIsAbelian directSumRing = directSumLift (Ring.groupIsAbelian R1) (Ring.groupIsAbelian R2)
+Ring.*Associative directSumRing = directSumLift (Ring.*Associative R1) (Ring.*Associative R2)
+Ring.*Commutative directSumRing = directSumLift (Ring.*Commutative R1) (Ring.*Commutative R2)
+Ring.*DistributesOver+ directSumRing = directSumLift (Ring.*DistributesOver+ R1) (Ring.*DistributesOver+ R2)
+Ring.identIsIdent directSumRing = directSumLift (Ring.identIsIdent R1) (Ring.identIsIdent R2)
diff --git a/Setoids/DirectSum.agda b/Setoids/DirectSum.agda
new file mode 100644
index 0000000..59845e8
--- /dev/null
+++ b/Setoids/DirectSum.agda
@@ -0,0 +1,21 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Functions
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import LogicalFormulae
+open import Sets.EquivalenceRelations
+open import Setoids.Setoids
+
+module Setoids.DirectSum {m n o p : _} {A : Set m} {B : Set n} (R : Setoid {m} {o} A) (S : Setoid {n} {p} B) where
+
+open Setoid
+
+directSumSetoid : Setoid (A && B)
+_∼_ (directSumSetoid) (a ,, b) (c ,, d) = (Setoid._∼_ R a c) && (Setoid._∼_ S b d)
+Equivalence.reflexive (eq (directSumSetoid)) {(a ,, b)} = Equivalence.reflexive (Setoid.eq R) ,, Equivalence.reflexive (Setoid.eq S)
+Equivalence.symmetric (eq (directSumSetoid)) {(a ,, b)} {(c ,, d)} (fst ,, snd) = Equivalence.symmetric (Setoid.eq R) fst ,, Equivalence.symmetric (Setoid.eq S) snd
+Equivalence.transitive (eq (directSumSetoid)) {a ,, b} {c ,, d} {e ,, f} (fst1 ,, snd1) (fst2 ,, snd2) = Equivalence.transitive (Setoid.eq R) fst1 fst2 ,, Equivalence.transitive (Setoid.eq S) snd1 snd2
+
+directSumLift : {r s : A} {t u : B} → (Setoid._∼_ R r s) → (Setoid._∼_ S t u) → Setoid._∼_ directSumSetoid (r ,, t) (s ,, u)
+_&&_.fst (directSumLift r=s t=u) = r=s
+_&&_.snd (directSumLift r=s t=u) = t=u
diff --git a/Setoids/Setoids.agda b/Setoids/Setoids.agda
index 4f159ae..e5ce69f 100644
--- a/Setoids/Setoids.agda
+++ b/Setoids/Setoids.agda
@@ -41,12 +41,6 @@ module Setoids.Setoids where
   Equivalence.symmetric (eq (reflSetoid A)) {b} {.b} refl = refl
   Equivalence.transitive (eq (reflSetoid A)) {b} {.b} {.b} refl refl = refl
 
-  directSumSetoid : {m n o p : _} → {A : Set m} {B : Set n} → (r : Setoid {m} {o} A) → (s : Setoid {n} {p} B) → Setoid (A && B)
-  _∼_ (directSumSetoid r s) (a ,, b) (c ,, d) = (Setoid._∼_ r a c) && (Setoid._∼_ s b d)
-  Equivalence.reflexive (eq (directSumSetoid r s)) {(a ,, b)} = Equivalence.reflexive (Setoid.eq r) ,, Equivalence.reflexive (Setoid.eq s)
-  Equivalence.symmetric (eq (directSumSetoid r s)) {(a ,, b)} {(c ,, d)} (fst ,, snd) = Equivalence.symmetric (Setoid.eq r) fst ,, Equivalence.symmetric (Setoid.eq s) snd
-  Equivalence.transitive (eq (directSumSetoid r s)) {a ,, b} {c ,, d} {e ,, f} (fst1 ,, snd1) (fst2 ,, snd2) = Equivalence.transitive (Setoid.eq r) fst1 fst2 ,, Equivalence.transitive (Setoid.eq s) snd1 snd2
-
   record SetoidInjection {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
     open Setoid S renaming (_∼_ to _∼A_)
     open Setoid T renaming (_∼_ to _∼B_)
diff --git a/Vectors/VectorSpace.agda b/Vectors/VectorSpace.agda
new file mode 100644
index 0000000..ac3bf4a
--- /dev/null
+++ b/Vectors/VectorSpace.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Groups.Abelian.Definition
+open import Numbers.Naturals.Naturals
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Modules.Definition
+open import Fields.Fields
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Vectors.VectorSpace {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+R_ _*_) {m n : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} (G : AbelianGroup G') (_·_ : A → M → M) where
+
+record VectorSpace : Set (lsuc a ⊔ b ⊔ m ⊔ n) where
+  field
+    isModule : Module R G _·_
+    isField : Field R