small fixes

src/Algebra/Group/Category.ard

@@ -38,13 +38,13 @@
       ide `qed
 
     | isNormal g {h} p =>
-      func (inverse g * h * g)                 ==< func-* >==
-      func (inverse g * h) * func g            ==< pmap (`* func g) func-* >==
-      (func (inverse g) * func h ) * func g    ==< *-assoc >==
-      func (inverse g) *(func h * func g)      ==< pmap (\lam (ee : Cod) => func (inverse g) * (ee * func g)) p >==
-      func (inverse g) * (ide * func g)        ==< pmap (func (inverse g) *) ide-left >==
-      func (inverse g) * func g                ==< pmap (`* func g) func-inverse >==
-      inverse (func g) * func g                ==< inverse-left >==
+      func (g * h * inverse g)                 ==< func-* >==
+      func (g * h) * (func (inverse g))        ==< pmap (`* (func (inverse g))) func-* >==
+      func g * func h * (func (inverse g))     ==< pmap (\lam z => func g * z * (func (inverse g))) p >==
+      func g * ide * (func (inverse g))        ==< pmap (`* (func (inverse g))) ide-right >==
+      func g * (func (inverse g))              ==< inv func-* >==
+      func (g * inverse g)                     ==< pmap func inverse-right >==
+      func ide                                 ==< func-ide >==
       ide `qed
 
     | contains_* {x} {y} p q =>
@@ -95,30 +95,12 @@
       | func-* => idp
   }
 
-\instance B (M : Monoid) : Precat (\Sigma)
-  | Hom _ _ => M
-  | id _ => M.ide
-  | o { _ _ _ : \Sigma} m n => m * n
-  | id-left => ide-left
-  | id-right => ide-right
-  | o-assoc => *-assoc
-
-\instance PSh(G : Group) : \Type => Functor (B G) SetCat
-
 \instance ImageGroup (f : GroupHom) : Group
   | Monoid => ImageMonoid f
   | inverse a => (inverse a.1, TruncP.map a.2 \lam s => (inverse s.1, f.func-inverse *> pmap inverse s.2))
   | inverse-left => ext inverse-left
   | inverse-right => ext inverse-right
 
-\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

src/Algebra/Group/GSetCat.ard → src/Algebra/Group/GSet/Category.ard

@@ -1,5 +1,5 @@
 \import Algebra.Group
-\import Algebra.Group.GSet
+\import Algebra.Group.GSet.GSet
 \import Algebra.Group.Sub
 \import Category
 \import Category.Meta
@@ -19,15 +19,6 @@
   \func isIso => \Sigma (isSurj func) (isInj func)
 }
 
-\func CanonicalMapChoosingPoint-set {G : Group} (E : GroupAction G) (s : E) (e : E.choosePoint s) : E \elim e
-  | in~ a => a ** s
-  | ~-equiv x y r => x ** s ==< {?} >==
-  x ** ((inverse x G.* y) ** s) ==< **-assoc >==
-  (x G.* (inverse x G.* y)) ** s ==< pmap (\lam z => z ** s) (inv G.*-assoc) >==
-  ((x G.* inverse x) G.* y) ** s ==< pmap (\lam z => (z G.* y) ** s) inverse-right >==
-  (G.ide G.* y) ** s ==< pmap (\lam z => z ** s) G.ide-left >==
-   y ** s `qed
-
 \func id-equivar {G : Group} (X : GroupAction G) : EquivariantMaps G { | Dom => X | Cod => X} \cowith
   | func (x : X) => x
   | func-** {x : X} {g : G} => idp

src/Algebra/Group/GSet.ard → src/Algebra/Group/GSet/GSet.ard

@@ -45,7 +45,6 @@
   | trans : \Pi (v v' : E) -> ∃ (g : G) (g ** v = v')
 }
 \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)
@@ -95,11 +94,3 @@
   conjugate (m * n) e `qed
   | id-action {e : G} : conjugate ide e = e => conjugate-via-id e
   \where \lemma lemma-par {a b c d e : G} : a * (b * c * d) * e = (a * b) * c * (d * e) => equation
-
-
-
-
-
-
-
-

src/Algebra/Group/QuotientProperties.ard

@@ -16,14 +16,11 @@
 \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 \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 =>
@@ -64,7 +61,7 @@
 }
 
 
-\class UniversalQuotient {
+\class UniversalGroupQuotient {
   | G : Group
   | H : Group
   | f : GroupHom G H
@@ -122,7 +119,7 @@
 {- | 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 UniversalProperties : UniversalQuotient {| G => G | H => H | f => f} \cowith
+  \func UniversalProperties : UniversalGroupQuotient {| G => G | H => H | f => f} \cowith
     | N => f.Kernel
     | p => SubGroupPreorder.<=-refl
 

src/Algebra/Group/Sub.ard

@@ -96,34 +96,18 @@
   => \lam (g : G) (r : H.contains g) => q g (p g r)
 
 
-\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)
-                            (q : \Pi (g : G) -> y g -> x g) (g : G)  : x g = y g =>
-      ext (p g, q g)
-
-\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
-  => {?}
-
-\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)
-
 \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 (inverse g) c
+--  \lemma isNormal' (g : S) {h : S} (c : contains h) : contains (g * h * inverse g)
+--    => simplify in isNormal 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)
+      | 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)
     }
     | ide-left {x} => cases x \with {
       | in~ a => pmap in~ ide-left
@@ -137,7 +121,7 @@
     | inverse (x : Cosets) : Cosets \with {
       | in~ g => in~ (Group.inverse g)
       | ~-equiv x y r => ~-pequiv $ rewrite inverse-isInv $ rewriteEq (inverse_*, inverse-isInv) in
-                                    contains_inverse (rewriteEq (inverse-right {S} {x}, ide-left) in isNormal' x r)
+                                    contains_inverse (rewriteEq (inverse-right {S} {x}, ide-left) in isNormal x r)
     }
     | inverse-left {x} => cases x \with {
       | in~ a => pmap in~ inverse-left