mono-half of 1 iso theorem

src/Algebra/Group/Category.ard

@@ -111,8 +111,13 @@
   | inverse-left => ext inverse-left
   | inverse-right => ext inverse-right
 
-\func truncate-hom {G H : Group} (f : GroupHom G H) : GroupHom G (ImageGroup f) => {?}
-
+\func restrictHom {G H : Group} (f : GroupHom G H) : GroupHom G (ImageGroup f) \cowith
+  | func => fnc
+  | func-ide => {?}
+  | func-* {g h : G} : fnc (g * h) = fnc g * fnc h => {?}
+  \where{
+    \func fnc (g : G) : ImageGroup f => (f g, inP (g, idp))
+  }
 \record AddGroupHom \extends AddMonoidHom {
   \override Dom : AddGroup
   \override Cod : AddGroup

src/Algebra/Group/GSet.ard

@@ -101,3 +101,11 @@
   | ** (g : G) (H : SubGroup G) => {?}
   | **-assoc => {?}
   | id-action => {?}
+
+
+
+
+
+
+
+

src/Algebra/Group/GSetType.ard

@@ -21,7 +21,10 @@ of group actions with chosen point in the underlying set -}
   \where \func Stabilizer_ {G : Group} (E : TransitiveGroupAction G) (pt : E) : SubGroup G =>
     E.Stabilizer pt
 
-\func SubgroupsAreTransitiveActions (G : Group) : SubGroup G = TransitivePointedGroupAction G => {?}
+\func subgroup-action-subgroup {G : Group} (x : SubGroup G) : SubGroupByTransitivePointedAction (TransitivePointedActionBySubgroup x) = x
+
+\func SubgroupsAreTransitiveActions (G : Group) : SubGroup G = TransitivePointedGroupAction G =>
+  iso TransitiveActionBySubgroup SubGroupByTransitivePointedAction
 
 \data action-groupoid {G : Group} (E : GroupAction G)
   | pt E.E

src/Algebra/Group/QuotientProperties.ard

@@ -21,6 +21,13 @@
 \open Group
 \open Algebra.Group.Sub
 
+\func Quot {G H : Group}(f : GroupHom G H) : Group => f.Kernel.quotient
+
+\func \infix 7 / (G : Group) (H : NormalSubGroup G) : Group => H.quotient
+
+\func kernelEquivProp {G : Group} (N : NormalSubGroup G) (a : G)(p : N.contains a) : N.quotient.ide = in~ a => {?}
+
+
 {- | a set function that having $G, H$ and $f : G \to H$ and a
  -    normal subgroup $N \leq G$ s.t. $N \leqslant \ker(f)$ produces for each element of $G/N$ an element of $H$.
  - One gets a diagram of the form
@@ -40,6 +47,7 @@
 {- | this a synonym for universalQuotientMorphismSetwise used because it is shorter-}
 \func uqms {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel) => universalQuotientMorphismSetwise f N p
 
+
 {- | this is a proof that in the previous assumptions the function
  - universalQuotientMorphismSetwise is multiplicative -}
 \func universalQuotientMorphismMultiplicative {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel)
@@ -55,7 +63,7 @@
  - that the function universalQuotientMorphismSetwise
  - indeed gives a group homomorphism. Thus the arrow $G/N \xrightarrow{\text{uqms}} H$ indeed lies in Group-}
 \func universalQuotientMorph {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G)
-                             (p : N SubGroupPreorder.<= f.Kernel) : GroupHom N.quotient H \cowith
+                             (p : N SubGroupPreorder.<= f.Kernel) : GroupHom (G / N) H \cowith
   | func => uqms f N p
   | func-ide => uqms f N p N.quotient.ide ==< idp >== uqms f N p (in~ 1) ==< idp >== f ide ==< f.func-ide >== ide `qed
   | func-* {x y : N.quotient} => universalQuotientMorphismMultiplicative f N p x y
@@ -67,11 +75,54 @@
   (universalQuotientMorph f N p) (quotient-map x) ==< idp >==
   (universalQuotientMorph f N p) (in~ x) ==< idp >== f x `qed)
 
-\func help {G H : Group} (f : GroupHom G H) : GroupHom G (ImageGroup f) => {?}
 
