TheoremOnTransitivePointedAndSubgroupd

src/Algebra/Group/GSet.ard

@@ -44,7 +44,12 @@
   | trans : \Pi (v v' : E) -> ∃ (g : G) (g ** v = v')
 }
 
+\func PointedGroupAction (G : Group) : \Type => \Sigma (E : GroupAction G) (pt : E)
+
+\func TransitivePointedGroupAction (G : Group) : \Type => \Sigma (E : TransitiveGroupAction G) (pt : E)
+
 \func ActionBySubgroup {G : Group} (H : SubGroup G) : GroupAction G \cowith
+  -- comment $$\int_a^b $$
   | E => H.Cosets
   | ** (g : G) (e : H.Cosets) : H.Cosets \with {
     | g, in~ a => in~ (g * a)
@@ -80,4 +85,12 @@
                               in~ (a1 * ide) ==< pmap in~ ide-right >==
                               in~ a1 `qed
                            )
-   }
+   }
+\func TransitivePointedActionBySubgroup {G : Group} (H : SubGroup G) : TransitivePointedGroupAction G
+  => (TransitiveActionBySubgroup H, in~ ide)
+
+\func SubGroupByTransitivePointedAction {G : Group} (E : TransitivePointedGroupAction G) : SubGroup G => Stabilizer_ E.1 E.2
+    \where \func Stabilizer_ {G : Group} (E : TransitiveGroupAction G) (pt : E) : SubGroup G =>
+      E.Stabilizer pt
+
+\func SubgroupsAreTransitiveActions (G : Group) : SubGroup G = TransitivePointedGroupAction G => {?}

src/Algebra/Group/Sub.ard

@@ -53,6 +53,11 @@
                   (q : \Pi (g : G) -> K.contains g -> N.contains g)
   => \lam (g : G) (r : H.contains g) => q g (p g r)
 
+\instance SubGroupPoset {G : Group} : Poset (SubGroup G)
+  | Preorder => SubGroupPreorder
+  | <=-antisymmetric {x y : SubGroup G} : (\Pi (g : G) -> x g -> y g) -> (\Pi (g : G) -> y g -> x g) -> x = y =>
+    \lam p q =>
+
 \class NormalSubGroup \extends SubGroup {
   | isNormal (g : S) {h : S} : contains h -> contains (conjugate g h)