code style fix

JetBrains · Jun 19, 2024 · 0534f12 · 0534f12
1 parent ceaa12a
commit 0534f12
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/src/Algebra/Group/GSet/Category.ard b/src/Algebra/Group/GSet/Category.ard
@@ -11,22 +11,22 @@
 \import Set
 \import Set.Category
 
-\record EquivariantMaps (G : Group) \extends SetHom{
+\record EquivariantMap (G : Group) \extends SetHom{
   \override Dom : GroupAction G
   \override Cod : GroupAction G
   | 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 id-equivar {G : Group} (X : GroupAction G) : EquivariantMap G { | Dom => X | Cod => X} \cowith
   | func (x : X) => x
   | func-** {x : X} {g : G} => idp
 
 \instance GSet (G : Group) : Cat (GroupAction G)
-  | Hom A B => EquivariantMaps G { | Dom => A | Cod => B}
+  | Hom A B => EquivariantMap 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 {
+  | o {x y z : GroupAction G} (g : EquivariantMap G y z) (f : EquivariantMap G x y) => \new EquivariantMap G {
     | func (a : x) => g (f a)
     | func-** {a : x} {h : G} =>
       g ( f (h ** a)) ==< pmap g func-** >==

diff --git a/src/Algebra/Group/GSet/GSet.ard b/src/Algebra/Group/GSet/GSet.ard
@@ -82,6 +82,7 @@
                            )
    }
 
+-- action by conjugating its own elements
 \func conjAction (G : Group) : GroupAction G \cowith
   | E => G
   | ** (g : G)  => conjugate g