mono property

src/Algebra/Group/QuotientProperties.ard

@@ -16,17 +16,26 @@
 \import Paths
 \import Paths.Meta
 \import Relation.Equivalence
+\import Set
 \import Set.Category
 \import Algebra.Group.Category
 \open Group
 \open Algebra.Group.Sub
 
-\func Quot {G H : Group}(f : GroupHom G H) : Group => f.Kernel.quotient
+-- \func Quot {G H : Group}(f : GroupHom G H) : Group => f.Kernel.quotient
+
+\func surjectivityProperty {X Y Z : BaseSet} (f : X -> Y) (g : Y -> Z)
+                           (h : X -> Z) (r : h = g SetCat.∘ f) (p : isSurj h) (q : isSurj f) : isSurj g => {?}
+
+\func reduceEqProperty {X Y Z : Group} {f : GroupHom X Y} {g : GroupHom Y Z}
+                           {h : GroupHom X Z} (r : h = g GroupCat.∘ f)  : h.func = g.func SetCat.∘ f.func => {?}
 
 \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 => {?}
 
+\func projectionIsSurj {G : Group} (N : NormalSubGroup G) : isSurj (quotient-map {G} {N}) => {?}
+
 
 {- | 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$.
@@ -36,7 +45,7 @@
                                        (p : N SubGroupPreorder.<= f.Kernel)
                                        (a : N.quotient) : H \elim a
   | in~ n => f n
-  | ~-equiv y x r => equality-check ((inverse (f y)) * (f x) ==< pmap (\lam y => y * (f x)) (inv f.func-inverse) >==
+  | ~-equiv y x r => equality-check (inverse (f y) * (f x) ==< pmap (\lam y => y * (f x)) (inv f.func-inverse) >==
     f (inverse y) * (f x) ==< inv func-* >==
     f (inverse y * x) ==< lemma' f N p r >== ide `qed)
   \where
@@ -82,15 +91,18 @@
   | H : Group
   | f : GroupHom G H
 
-  \func univKer-hom : GroupHom (G / f.Kernel) H => universalQuotientMorph f (f.Kernel) SubGroupPreorder.<=-refl
+  \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 )
+    => \case g \as b, idp : g = b \return b = f.Kernel.quotient.ide\with{
+      | in~ a, p => inv (
+        kernelEquivProp f.Kernel a
+            (universalQuotientKernel' a  (transport (\lam z => univKer-hom z = ide) p q))
+                        )
     }
     \where{
       \func helper-1 (a : G)
@@ -119,7 +131,6 @@
 
   \func univKer-epi (p : isSurj f): isSurj univKer-hom.func => {?}
 
-
   \func FirstIsoTheorem (p : isSurj f) : univKer-hom.isIsomorphism => (univKer-mono, univKer-epi p)
 }