diff --git a/source/alignment.mmt b/source/alignment.mmt new file mode 100644 index 0000000000000000000000000000000000000000..b24dc3c662018a04b95a7bc1b6204c49104810ee --- /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 0000000000000000000000000000000000000000..379fcb2630374ce0e6006f694fe15721f4dfb689 --- /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