upd names and future staff

JetBrains · Mar 24, 2024 · cd5bfdb · cd5bfdb
1 parent 44a1e68
commit cd5bfdb
Show file tree

Hide file tree

Showing 8 changed files with 58 additions and 29 deletions.
diff --git a/.gitignore b/.gitignore
@@ -4,6 +4,7 @@
 /meta/.idea/
 bin
 *.iml
+*DS_Store*
 
 # Created by https://www.gitignore.io/api/vim
 

diff --git a/src/Algebra/Group/Category.ard b/src/Algebra/Group/Category.ard
@@ -95,7 +95,21 @@
       | func-* => idp
   }
 
-
+--\instance ImageMonoid (f : MonoidHom) : Monoid
+--  | Pointed => ImageMulPointed f
+--  | * a b => (a.1 * b.1, \case a.2, b.2 \with {
+--    | inP t, inP s => inP (t.1 * s.1, func-* *> pmap2 (*) t.2 s.2)
+--  })
+--  | ide-left => ext ide-left
+--  | ide-right => ext ide-right
+--  | *-assoc => ext *-assoc
+
+\instance ImageGroup (f : GroupHom) : Group
+  | Monoid => ImageMonoid f
+  | inverse (x, p) => (inverse x, get-inverse p)
+  | inverse-left => {?}
+  | inverse-right => {?}
+  \where \func get-inverse{x : f.Cod}  (p : ∃ (g : f.Dom)(f g =  x)) :  ∃ (g : f.Dom)(f g = inverse x) => {?}
 
 \record AddGroupHom \extends AddMonoidHom {
   \override Dom : AddGroup

diff --git a/src/Algebra/Group/GSet.ard b/src/Algebra/Group/GSet.ard
@@ -36,13 +36,15 @@
       (inverse m * m) ** s ==< pmap (\lam x => x ** s) inverse-left >==
       ide ** s ==< id-action >==
       s `qed
+
+  \func choosePoint (e : E) => action-by-subgroup (Stabilizer e)
 }
 
 \class TransitiveGroupAction \extends GroupAction {
   | trans : \Pi (v v' : E) -> ∃ (g : G) (g ** v = v')
 }
 
-\func action-by-subgroup (G : Group) (H : SubGroup G) : GroupAction G \cowith
+\func action-by-subgroup {G : Group} (H : SubGroup G) : GroupAction G \cowith
   | E => H.Cosets
   | ** (g : G) (e : H.Cosets) : H.Cosets \with {
     | g, in~ a => in~ (g * a)

diff --git a/src/Algebra/Group/GSetCat.ard b/src/Algebra/Group/GSetCat.ard
@@ -1,34 +1,38 @@
 \import Algebra.Group
 \import Algebra.Group.GSet
 \import Category
+\import Category.Meta
 \import Function (isInj, isSurj)
 \import Function.Meta ($)
 \import Paths
+\import Paths.Meta
 \import Set
 \import Set.Category
 
 \record EquivariantMaps (G : Group) \extends SetHom{
   \override Dom : GroupAction G
   \override Cod : GroupAction G
-  | **-equiv {e : Dom} {g : G} : func (g ** e) = g ** func e
+  | func-** {e : Dom} {g : G} : func (g ** e) = g ** func e -- equivariance
 
   \func isIso => \Sigma (isSurj func) (isInj func)
 }
 
+
 \func id-equivar {G : Group} (X : GroupAction G) : EquivariantMaps G { | Dom => X | Cod => X} \cowith
   | func (x : X) => x
-  | **-equiv {x : X} {g : G} => idp
+  | func-** {x : X} {g : G} => idp
 
-\instance GSet (G : Group) : Precat (GroupAction G)
+\instance GSet (G : Group) : Cat (GroupAction G)
   | Hom A B => EquivariantMaps G { | Dom => A | Cod => B}
   | id X => id-equivar X
   | o {x y z : GroupAction G} (g : EquivariantMaps G y z) (f : EquivariantMaps G x y) => \new EquivariantMaps G {
     | func (a : x) => g (f a)
-    | **-equiv {a : x} {h : G} =>
-      g ( f (h ** a)) ==< pmap g **-equiv >==
-      g (h ** f a) ==< **-equiv >==
+    | func-** {a : x} {h : G} =>
+      g ( f (h ** a)) ==< pmap g func-** >==
+      g (h ** f a) ==< func-** >==
       h ** (g (f a)) `qed
   }
   | id-left => idp
   | id-right => idp