-\func FirstIsoHom {G H : Group} (f : GroupHom G H) : GroupHom f.Kernel.quotient (ImageGroup (quotient-map {G} {f.Kernel}))
-  => help kernelMap
-  \where \func kernelMap : GroupHom f.Kernel.quotient H => universalQuotientMorph f f.Kernel SubGroupPreorder.<=-refl
+{- | Now we apply all of these universal properties to the case when N = Ker f and we get the first isomorphism theorem in the end-}
+\class FirstIsomorphismTheorem {
+  | G : Group
+  | H : Group
+  | f : GroupHom G H
+
+  \func univKer-hom : GroupHom (G / f.Kernel) H => universalQuotientMorph f (f.Kernel) SubGroupPreorder.<=-refl
+
+  \lemma universalKerProp : univKer-hom GroupCat.∘ quotient-map = f
+    => universalQuotientProperty f f.Kernel SubGroupPreorder.<=-refl
+
+  \lemma universalQuotientKernel (g : G / f.Kernel)
+                                 (q : univKer-hom g = ide) : g = f.Kernel.quotient.ide
+    => \case g \as b, idp : g = b \with{
+      | in~ a, p => {?} -- inv (kernelEquivProp f.Kernel a )
+    }
+    \where{
+      \func helper-1 (a : G)
+                     (q : univKer-hom (in~ a) = ide) : in~ a = f.Kernel.quotient.ide =>
+        inv (kernelEquivProp f.Kernel a (universalQuotientKernel' a q))
+    }
+
+
+  \func evidTrivKer : univKer-hom.TrivialKernel =>
+    \lam {g : G / f.Kernel} (p : univKer-hom.Kernel.contains g) => universalQuotientKernel g p
+
+  \lemma universalQuotientKernel'  (a : G)
+                                  (q : univKer-hom (in~ a) = ide) : f.Kernel.contains a
+    =>
+      f a ==< inv (technical-helper a) >==
+      univKer-hom (in~ a) ==< q >==
+      ide `qed
+    \where \lemma technical-helper  (a : G) : univKer-hom (in~ a) = f a =>
+      univKer-hom (in~ a) ==< pmap univKer-hom {in~ a} {quotient-map a} idp >==
+      univKer-hom (quotient-map a) ==< idp >==
+      (univKer-hom  GroupCat.∘ quotient-map) a ==< pmap (\lam (z : GroupHom G H) => z a) universalKerProp >==
+      f a `qed
+
+
+  \lemma univKer-mono : isInj univKer-hom.func => univKer-hom.Kernel-injectivity-test evidTrivKer
+
+  \func univKer-epi (p : isSurj f): isSurj univKer-hom.func => {?}
+
+
+  \func FirstIsoTheorem (p : isSurj f) : univKer-hom.isIsomorphism => (univKer-mono, univKer-epi p)
+}
+
 
 
 

src/Algebra/Group/Sub.ard

@@ -12,6 +12,7 @@
 \import Paths.Meta
 \import Relation.Equivalence
 \import Order.PartialOrder
+\import Set
 \import Set.Category
 \open Group
 
@@ -48,6 +49,21 @@
   \override S : Group
 }
 
+\func anotherSubgroupDefinition{G : Group} (X : SubSet G)
+                               (p : \Pi (x y : G) -> X.contains x -> X.contains y -> X.contains ((inverse x) * y))
+                               (q : X.contains ide) : SubGroup G {| contains => X.contains | contains_ide => q} \cowith
+  | contains_* {x y : G} (r : X.contains x) (r' : X.contains y) : X.contains (x * y) => transport (\lam z => X.contains (z * y)) G.inverse-isInv (contains_*' r r')
+  | contains_inverse {g : G} (xi : X.contains g) : X.contains (inverse g) => inv g xi
+  \where {
+    \func helper (g : G) (r : X.contains g) : X.contains (inverse g * G.ide) => p g ide r q
+
+    \func inv (g : G) (r : X.contains g) : X.contains (inverse g) => transport X.contains G.ide-right (helper g r)
+
+    \func contains_*' {x y : G} (r : X.contains x) (r' : X.contains y) : X.contains (inverse (inverse x) * y) => p (inverse x) y (inv x r) r'
+  }
+
+
+
 \instance SubGroupPreorder {G : Group} : Preorder (SubGroup G)
   | <= (H K : SubGroup G) => \Pi (g : G) -> H.contains g -> K.contains g
   | <=-refl {H : SubGroup G} => \lam (g : G) (p : H.contains g) => p
@@ -57,7 +73,7 @@
   => \lam (g : G) (r : H.contains g) => q g (p g r)
 
 
-\lemma pseudo-<=-antisymmetric {G : Group}{x y : SubGroup G} :
+\lemma <=-antisymmetric-contains {G : Group}{x y : SubGroup G} :
   (\Pi (g : G) -> x g -> y g) -> (\Pi (g : G) -> y g -> x g) -> x.contains = y.contains
   => \lam p q => funExt {G} (\lam z => \Prop) (equal-funcs p q)
   \where \lemma equal-funcs {x y : SubGroup G} (p : \Pi (g : G) -> x g -> y g)
@@ -69,12 +85,12 @@
   | <=-antisymmetric {x y : SubGroup G} : (\Pi (g : G) -> x g -> y g) -> (\Pi (g : G) -> y g -> x g) -> x = y
   => {?}
 
-
 \func funExt {A : \Type} (B : A -> \Type) {f g : \Pi (a : A) -> B a}
              (p : \Pi (a : A) -> f a = g a) : f = g
   => path (\lam i => \lam a => p a @ i)
 
 
+
 \func conjSubGrp {G : Group} (g : G) (H : SubGroup G) : SubGroup G \cowith
   | contains h => H.contains (conjugate (inverse g) h)
   | contains_ide => pmap (\lam (u : \Sigma()() -> H.contains_ide)) H.contains_ide (H.contains (conjugate (inverse g) G.ide) ==< pmap H.contains (conjugate-id (inverse g)) >==