Merge branch 's3midetnov-representation'

src/Algebra/Group.ard

@@ -1,7 +1,10 @@
+\import Algebra.Meta
 \import Algebra.Monoid
 \import Algebra.Monoid.Category
+\import Algebra.Pointed
 \import Data.Array
 \import Data.Or
+\import Equiv
 \import Function.Meta ($)
 \import Logic
 \import Meta
@@ -13,9 +16,16 @@
 
 \class Group \extends CancelMonoid {
   | inverse : E -> E
+
   | inverse-left {x : E} : inverse x * x = ide
   | inverse-right {x : E} : x * inverse x = ide
 
+  \default inverse-left => make-inverse-left inverse inverse-right
+  \default inverse-right => make-inverse-left {Monoid.op} inverse inverse-left
+
+  \default ide-left {x} => make-ide-left E (*) ide inverse *-assoc ide-right inverse-right inverse-left x
+  \default ide-right {x} => make-ide-left E (\lam (x y : E) => y * x) ide inverse (\lam {x y z : E} => inv (*-assoc {_} {z} {y} {x})) ide-left inverse-left inverse-right x
+
   | cancel_*-left x {y} {z} p =>
       y                   ==< inv ide-left >==
       ide * y             ==< pmap (`* y) (inv inverse-left) >==
@@ -96,28 +106,49 @@
                 (\new Inv e (inverse e) inverse-left inverse-right)
                 (\new Inv e' (inverse e') inverse-left inverse-right)
     }
-}
-
-\func conjugate {E : Group} (g : E) (h : E) : E => g * h * inverse g
-
-\func conjugate-via-id {E : Group} (g : E) : conjugate E.ide g = g =>
-  conjugate E.ide g ==< idp >==
-  E.ide * g * inverse E.ide ==< E.*-assoc >==
-  E.ide * (g * inverse E.ide) ==< E.ide-left >==
-  g * (inverse E.ide) ==< pmap (g * ) E.inverse_ide >==
-  g * E.ide ==< E.ide-right >==
-  g `qed
-
-\func conjugate-id  {E : Group} (g : E) : conjugate g E.ide = E.ide =>
-  conjugate g E.ide ==< idp >==
-  g * E.ide * (inverse g) ==< pmap (\lam z => z * (inverse g)) E.ide-right >==
-  g * (inverse g) ==< E.inverse-right >==
-  E.ide `qed
-
 
+  \private \lemma make-inverse-left {M : Monoid} (inverse : M -> M) (inverse-right : \Pi {x : M} -> x * inverse x = ide) {x : M} : inverse x * x = ide
+    => \have | inverse-x-idempotent : (inverse x * x) * (inverse x * x) = inverse x * x =>
+                (inverse x * x) * (inverse x * x) ==< *-assoc >==
+                inverse x * (x * (inverse x * x)) ==< pmap (inverse x *) (inv *-assoc) >==
+                inverse x * ((x * inverse x) * x) ==< cong inverse-right >==
+                inverse x * (ide * x)             ==< inv *-assoc >==
+                (inverse x * ide) * x             ==< cong ide-right >==
+                inverse x * x                     `qed
+             | idempotent-is-trivial {a : M} (a-idempotent : a * a = a) : a = ide =>
+                a                   ==< inv ide-right >==
+                a * ide             ==< cong (inv inverse-right) >==
+                a * (a * inverse a) ==< inv *-assoc >==
+                (a * a) * inverse a ==< cong a-idempotent >==
+                a * inverse a       ==< inverse-right >==
+                ide                 `qed
+       \in idempotent-is-trivial inverse-x-idempotent
+
+  -- TODO: Use semigroup
+  \private \lemma make-ide-left (X : \Set) (* : X -> X -> X) (ide : X) (inverse : X -> X)
+                       (*-assoc : \Pi {x y z : X} -> * (* x y) z = * x (* y z))
+                       (ide-right : \Pi {x : X} -> * x ide = x)
+                       (inverse-right : \Pi {x : X} -> * x (inverse x) = ide)
+                       (inverse-left : \Pi {x : X} -> * (inverse x) x = ide)
+                       (x : X) : * ide x = x =>
+    * ide x                ==< pmap (* __ x) (inv inverse-right) >==
+    * (* x (inverse x)) x  ==< *-assoc >==
+    * x (* (inverse x) x)  ==< cong inverse-left >==
+    * x ide                ==< ide-right >==
+    x                      `qed
+
+
+  \func translate-is-Equiv {G : Group} (h : G) : QEquiv (h *) \cowith
+    | ret => inverse h *
+    | ret_f _ => rewrite (inv G.*-assoc, G.inverse-left, G.ide-left) idp
+    | f_sec _ => rewrite (inv G.*-assoc, G.inverse-right, G.ide-left) idp
+}
 
 \func \infixl 7 / {G : Group} (x y : G) => x * inverse y
 
+\func conjugate {E : Group} (g h : E)
+  => g * h * inverse g
+
 \class AddGroup \extends AddMonoid {
   | negative : E -> E
   | negative-left {x : E} : negative x + x = zro

src/Algebra/Group/Aut.ard

@@ -1,4 +1,6 @@
 \import Algebra.Group
+\import Algebra.Monoid
+\import Category
 \import Paths
 
 \instance Aut {A : \1-Type} (a : A) : Group (a = a)
@@ -9,4 +11,10 @@
   | *-assoc {x} {y} {z} => *>-assoc x y z
   | inverse => inv
   | inverse-left {x} => inv_*> x
-  | inverse-right {x} => *>_inv x
+
+\func End {C : Precat} (c : C) : Monoid (Hom c c) \cowith
+  | ide => id c
+  | * => ∘
+  | ide-left => id-left
+  | ide-right => id-right
+  | *-assoc => o-assoc

src/Algebra/Group/Category.ard

@@ -1,10 +1,11 @@
 \import Algebra.Group
 \import Algebra.Group.Sub
+\import Algebra.Meta
 \import Algebra.Monoid
 \import Algebra.Monoid.Category
 \import Algebra.Pointed
 \import Algebra.Pointed.Category
-\import Category (Cat, Precat)
+\import Category (Cat, Iso)
 \import Category.Functor
 \import Category.Meta
 \import Category.Subcat
@@ -13,6 +14,7 @@
 \import Function.Meta
 \import Logic
 \import Logic.Meta
+\import Meta
 \import Paths
 \import Paths.Meta
 \import Set.Category
@@ -22,6 +24,8 @@
   \override Dom : Group
   \override Cod : Group
 
+  | func-ide => cancel_*-left (func ide) $ inv func-* *> pmap func ide-left *> inv ide-right
+
   \lemma func-inverse {x : Dom} : func (inverse x) = inverse (func x) => check-for-inv $
     func x * func (inverse x)   ==< inv func-* >==
     func (x * inverse x)        ==< pmap func inverse-right >==
@@ -38,13 +42,13 @@
       ide `qed
 
     | isNormal g {h} p =>
-      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 >==
+      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 =>
@@ -68,17 +72,16 @@
   \lemma Kernel-injectivity-corrolary (p : isInj func) : TrivialKernel =>
     \lam q => p (q *> inv func-ide)
 
-  \func isIsomorphism : \Prop => \Sigma (isInj func) (isSurj func)
+  \func IsIsomorphism : \Prop => \Sigma (isInj func) (isSurj func)
 }
 
-\func quotient-map {S : Group} {H : NormalSubGroup S} : GroupHom S H.quotient \cowith
-  | func (s : S) => NormalSubGroup.quotient-proj-setwise s
-  | func-ide => idp
-  | func-* => idp
-
 \instance GroupCat : Cat Group
   | Hom => GroupHom
-  | id => id
+  | id (G : Group) : GroupHom G G \cowith {
+    | func x => x
+    | func-ide => idp
+    | func-* => idp
+  }
   | o {x y z : Group} (g : GroupHom y z) (f : GroupHom x y) => \new GroupHom {
     | func x => g (f x)
     | func-ide => pmap g f.func-ide *> g.func-ide
@@ -89,18 +92,101 @@
   | o-assoc => idp
   | univalence => sip \lam f _ => exts (func-ide {f}, \lam _ _ => func-* {f}, \lam _ => GroupHom.func-inverse {f})
   \where {
-    \func id (M : Group) : GroupHom M M \cowith
-      | func x => x
-      | func-ide => idp
-      | func-* => idp
+    \func ForgetSet : FaithfulFunctor GroupCat SetCat \cowith
+      | F G => G
+      | Func f => f
+      | Func-id => idp
+      | Func-o => idp
+      | isFaithful => \lam p => ext p
+
+    -- TODO: Prove this more generally for algebraic theories?
+    \lemma Iso<->Inj+Surj {G H : Group} (f : GroupHom G H) : Iso {GroupCat} f <-> f.IsIsomorphism
+      => (\lam p => SetIso->Inj+Surj (ForgetSet.Func-iso p),
+          \lam p => \new Iso {
+            | hinv => \new GroupHom {
+              | func => inve p
+              | func-ide => aux (this_iso p) f.func-ide
+              | func-* {x y : H} => rewrite (this_inv_ap p x, this_inv_ap p y,
+                                             inv f.func-*, inv $ inv_this_ap p (inve p x G.* inve p y),
+                                             inv $ this_inv_ap p x, inv $ this_inv_ap p y ) idp
+            }
+            | hinv_f => exts \lam e => inv (inv_this_ap p e)
+            | f_hinv => exts \lam e => inv (this_inv_ap p e)
+          })
+      \where \private {
+      {- | some  set theoretic lemmas -}
+
+        \lemma this_inv_ap (p : f.IsIsomorphism) (h : H) : h = f (inve p h)
+          => inv (path \lam i => (Iso.f_hinv {this_iso p} i) h)
+
+        \lemma inv_this_ap (p : f.IsIsomorphism) (g : G) : g = inve p (f g)
+          => inv (path \lam i => (Iso.hinv_f {this_iso p} i) g)
+
+        \func this_iso (p : f.IsIsomorphism) => Inj+Surj->SetIso f p.1 p.2
+
+        \func inve (p : f.IsIsomorphism) => Iso.hinv {this_iso p}
+
+        \lemma aux {A B : \Set} (f : Iso {SetCat} {A} {B}) {a : A} {b : B} (p : f.f a = b) : f.hinv b = a
+          => inv $ rewrite (aux' f, p) idp
+
+        \lemma aux' {A B : \Set} (f : Iso {SetCat} {A} {B}) {a : A} : a = f.hinv (f.f a)
+          => inv (path (\lam i => (f.hinv_f i) a))
+
+        \lemma aux'' {A B : \Set} (f : Iso {SetCat} {A} {B}) {b : B} : b = f.f (f.hinv b)
+          => inv (path (\lam i => (f.f_hinv i) b))
+
+        \lemma SetIso->Inj+Surj(f : Iso {SetCat}) : \Sigma (isInj f.f) (isSurj f.f)
+          => (Equiv.isInj {SetIso->Equiv f}, Equiv.isSurj {SetIso->Equiv f})
+
+        \lemma Inj+Surj->SetIso {X Y : \Set} (f : X -> Y) (p : isInj f) (q : isSurj f) : Iso {SetCat} f
+          => Equiv->SetIso (Equiv.fromInjSurj f p q)
+
+        \lemma Equiv->SetIso {X Y : \Set} {f : X -> Y} (eq : Equiv f) : Iso {SetCat} f \cowith
+          | hinv => Equiv.ret {eq}
+          | hinv_f => ext (Equiv.ret_f {eq})
+          | f_hinv => ext (Equiv.f_ret {eq})
+
+        \lemma SetIso->Equiv {X Y : \Set} {f : X -> Y} (p : Iso {SetCat} f) : Equiv f => \new QEquiv {
+          | ret => Iso.hinv {p}
+          | ret_f x => inv (aux' p {x})
+          | f_sec y => inv (aux'' p {y})
+        }
+      }
+
+    \lemma Iso<->TrivialKer+Surj {G H : Group} (f : GroupHom G H)
+      : Iso {GroupCat} f <-> (\Sigma f.TrivialKernel (isSurj f))
+      => <->trans (Iso<->Inj+Surj f) helper
+      \where \private \func helper : (\Sigma (isInj f)(isSurj f)) <-> (\Sigma f.TrivialKernel (isSurj f)) =>
+        (\lam p => (f.Kernel-injectivity-corrolary p.1, p.2),
+         \lam p => (f.Kernel-injectivity-test p.1, p.2))
   }
 
+\func quotient-map {S : Group} {H : NormalSubGroup S} : GroupHom S H.quotient \cowith
+  | func (s : S) => NormalSubGroup.quotient-proj-setwise s
+  | func-ide => idp
+  | func-* => idp
+
 \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 ImageGroupLeftHom (f : GroupHom) : GroupHom f.Dom (ImageGroup f) \cowith
+  | MonoidHom => ImageMonoidLeftHom f
+
+\func ImageGroupRightHom (f : GroupHom) : GroupHom (ImageGroup f) f.Cod \cowith
+  | MonoidHom => ImageMonoidRightHom f
+
+\func ImageSubGroup (f : GroupHom) : SubGroup f.Cod \cowith
+  | contains h => ∃(g : f.Dom)(f g = h)
+  | contains_ide => inP (Group.ide {f.Dom}, f.func-ide)
+  | contains_* cont1 cont2 => \case \elim  cont1, \elim  cont2 \with {
+    | inP a, inP b => inP(a.1 * b.1, rewrite (f.func-*, a.2, b.2) idp)
+  }
+  | contains_inverse cont1 => \case \elim cont1 \with {
+    | inP a => inP (inverse a.1, rewrite (f.func-inverse, a.2) idp)
+  }
 
 \record AddGroupHom \extends AddMonoidHom {
   \override Dom : AddGroup
@@ -191,12 +277,27 @@
   | negative-left => ext negative-left
   | negative-right => ext negative-right
 
-\func ImageGroupLeftHom (f : AddGroupHom) : AddGroupHom f.Dom (ImageAddGroup f) \cowith
-  | AddMonoidHom => ImageMonoidLeftHom f
+\func ImageAddGroupLeftHom (f : AddGroupHom) : AddGroupHom f.Dom (ImageAddGroup f) \cowith
+  | AddMonoidHom => ImageAddMonoidLeftHom f
 
-\func ImageGroupRightHom (f : AddGroupHom) : AddGroupHom (ImageAddGroup f) f.Cod \cowith
-  | AddMonoidHom => ImageMonoidRightHom f
+\func ImageAddGroupRightHom (f : AddGroupHom) : AddGroupHom (ImageAddGroup f) f.Cod \cowith
+  | AddMonoidHom => ImageAddMonoidRightHom f
 
 \instance ImageAbGroup {A : AddGroup} {B : AbGroup} (f : AddGroupHom A B) : AbGroup
   | AddGroup => ImageAddGroup f
-  | AbMonoid => ImageAbMonoid f
+  | AbMonoid => ImageAbMonoid f
+
+\func conjugateHom {E : Group} (g : E) : GroupHom E E \cowith
+  | func => conjugate g
+  | func-ide => unfold conjugate $ rewrite (E.ide-right, E.inverse-right) idp
+  | func-* {x y : E} =>
+    \have aux {x y z w t e : E} : x * y * z * (w * t * e) = (x * y) * (z * w) * (t * e) => equation
+    \in inv $ rewrite (aux, E.inverse-left, E.ide-right) equation
+
+\lemma conjugate-via-id {G : Group} {g : G} : conjugate ide g = g =>
+  conjugate ide g ==< idp >==
+  ide * g * inverse ide ==< *-assoc >==
+  ide * (g * inverse ide) ==< ide-left >==
+  g * inverse ide ==< pmap (g *) inverse_ide >==
+  g * ide ==< ide-right >==
+  g `qed

src/Algebra/Group/GSet.ard

@@ -1,23 +1,15 @@
 \import Algebra.Group
 \import Algebra.Group.Sub
-\import Algebra.Meta
 \import Algebra.Monoid
-\import Algebra.Monoid.Sub
 \import Algebra.Pointed
-\import Equiv
-\import Function
-\import Function.Meta ($)
 \import Logic
 \import Logic.Meta
 \import Paths
-\import Paths.Meta
 \import Relation.Equivalence
 \import Set
-\import Algebra.Monoid
-\import Set.Category
 
 \class GroupAction (G : Group) \extends BaseSet {
-  | \infixl 8 ** : G -> E -> E -- priority should be bigger than that of "+" in LModule (=7)
+  | \infixl 8 ** : G -> E -> E -- priority should be bigger than priority of "+" in LModule (=7)
   | **-assoc {m n : G} {e : E} : m ** (n ** e) = (m * n) ** e
   | id-action {e : E} : ide ** e = e
 
@@ -81,17 +73,3 @@
                               in~ a1 `qed
                            )
    }
-
--- action by conjugating its own elements
-\func conjAction (G : Group) : GroupAction G \cowith
-  | E => G
-  | ** (g : G)  => conjugate g
-  | **-assoc {m : G} {n : G} {e : G} : conjugate m (conjugate n e) = conjugate (m * n) e =>
-  conjugate m (conjugate n e) ==< pmap (conjugate m) idp >==
-  conjugate m (n * e * inverse n ) ==< idp >==
-  m * (n * e * inverse n ) * inverse m ==< lemma-par >==
-  (m * n) * e * (inverse n * inverse m) ==< pmap ((m * n * e) *) (inv G.inverse_*) >==
-  (m * n) * e * (inverse (m * n)) ==< idp >==
-  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