-  | o-assoc => idp
+  | o-assoc => idp
+  | univalence => sip \lam e _ => exts \lam g x => func-** {e}
diff --git a/src/Algebra/Group/QuotientProperties.ard b/src/Algebra/Group/QuotientProperties.ard
@@ -21,9 +21,9 @@
 \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
+\func universalQuotientMorphismSetwise {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-* >==
@@ -33,27 +33,27 @@
                  (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 uqms {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel) => universalQuotientMorphismSetwise 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
+\func universalQuotientMorphismMultiplicative {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 universalQuotientMorph {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
+  | func-* {x y : N.quotient} => universalQuotientMorphismMultiplicative 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.∘ quotient-map = f
-  => exts (\lam (x : G) => ((universal-quotient-morph f N p) GroupCat.∘ quotient-map) x ==< idp >==
-  (universal-quotient-morph f N p) (quotient-map x) ==< idp >==
-  (universal-quotient-morph f N p) (in~ x) ==< idp >== f x `qed)
+\lemma universalQuotientProperty {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G)
+                                 (p : N SubGroupPreorder.<= f.Kernel) :  (universalQuotientMorph f N p) GroupCat.∘ quotient-map = f
+  => exts (\lam (x : G) => ((universalQuotientMorph f N p) GroupCat.∘ quotient-map) x ==< idp >==
+  (universalQuotientMorph f N p) (quotient-map x) ==< idp >==
+  (universalQuotientMorph f N p) (in~ x) ==< idp >== f x `qed)
 
 
diff --git a/src/Algebra/Group/Sub.ard b/src/Algebra/Group/Sub.ard
@@ -32,13 +32,8 @@
   \func Cosets => Quotient (equivalence.~)
 
   \lemma invariant-right-multiplication {x y : S} (p : 1 equivalence.~ y) : in~{S} {equivalence.~} x = in~ {S} {equivalence.~} (x * y) => {?}
---    in~ {S} {equivalence.~} x = in~ {S} {equivalence.~} (x * y) =>
---    in~ {S} {equivalence.~} x ==< pmap (in~ {S} {equivalence.~}) (inv ide-right) >==
---    in~ {S} {equivalence.~} (x * 1) ==<
-
-  \lemma equivalence-to-1 {x y : S} (p : x equivalence.~ y) : 1 equivalence.~ inverse x * y
-    => {?}
 
+  \lemma equivalence-to-1 {x y : S} (p : x equivalence.~ y) : 1 equivalence.~ inverse x * y => {?}
 
 } \where {
   \func cStruct {G : CGroup} (S : SubGroup G) : CGroup \cowith

diff --git a/src/Algebra/Monoid/Category.ard b/src/Algebra/Monoid/Category.ard
@@ -251,6 +251,15 @@
   | zro-right => ext zro-right
   | +-assoc => ext +-assoc
 
+\instance ImageMonoid (f : MonoidHom) : Monoid
+  | Pointed => ImageMulPointed f
+  | * a b => (a.1 * b.1, \case a.2, b.2 \with {
+    | inP t, inP s => inP (t.1 * s.1, func-* *> pmap2 (*) t.2 s.2)
+  })
+  | ide-left => ext ide-left
+  | ide-right => ext ide-right
+  | *-assoc => ext *-assoc
+
 \func ImageMonoidLeftHom (f : AddMonoidHom) : AddMonoidHom f.Dom (ImageAddMonoid f) \cowith
   | AddPointedHom => ImagePointedLeftHom f
   | func-+ => ext func-+

diff --git a/src/Algebra/Pointed/Category.ard b/src/Algebra/Pointed/Category.ard
@@ -66,6 +66,10 @@
 \instance ImageAddPointed (f : AddPointedHom) : AddPointed (Image f)
   | zro => (0, inP (0, func-zro))
 
+\instance ImageMulPointed (f : PointedHom) : Pointed (Image f)
+  | ide => (ide, inP (ide, func-ide))
+
+
 \func ImagePointedLeftHom (f : AddPointedHom) : AddPointedHom f.Dom (ImageAddPointed f) \cowith
   | func a => (f a, inP (a, idp))
   | func-zro => ext func-zro
-Original file line number
+Diff line change
@@ Expand Up / @@ -4,6 +4,7 @@ @@
     /meta/.idea/
     bin
     *.iml
+    *DS_Store*
     # Created by https://www.gitignore.io/api/vim
@@ Expand Down @@