From 358e6d87025dbe40c6c9673e1025455de32bdc1a Mon Sep 17 00:00:00 2001
From: Markus Pfeiffer <markus.pfeiffer@morphism.de>
Date: Tue, 27 Jun 2017 14:04:14 +0100
Subject: [PATCH] Add outline

Add an outline of the needed structures for GAP and the example
we intent to implement.
---
 source/alignment.mmt       |  1 +
 source/draft-structure.mmt | 54 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 source/alignment.mmt
 create mode 100644 source/draft-structure.mmt

diff --git a/source/alignment.mmt b/source/alignment.mmt
new file mode 100644
index 0000000..b24dc3c
--- /dev/null
+++ b/source/alignment.mmt
@@ -0,0 +1 @@
+namespace http://www.gap-system.org j
\ No newline at end of file
diff --git a/source/draft-structure.mmt b/source/draft-structure.mmt
new file mode 100644
index 0000000..379fcb2
--- /dev/null
+++ b/source/draft-structure.mmt
@@ -0,0 +1,54 @@
+namespace http://mathhub.info/MitM/smglom/draft-0 
+
+
+import base http://mathhub.info/MitM/Foundation 
+
+// This is an outline of how to design the MitM for group theory 
+//
+// it is divided into 
+//  - abstract theory
+//
+//    - permutation groups
+//    - matrix groups
+//    - finitely presented groups
+
+// Group (abstract)
+
+// Group Homomorphism
+// (needs injective, surjective, bijective at some point
+//  should be inherited from underlying map?)
+
+// Subgroup
+// subset of group that is closed
+
+// AllSubgroups : {G : Group} → Set (of subgroups of G)
+
+// Subgroups via embeddings:
+// subgroup : {G : Group} → (injection H → G)
+
+// Cosets {G : Group} → U : Subgroup G → Set 
+
+
+
+// Group Action (what about pairs?)
+// really these are permutation actions...
+// need both left- and right-actions 
+// left-action : {X : Set} → {G : Group} → X × G → X
+// right-action : {X : Set} → {G : Group} → G × X → X
+//
+// also: action : {X : Set} → {G : Group} → G → SymmetricGroup(X)
+// Formalise the "isomorphism" between the two?
+// What about Automorphism groups of stuff? If we have a graph Γ and a group G
+// then we act on Γ by graph automorphisms
+
+// for any group action `act` we define
+// stabiliser : {act : GroupAction} → groundset act → Subgroup of G
+// orbit : {act : GroupAction} → groundset act → Subset (groundset act)
+// 
+
+// Centraliser
+// Normaliser
+
+// Computational-ish aspects
+
+// GroupByGenerators
\ No newline at end of file
-- 
GitLab