The orbit category of a group (#935)

src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md

@@ -11,6 +11,7 @@ open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types
+open import foundation.iterated-dependent-product-types
 open import foundation.propositions
 open import foundation.sets
 open import foundation.subtypes
@@ -97,37 +98,24 @@ module _
   (hom-set : A → A → Set l2)
   (comp-hom : composition-operation-binary-family-Set hom-set)
   where
-
-  is-associative-prop-composition-operation-binary-family-Set : Prop (l1 ⊔ l2)
-  is-associative-prop-composition-operation-binary-family-Set =
-    Π-Prop' A
-    ( λ x →
-      Π-Prop' A
-      ( λ y →
-        Π-Prop' A
-        ( λ z →
-          Π-Prop' A
-          ( λ w →
-            Π-Prop
-            ( type-Set (hom-set z w))
-            ( λ h →
-              Π-Prop
-              ( type-Set (hom-set y z))
-              ( λ g →
-                Π-Prop
-                ( type-Set (hom-set x y))
-                ( λ f →
-                  Id-Prop
-                    ( hom-set x w)
-                    ( comp-hom (comp-hom h g) f)
-                    ( comp-hom h (comp-hom g f)))))))))
-
   is-prop-is-associative-composition-operation-binary-family-Set :
     is-prop
       ( is-associative-composition-operation-binary-family-Set hom-set comp-hom)
   is-prop-is-associative-composition-operation-binary-family-Set =
-    is-prop-type-Prop
-      is-associative-prop-composition-operation-binary-family-Set
+    is-prop-iterated-implicit-Π 4
+      ( λ x y z w →
+        is-prop-iterated-Π 3
+          ( λ h g f →
+            is-set-type-Set
+              ( hom-set x w)
+              ( comp-hom (comp-hom h g) f)
+              ( comp-hom h (comp-hom g f))))
+
+  is-associative-prop-composition-operation-binary-family-Set : Prop (l1 ⊔ l2)
+  pr1 is-associative-prop-composition-operation-binary-family-Set =
+    is-associative-composition-operation-binary-family-Set hom-set comp-hom
+  pr2 is-associative-prop-composition-operation-binary-family-Set =
+    is-prop-is-associative-composition-operation-binary-family-Set
 ```
 
 ### Being unital is a property of composition operations in binary families of sets

src/category-theory/isomorphisms-in-precategories.lagda.md

@@ -165,8 +165,7 @@ module _
   where
 
   iso-eq-Precategory :
-    (x y : obj-Precategory C) →
-    x ＝ y → iso-Precategory C x y
+    (x y : obj-Precategory C) → x ＝ y → iso-Precategory C x y
   pr1 (iso-eq-Precategory x y p) = hom-eq-Precategory C x y p
   pr2 (iso-eq-Precategory x .x refl) = is-iso-id-hom-Precategory C
 

src/category-theory/replete-subprecategories.lagda.md

@@ -291,7 +291,7 @@ module _
   is-unfixed-replete-subprecategory-is-category-Subprecategory {x} =
     ind-iso-Category
       ( C , is-category-C)
-      ( λ B e → is-in-iso-Subprecategory C P e)
+      ( λ B → is-in-iso-Subprecategory C P)
       ( is-in-iso-id-Subprecategory C P x)
 
   is-replete-subprecategory-is-category-Subprecategory :

src/foundation/binary-relations.lagda.md

@@ -210,10 +210,10 @@ module _
   pr2 (extensionality-Relation-Prop S) =
     is-equiv-relates-same-elements-eq-Relation-Prop S
 
-  equivalence-relationates-same-elements-Relation-Prop :
+  eq-relates-same-elements-Relation-Prop :
     (S : Relation-Prop l2 A) →
     relates-same-elements-Relation-Prop R S → (R ＝ S)
-  equivalence-relationates-same-elements-Relation-Prop S =
+  eq-relates-same-elements-Relation-Prop S =
     map-inv-equiv (extensionality-Relation-Prop S)
 ```
 

src/foundation/coslice.lagda.md

@@ -53,17 +53,17 @@ module _
   {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : X → A) (g : X → B)
   where
 
-  hom-coslice = Σ (A → B) (λ h → (h ∘ f) ~ g)
+  hom-coslice = Σ (A → B) (λ h → h ∘ f ~ g)
 
 module _
   {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {f : X → A} {g : X → B}
   where
 
-  map-hom-coslice : hom-coslice f g → (A → B)
+  map-hom-coslice : hom-coslice f g → A → B
   map-hom-coslice = pr1
 
   triangle-hom-coslice :
-    (h : hom-coslice f g) → ((map-hom-coslice h) ∘ f) ~ g
+    (h : hom-coslice f g) → map-hom-coslice h ∘ f ~ g
   triangle-hom-coslice = pr2
 ```
 
@@ -95,7 +95,7 @@ module _
     (h k : hom-coslice f g) → (h ＝ k) ≃ htpy-hom-coslice h k
   extensionality-hom-coslice (h , H) =
     extensionality-Σ
-      ( λ {h' : A → B} (H' : (h' ∘ f) ~ g) (K : h ~ h') → H ~ ((K ·r f) ∙h H'))
+      ( λ {h' : A → B} (H' : h' ∘ f ~ g) (K : h ~ h') → H ~ ((K ·r f) ∙h H'))
       ( refl-htpy)
       ( refl-htpy)
       ( λ h' → equiv-funext)

src/foundation/equivalence-relations.lagda.md

@@ -100,10 +100,10 @@ module _
   pr2 (extensionality-equivalence-relation S) =
     is-equiv-relate-same-elements-eq-equivalence-relation S
 
-  equivalence-relationate-same-elements-equivalence-relation :
+  eq-relate-same-elements-equivalence-relation :
     (S : equivalence-relation l2 A) →
     relate-same-elements-equivalence-relation R S → (R ＝ S)
-  equivalence-relationate-same-elements-equivalence-relation S =
+  eq-relate-same-elements-equivalence-relation S =
     map-inv-equiv (extensionality-equivalence-relation S)
 ```
 
@@ -319,7 +319,7 @@ is-section-equivalence-relation-partition-equivalence-relation :
   {l : Level} {A : UU l} (R : equivalence-relation l A) →
   equivalence-relation-partition (partition-equivalence-relation R) ＝ R
 is-section-equivalence-relation-partition-equivalence-relation R =
-  equivalence-relationate-same-elements-equivalence-relation
+  eq-relate-same-elements-equivalence-relation
     ( equivalence-relation-partition (partition-equivalence-relation R))
     ( R)
     ( relate-same-elements-equivalence-relation-partition-equivalence-relation
@@ -551,7 +551,7 @@ is-retraction-equivalence-relation-Surjection-Into-Set :
     ( surjection-into-set-equivalence-relation R) ＝
   R
 is-retraction-equivalence-relation-Surjection-Into-Set R =
-  equivalence-relationate-same-elements-equivalence-relation
+  eq-relate-same-elements-equivalence-relation
     ( equivalence-relation-Surjection-Into-Set
       ( surjection-into-set-equivalence-relation R))
     ( R)

src/foundation/identity-systems.lagda.md

@@ -105,9 +105,12 @@ module _
   abstract
     fundamental-theorem-id-is-identity-system :
       is-identity-system B a b →
-      (f : (x : A) → a ＝ x → B x) → (x : A) → is-equiv (f x)
-    fundamental-theorem-id-is-identity-system H f =
-      fundamental-theorem-id
-        ( is-torsorial-is-identity-system H)
-        ( f)
+      (f : (x : A) → a ＝ x → B x) → is-fiberwise-equiv f
+    fundamental-theorem-id-is-identity-system H =
+      fundamental-theorem-id (is-torsorial-is-identity-system H)
 ```
+
+## External links
+
+- [Identity systems](https://1lab.dev/1Lab.Path.IdentitySystem.html) at 1lab
+- [identity system](https://ncatlab.org/nlab/show/identity+system) at $n$Lab

src/group-theory.lagda.md

@@ -16,7 +16,9 @@ open import group-theory.cartesian-products-monoids public
 open import group-theory.cartesian-products-semigroups public
 open import group-theory.category-of-abelian-groups public
 open import group-theory.category-of-concrete-groups public
+open import group-theory.category-of-group-actions public
 open import group-theory.category-of-groups public
+open import group-theory.category-of-orbits-groups public
 open import group-theory.category-of-semigroups public
 open import group-theory.cayleys-theorem public
 open import group-theory.centers-groups public

src/group-theory/category-of-group-actions.lagda.md

@@ -0,0 +1,71 @@
+# The category of group actions
+
+```agda
+module group-theory.category-of-group-actions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.isomorphisms-in-large-precategories
+open import category-theory.large-categories
+open import category-theory.large-precategories
+open import category-theory.precategories
+
+open import foundation.dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.universe-levels
+
+open import group-theory.group-actions
+open import group-theory.groups
+open import group-theory.homomorphisms-group-actions
+open import group-theory.isomorphisms-group-actions
+open import group-theory.precategory-of-group-actions
+```
+
+</details>
+
+## Idea
+
+The [large category](category-theory.large-categories.md) of
+[group actions](group-theory.group-actions.md) consists of group actions and
+[morphisms of group actions](group-theory.homomorphisms-group-actions.md)
+between them.
+
+## Definitions
+
+### The large category of `G`-sets
+
+```agda
+module _
+  {l1 : Level} (G : Group l1)
+  where
+
+  is-large-category-action-Group-Large-Category :
+    is-large-category-Large-Precategory (action-Group-Large-Precategory G)
+  is-large-category-action-Group-Large-Category X =
+    fundamental-theorem-id
+      ( is-torsorial-iso-action-Group G X)
+      ( iso-eq-Large-Precategory (action-Group-Large-Precategory G) X)
+
+  action-Group-Large-Category :
+    Large-Category (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
+  large-precategory-Large-Category action-Group-Large-Category =
+      action-Group-Large-Precategory G
+  is-large-category-Large-Category action-Group-Large-Category =
+    is-large-category-action-Group-Large-Category
+```
+
+### The small category of `G`-sets
+
+```agda
+module _
+  {l1 : Level} (G : Group l1)
+  where
+
+  action-Group-Category :
+    (l2 : Level) → Category (l1 ⊔ lsuc l2) (l1 ⊔ l2)
+  action-Group-Category =
+    category-Large-Category (action-Group-Large-Category G)
+```

src/group-theory/category-of-orbits-groups.lagda.md

@@ -0,0 +1,102 @@
+# The orbit category of a group
+
+```agda
+module group-theory.category-of-orbits-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.full-large-subcategories
+open import category-theory.isomorphisms-in-large-precategories
+open import category-theory.large-categories
+open import category-theory.large-precategories
+open import category-theory.precategories
+
+open import foundation.dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.universe-levels
+
+open import group-theory.category-of-group-actions
+open import group-theory.group-actions
+open import group-theory.groups
+open import group-theory.homomorphisms-group-actions
+open import group-theory.isomorphisms-group-actions
+open import group-theory.precategory-of-group-actions
+open import group-theory.transitive-group-actions
+```
+
+</details>
+
+## Idea
+
+The **orbit category of a group** `𝒪(G)` is the
+[full subcategory](category-theory.full-large-subcategories.md) of the
+[category of `G`-sets](group-theory.category-of-group-actions.md) consisting of
+orbits of `G`, i.e. [transitive](group-theory.transitive-group-actions.md)
+[`G`-sets](group-theory.group-actions.md). Equivalently, an orbit of `G` is a
+`G`-set that is
+[merely equivalent](group-theory.mere-equivalences-group-actions.md) to a
+quotient `G`-set `G/H` for some [subgroup](group-theory.subgroups.md) `H`.
+
+## Definitions
+
+### The large orbit category of a group
+
+```agda
+module _
+  {l1 : Level} (G : Group l1)
+  where
+
+  orbit-Group-Full-Large-Subcategory :
+    Full-Large-Subcategory (l1 ⊔_) (action-Group-Large-Category G)
+  orbit-Group-Full-Large-Subcategory = is-transitive-prop-action-Group G
+
+  orbit-Group-Large-Category :
+    Large-Category (λ l → l1 ⊔ lsuc l) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
+  orbit-Group-Large-Category =
+    large-category-Full-Large-Subcategory
+      ( action-Group-Large-Category G)
+      ( orbit-Group-Full-Large-Subcategory)
+```
+
+### The large orbit precategory of a group
+
+```agda
+module _
+  {l1 : Level} (G : Group l1)
+  where
+
+  orbit-Group-Large-Precategory :
+    Large-Precategory (λ l → l1 ⊔ lsuc l) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
+  orbit-Group-Large-Precategory =
+    large-precategory-Large-Category (orbit-Group-Large-Category G)
+```
+
+### The small orbit category of a group
+
+```agda
+module _
+  {l1 : Level} (G : Group l1)
+  where
+
+  orbit-Group-Category : (l2 : Level) → Category (l1 ⊔ lsuc l2) (l1 ⊔ l2)
+  orbit-Group-Category = category-Large-Category (orbit-Group-Large-Category G)
+```
+
+### The small orbit precategory of a group
+
+```agda
+module _
+  {l1 : Level} (G : Group l1)
+  where
+
+  orbit-Group-Precategory : (l2 : Level) → Precategory (l1 ⊔ lsuc l2) (l1 ⊔ l2)
+  orbit-Group-Precategory =
+    precategory-Large-Category (orbit-Group-Large-Category G)
+```
+
+## External links
+
+- [orbit category](https://ncatlab.org/nlab/show/orbit+category) at $n$Lab

src/group-theory/cayleys-theorem.lagda.md

@@ -33,12 +33,12 @@ module _
 
   map-Cayleys-theorem :
     type-Group G → type-Group (symmetric-Group (set-Group G))
-  map-Cayleys-theorem x = equiv-mul-Group G x
+  map-Cayleys-theorem = equiv-mul-Group G
 
   preserves-mul-map-Cayleys-theorem :
     preserves-mul-Group G (symmetric-Group (set-Group G)) map-Cayleys-theorem
   preserves-mul-map-Cayleys-theorem {x} {y} =
-    eq-htpy-equiv (λ z → associative-mul-Group G x y z)
+    eq-htpy-equiv (associative-mul-Group G x y)
 
   hom-Cayleys-theorem : hom-Group G (symmetric-Group (set-Group G))
   pr1 hom-Cayleys-theorem = map-Cayleys-theorem

src/group-theory/congruence-relations-abelian-groups.lagda.md

@@ -203,9 +203,9 @@ extensionality-congruence-Ab :
 extensionality-congruence-Ab A =
   extensionality-congruence-Group (group-Ab A)
 
-equivalence-relationate-same-elements-congruence-Ab :
+eq-relate-same-elements-congruence-Ab :
   {l1 l2 : Level} (A : Ab l1) (R S : congruence-Ab l2 A) →
   relate-same-elements-congruence-Ab A R S → R ＝ S
-equivalence-relationate-same-elements-congruence-Ab A =
-  equivalence-relationate-same-elements-congruence-Group (group-Ab A)
+eq-relate-same-elements-congruence-Ab A =
+  eq-relate-same-elements-congruence-Group (group-Ab A)
 ```

src/group-theory/congruence-relations-commutative-monoids.lagda.md

@@ -179,11 +179,11 @@ extensionality-congruence-Commutative-Monoid :
 extensionality-congruence-Commutative-Monoid M =
   extensionality-congruence-Monoid (monoid-Commutative-Monoid M)
 
-equivalence-relationate-same-elements-congruence-Commutative-Monoid :
+eq-relate-same-elements-congruence-Commutative-Monoid :
   {l1 l2 : Level} (M : Commutative-Monoid l1)
   (R S : congruence-Commutative-Monoid l2 M) →
   relate-same-elements-congruence-Commutative-Monoid M R S → R ＝ S
-equivalence-relationate-same-elements-congruence-Commutative-Monoid M =
-  equivalence-relationate-same-elements-congruence-Monoid
+eq-relate-same-elements-congruence-Commutative-Monoid M =
+  eq-relate-same-elements-congruence-Monoid
     ( monoid-Commutative-Monoid M)
 ```