quotient universal property

src/Algebra/Group/QuotientProperties.ard

@@ -0,0 +1,59 @@
+\import Algebra.Group
+\import Algebra.Group.Sub
+\import Algebra.Monoid
+\import Algebra.Monoid.Category
+\import Algebra.Pointed
+\import Algebra.Pointed.Category
+\import Category (Cat, Precat)
+\import Category.Functor
+\import Category.Meta
+\import Category.Subcat
+\import Equiv
+\import Function
+\import Function.Meta
+\import Logic
+\import Logic.Meta
+\import Paths
+\import Paths.Meta
+\import Relation.Equivalence
+\import Set.Category
+\import Algebra.Group.Category
+\open Group
+\open Algebra.Group.Sub
+
+\func universal-quotient-morphism-setwise {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G)
+                                          (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) >==
+    f (inverse y) * (f x) ==< inv func-* >==
+    f (inverse y * x) ==< lemma' f N p r >== ide `qed)
+  \where
+    \lemma lemma' {x y : G} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel)
+                 (r : N.contains ((inverse y) * x)) : f (inverse y * x) = ide =>
+      f (inverse y * x) ==< p ((inverse y) * x) r >== ide `qed
+
+\func uqms {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel) => universal-quotient-morphism-setwise f N p
+
+\func universal-quotient-morphism-multiplicative {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel)
+                                                 (x y : N.quotient) : uqms f N p (x N.quotient.* y) = (uqms f N p x) * (uqms f N p y) \elim x, y
+  | in~ a, in~ a1 => uqms f N p ((in~ a) N.quotient.* (in~ a1)) ==< idp >== uqms f N p (in~ (a * a1))
+                                                                              ==< idp >== f (a * a1) ==< f.func-* >== (f a) * (f a1)
+                                                                                                                        ==< pmap ((f a)*) idp >== (f a) * uqms f N p (in~ a1)
+                                                                                                                                                    ==< pmap (\lam x => x * uqms f N p (in~ a1)) idp >==
+                                                                                                                                                  (uqms f N p (in~ a)) * (uqms f N p (in~ a1)) `qed
+
+\func universal-quotient-morph {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G)
+                               (p : N SubGroupPreorder.<= f.Kernel) : GroupHom N.quotient 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} => universal-quotient-morphism-multiplicative f N p x y
+
+
+\lemma universal-quotient-property {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G)
+                                 (p : N SubGroupPreorder.<= f.Kernel) :  (universal-quotient-morph f N p) GroupCat.∘ N.quotient-map = f
+  => exts (\lam (x : G) => ((universal-quotient-morph f N p) GroupCat.∘ N.quotient-map) x ==< idp >==
+  (universal-quotient-morph f N p) (N.quotient-map x) ==< idp >==
+  (universal-quotient-morph f N p) (in~ x) ==< idp >== f x `qed)
+
+

src/Algebra/Group/Sub.ard

@@ -1,4 +1,5 @@
 \import Algebra.Group
+\import Algebra.Group.Category
 \import Algebra.Meta
 \import Algebra.Monoid
 \import Algebra.Monoid.Sub
@@ -7,9 +8,10 @@
 \import Paths
 \import Paths.Meta
 \import Relation.Equivalence
-\import Set
+\import Order.PartialOrder
 \open Group
 
+
 \class SubGroup \extends SubMonoid {
   \override S : Group
   | contains_inverse {x : S} : contains x -> contains (inverse x)
@@ -37,6 +39,14 @@
   \override S : Group
 }
 
+\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
+  | <=-transitive {H K N : SubGroup G}
+                  (p : \Pi (g : G) -> H.contains g -> K.contains g)
+                  (q : \Pi (g : G) -> K.contains g -> N.contains g)
+  => \lam(g : G)(r : H.contains g) => q g (p g r)
+
 \class NormalSubGroup \extends SubGroup {
   | isNormal (g : S) {h : S} : contains h -> contains (conjugate g h)
 
@@ -69,6 +79,10 @@
     | inverse-right {x} => cases x \with {
       | in~ a => pmap in~ inverse-right
     }
+  \func quotient-map : GroupHom S quotient \cowith
+    | func (s : S) => in~ s
+    | func-ide => idp
+    | func-* => idp
 }
 
 \class SubAddGroup \extends SubAddMonoid {