refactoring

src/Algebra/Group/QuotientProperties.ard

@@ -21,21 +21,7 @@
 \open Group
 \open Algebra.Group.Sub
 
-\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 =>
-  N.quotient.ide ==< idp >==
-  in~ ide ==< inv (~-pequiv help-condition) >==
-  in~ a `qed
-  \where
-    \func help-condition : a N.equivalence.~ 1 => N.equivalence.~-symmetric {1} {a} (N.contains->equiv p)
-
-{- | probably it can be re-done with Quotient.in-surj function -}
-\func projectionIsSurj {G : Group} (N : NormalSubGroup G) : isSurj (quotient-map {G} {N}) =>
-  \lam (z : G / N) => \case \elim z \with{
-    | in~ a => inP (a, quotient-map a ==< idp >== in~ a `qed)
-  }
-
+\func \infix 7 // (G : Group) (H : NormalSubGroup G) : Group => H.quotient
 
 {- | properties needed from a commutative triangle $$X \to Y \to Z$$ in the category of groups -}
 \class GroupTriangle{
@@ -103,7 +89,7 @@
    - of quotient groups. Basically, it proves
    - that the function universalQuotientMorphismSetwise
    - indeed gives a group homomorphism. Thus the arrow $G/N \xrightarrow{\text{uqms}} H$ indeed lies in Group-}
-  \func universalQuotientMorph  : GroupHom (G / N) H \cowith
+  \func universalQuotientMorph  : GroupHom (G // N) H \cowith
     | func => uqms
     | func-ide => uqms  N.quotient.ide ==< idp >== uqms  (in~ 1) ==< idp >== f ide ==< f.func-ide >== ide `qed
     | func-* {x y : N.quotient} => universalQuotientMorphismMultiplicative x y
@@ -125,36 +111,34 @@
 
   \func Triangle : GroupTriangle \cowith
     | X => G
-    | Y => G / f.Kernel
+    | Y => G // f.Kernel
     | Z => H
     | f => quot
     | g => UniversalProperties.universalQuotientMorph
     | h => f
     | comm => UniversalProperties.universalQuotientProperty
 
-  \func univ : GroupHom (G / f.Kernel) H => UniversalProperties.universalQuotientMorph
-  \func quot : GroupHom G (G / f.Kernel) => quotient-map
+  \func univ : GroupHom (G // f.Kernel) H => UniversalProperties.universalQuotientMorph
+  \func quot : GroupHom G (G // f.Kernel) => quotient-map
 
   \lemma universalKerProp : univ GroupCat.∘ quot = f
     => UniversalProperties.universalQuotientProperty
 
-  \lemma universalQuotientKernel (g : G / f.Kernel)
+  \lemma universalQuotientKernel (g : G // f.Kernel)
                                  (q : univ g = ide) : g = f.Kernel.quotient.ide
     => \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 => univ z = ide) p q))
+      | in~ a, p => inv (f.Kernel.criterionForKernel a (universalQuotientKernel' a  (transport (\lam z => univ z = ide) p q))
                         )
     }
     \where{
       \func helper-1 (a : G)
                      (q : univ (in~ a) = ide) : in~ a = f.Kernel.quotient.ide =>
-        inv (kernelEquivProp f.Kernel a (universalQuotientKernel' a q))
+        inv (f.Kernel.criterionForKernel a (universalQuotientKernel' a q))
     }
 
 
   \func evidTrivKer : univ.TrivialKernel =>
-    \lam {g : G / f.Kernel} (p : univ.Kernel.contains g) => universalQuotientKernel g p
+    \lam {g : G // f.Kernel} (p : univ.Kernel.contains g) => universalQuotientKernel g p
 
   \lemma universalQuotientKernel'  (a : G)
                                   (q : univ (in~ a) = ide) : f.Kernel.contains a
@@ -172,7 +156,7 @@
   \lemma univKer-mono : isInj univ.func => univ.Kernel-injectivity-test evidTrivKer
 
   \func univKer-epi (p : isSurj f): isSurj univ
-    => Triangle.surjectivity-2-out-3 p (projectionIsSurj f.Kernel)
+    => Triangle.surjectivity-2-out-3 p f.Kernel.quotIsSurj
 
   \func FirstIsoTheorem (p : isSurj f) : univ.isIsomorphism => (univKer-mono, univKer-epi p)
 }

src/Algebra/Group/Sub.ard

@@ -5,7 +5,9 @@
 \import Algebra.Pointed
 \import Data.Bool
 \import Equiv
+\import Function
 \import Function.Meta
+\import Logic
 \import Logic.Meta
 \import Meta
 \import Paths
@@ -95,19 +97,25 @@
                   (q : \Pi (g : G) -> K.contains g -> N.contains g)
   => \lam (g : G) (r : H.contains g) => q g (p g r)
 
+\func kernelEquivProp {G : Group} (N : NormalSubGroup G) (a : G) (p : N.contains a) : N.quotient.ide = in~ a =>
+  N.quotient.ide ==< idp >==
+  in~ ide ==< inv (~-pequiv help-condition) >==
+  in~ a `qed
+  \where
+    \func help-condition : a N.equivalence.~ 1 => N.equivalence.~-symmetric {1} {a} (N.contains->equiv p)
 
 \class NormalSubGroup \extends SubGroup {
   | isNormal (g : S) {h : S} : contains h -> contains (conjugate g h)
 
---  \lemma isNormal' (g : S) {h : S} (c : contains h) : contains (g * h * inverse g)
---    => simplify in isNormal g c
+  \lemma isNormal' (g : S) {h : S} (c : contains h) : contains ((inverse g) * h * g)
+    => simplify in isNormal (inverse g) c
 
   \func quotient : Group Cosets \cowith
     | ide => in~ 1
     | * (x y : Cosets) : Cosets \with {
       | in~ g, in~ g' => in~ (g Group.* g')
       | in~ g, ~-equiv x y r =>  ~-pequiv $ rewriteEq (inverse_*, inverse-left {S} {g}, ide-left) r
-      | ~-equiv x y r, in~ g =>  ~-pequiv $ rewriteEq inverse_* $ transport contains equation (isNormal g r)
+      | ~-equiv x y r, in~ g =>  ~-pequiv $ rewriteEq inverse_* $ transport contains equation (isNormal' g r)
     }
     | ide-left {x} => cases x \with {
       | in~ a => pmap in~ ide-left
@@ -132,6 +140,16 @@
 
   \func quotient-proj-setwise : SetHom S quotient \cowith
     | func s => in~ s
+
+  \func criterionForKernel (a : S) (p : contains a) : quotient.ide = in~ a => rewrite (inv (~-pequiv help-condition)) idp
+    \where
+      \func help-condition : a equivalence.~ 1 => equivalence.~-symmetric {1} {a} (contains->equiv p)
+
+  {- | probably it can be re-done with Quotient.in-surj function -}
+  \func quotIsSurj : isSurj quotient-proj-setwise =>
+    \lam (z : quotient) => \case \elim z \with{
+      | in~ a => inP (a, quotient-proj-setwise a ==< idp >== in~ a `qed)
+    }
 }
 
 \class SubAddGroup \extends SubAddMonoid {