From af39f7d24ef00e3d358abddb9100c665aa3f6c46 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 1 Nov 2023 15:29:30 +0100 Subject: [PATCH 1/5] some refactorings concrete stuff --- src/category-theory/groupoids.lagda.md | 23 ++-- src/group-theory/concrete-groups.lagda.md | 139 +++++++++++++++------- src/group-theory/torsors.lagda.md | 126 +++++++++++--------- 3 files changed, 174 insertions(+), 114 deletions(-) diff --git a/src/category-theory/groupoids.lagda.md b/src/category-theory/groupoids.lagda.md index 1a6a69141c..dd599ebac8 100644 --- a/src/category-theory/groupoids.lagda.md +++ b/src/category-theory/groupoids.lagda.md @@ -75,8 +75,8 @@ module _ id-hom-Groupoid = id-hom-Category category-Groupoid comp-hom-Groupoid : - {x y z : obj-Groupoid} → hom-Groupoid y z → - hom-Groupoid x y → hom-Groupoid x z + {x y z : obj-Groupoid} → + hom-Groupoid y z → hom-Groupoid x y → hom-Groupoid x z comp-hom-Groupoid = comp-hom-Category category-Groupoid associative-comp-hom-Groupoid : @@ -135,30 +135,29 @@ module _ fundamental-theorem-id ( is-contr-equiv' ( Σ ( Σ (type-1-Type X) (λ y → x ＝ y)) - ( λ yp → - Σ ( Σ (pr1 yp ＝ x) (λ q → (q ∙ pr2 yp) ＝ refl)) - ( λ ql → (pr2 yp ∙ pr1 ql) ＝ refl))) + ( λ (y , p) → + Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl)) + ( λ (q , l) → p ∙ q ＝ refl))) ( ( equiv-tot ( λ y → equiv-tot ( λ p → associative-Σ ( y ＝ x) - ( λ q → (q ∙ p) ＝ refl) - ( λ qr → (p ∙ pr1 qr) ＝ refl)))) ∘e + ( λ q → q ∙ p ＝ refl) + ( λ (q , r) → p ∙ q ＝ refl)))) ∘e ( associative-Σ ( type-1-Type X) ( λ y → x ＝ y) - ( λ yp → - Σ ( Σ (pr1 yp ＝ x) (λ q → (q ∙ pr2 yp) ＝ refl)) - ( λ ql → (pr2 yp ∙ pr1 ql) ＝ refl)))) + ( λ (y , p) → + Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl)) + ( λ (q , l) → p ∙ q ＝ refl)))) ( is-contr-iterated-Σ 2 ( is-torsorial-path x , ( x , refl) , ( is-contr-equiv ( Σ (x ＝ x) (λ q → q ＝ refl)) - ( equiv-tot - ( λ q → equiv-concat (inv right-unit) refl)) + ( equiv-tot (λ q → equiv-concat (inv right-unit) refl)) ( is-torsorial-path' refl)) , ( refl , refl) , ( is-proof-irrelevant-is-prop diff --git a/src/group-theory/concrete-groups.lagda.md b/src/group-theory/concrete-groups.lagda.md index cb880865e1..72e6aeb5c5 100644 --- a/src/group-theory/concrete-groups.lagda.md +++ b/src/group-theory/concrete-groups.lagda.md @@ -20,6 +20,8 @@ open import foundation.truncation-levels open import foundation.universe-levels open import group-theory.groups +open import group-theory.semigroups +open import group-theory.monoids open import higher-group-theory.higher-groups @@ -34,7 +36,9 @@ A **concrete group** is a [pointed](structured-types.pointed-types.md) [connected](foundation.0-connected-types.md) [1-type](foundation-core.1-types.md). -## Definition +## Definitions + +### Concrete groups ```agda Concrete-Group : (l : Level) → UU (lsuc l) @@ -101,91 +105,134 @@ module _ ( λ where refl → is-set-type-Concrete-Group)) classifying-1-type-Concrete-Group : Truncated-Type l one-𝕋 - pr1 classifying-1-type-Concrete-Group = - classifying-type-Concrete-Group + pr1 classifying-1-type-Concrete-Group = classifying-type-Concrete-Group pr2 classifying-1-type-Concrete-Group = is-1-type-classifying-type-Concrete-Group Id-BG-Set : (X Y : classifying-type-Concrete-Group) → Set l Id-BG-Set X Y = Id-Set classifying-1-type-Concrete-Group X Y +``` - unit-Concrete-Group : type-Concrete-Group - unit-Concrete-Group = unit-∞-Group ∞-group-Concrete-Group +### The abstract group associated to a concrete group + +```agda +module _ + {l : Level} (G : Concrete-Group l) + where - mul-Concrete-Group : (x y : type-Concrete-Group) → type-Concrete-Group - mul-Concrete-Group = mul-∞-Group ∞-group-Concrete-Group + unit-Concrete-Group : type-Concrete-Group G + unit-Concrete-Group = unit-∞-Group (∞-group-Concrete-Group G) - mul-Concrete-Group' : (x y : type-Concrete-Group) → type-Concrete-Group + mul-Concrete-Group : (x y : type-Concrete-Group G) → type-Concrete-Group G + mul-Concrete-Group = mul-∞-Group (∞-group-Concrete-Group G) + + mul-Concrete-Group' : (x y : type-Concrete-Group G) → type-Concrete-Group G mul-Concrete-Group' x y = mul-Concrete-Group y x associative-mul-Concrete-Group : - (x y z : type-Concrete-Group) → + (x y z : type-Concrete-Group G) → ( mul-Concrete-Group (mul-Concrete-Group x y) z) ＝ ( mul-Concrete-Group x (mul-Concrete-Group y z)) associative-mul-Concrete-Group = - associative-mul-∞-Group ∞-group-Concrete-Group + associative-mul-∞-Group (∞-group-Concrete-Group G) left-unit-law-mul-Concrete-Group : - (x : type-Concrete-Group) → mul-Concrete-Group unit-Concrete-Group x ＝ x + (x : type-Concrete-Group G) → mul-Concrete-Group unit-Concrete-Group x ＝ x left-unit-law-mul-Concrete-Group = - left-unit-law-mul-∞-Group ∞-group-Concrete-Group + left-unit-law-mul-∞-Group (∞-group-Concrete-Group G) right-unit-law-mul-Concrete-Group : - (y : type-Concrete-Group) → mul-Concrete-Group y unit-Concrete-Group ＝ y + (y : type-Concrete-Group G) → mul-Concrete-Group y unit-Concrete-Group ＝ y right-unit-law-mul-Concrete-Group = - right-unit-law-mul-∞-Group ∞-group-Concrete-Group + right-unit-law-mul-∞-Group (∞-group-Concrete-Group G) coherence-unit-laws-mul-Concrete-Group : left-unit-law-mul-Concrete-Group unit-Concrete-Group ＝ right-unit-law-mul-Concrete-Group unit-Concrete-Group coherence-unit-laws-mul-Concrete-Group = - coherence-unit-laws-mul-∞-Group ∞-group-Concrete-Group + coherence-unit-laws-mul-∞-Group (∞-group-Concrete-Group G) - inv-Concrete-Group : type-Concrete-Group → type-Concrete-Group - inv-Concrete-Group = inv-∞-Group ∞-group-Concrete-Group + inv-Concrete-Group : type-Concrete-Group G → type-Concrete-Group G + inv-Concrete-Group = inv-∞-Group (∞-group-Concrete-Group G) left-inverse-law-mul-Concrete-Group : - (x : type-Concrete-Group) → + (x : type-Concrete-Group G) → mul-Concrete-Group (inv-Concrete-Group x) x ＝ unit-Concrete-Group left-inverse-law-mul-Concrete-Group = - left-inverse-law-mul-∞-Group ∞-group-Concrete-Group + left-inverse-law-mul-∞-Group (∞-group-Concrete-Group G) right-inverse-law-mul-Concrete-Group : - (x : type-Concrete-Group) → + (x : type-Concrete-Group G) → mul-Concrete-Group x (inv-Concrete-Group x) ＝ unit-Concrete-Group right-inverse-law-mul-Concrete-Group = - right-inverse-law-mul-∞-Group ∞-group-Concrete-Group + right-inverse-law-mul-∞-Group (∞-group-Concrete-Group G) - abstract-group-Concrete-Group : Group l - pr1 (pr1 abstract-group-Concrete-Group) = set-Concrete-Group - pr1 (pr2 (pr1 abstract-group-Concrete-Group)) = mul-Concrete-Group - pr2 (pr2 (pr1 abstract-group-Concrete-Group)) = associative-mul-Concrete-Group - pr1 (pr1 (pr2 abstract-group-Concrete-Group)) = unit-Concrete-Group - pr1 (pr2 (pr1 (pr2 abstract-group-Concrete-Group))) = + semigroup-Concrete-Group : Semigroup l + pr1 semigroup-Concrete-Group = set-Concrete-Group G + pr1 (pr2 semigroup-Concrete-Group) = mul-Concrete-Group + pr2 (pr2 semigroup-Concrete-Group) = associative-mul-Concrete-Group + + is-unital-semigroup-Concrete-Group : + is-unital-Semigroup semigroup-Concrete-Group + pr1 is-unital-semigroup-Concrete-Group = unit-Concrete-Group + pr1 (pr2 is-unital-semigroup-Concrete-Group) = left-unit-law-mul-Concrete-Group - pr2 (pr2 (pr1 (pr2 abstract-group-Concrete-Group))) = + pr2 (pr2 is-unital-semigroup-Concrete-Group) = right-unit-law-mul-Concrete-Group - pr1 (pr2 (pr2 abstract-group-Concrete-Group)) = - inv-Concrete-Group - pr1 (pr2 (pr2 (pr2 abstract-group-Concrete-Group))) = + + is-abstract-group-Concrete-Group' : + is-group' semigroup-Concrete-Group is-unital-semigroup-Concrete-Group + pr1 is-abstract-group-Concrete-Group' = inv-Concrete-Group + pr1 (pr2 is-abstract-group-Concrete-Group') = left-inverse-law-mul-Concrete-Group - pr2 (pr2 (pr2 (pr2 abstract-group-Concrete-Group))) = + pr2 (pr2 is-abstract-group-Concrete-Group') = right-inverse-law-mul-Concrete-Group + is-abstract-group-Concrete-Group : is-group semigroup-Concrete-Group + pr1 is-abstract-group-Concrete-Group = is-unital-semigroup-Concrete-Group + pr2 is-abstract-group-Concrete-Group = is-abstract-group-Concrete-Group' + + abstract-group-Concrete-Group : Group l + pr1 abstract-group-Concrete-Group = semigroup-Concrete-Group + pr2 abstract-group-Concrete-Group = is-abstract-group-Concrete-Group +``` + +### The opposite abstract group associated to a concrete group + +```agda +module _ + {l : Level} (G : Concrete-Group l) + where + + op-semigroup-Concrete-Group : Semigroup l + pr1 op-semigroup-Concrete-Group = set-Concrete-Group G + pr1 (pr2 op-semigroup-Concrete-Group) = mul-Concrete-Group' G + pr2 (pr2 op-semigroup-Concrete-Group) x y z = + inv (associative-mul-Concrete-Group G z y x) + + is-unital-op-semigroup-Concrete-Group : + is-unital-Semigroup op-semigroup-Concrete-Group + pr1 is-unital-op-semigroup-Concrete-Group = unit-Concrete-Group G + pr1 (pr2 is-unital-op-semigroup-Concrete-Group) = + right-unit-law-mul-Concrete-Group G + pr2 (pr2 is-unital-op-semigroup-Concrete-Group) = + left-unit-law-mul-Concrete-Group G + + is-abstract-group-op-Concrete-Group' : + is-group' op-semigroup-Concrete-Group is-unital-op-semigroup-Concrete-Group + pr1 is-abstract-group-op-Concrete-Group' = inv-Concrete-Group G + pr1 (pr2 is-abstract-group-op-Concrete-Group') = + right-inverse-law-mul-Concrete-Group G + pr2 (pr2 is-abstract-group-op-Concrete-Group') = + left-inverse-law-mul-Concrete-Group G + + is-abstract-group-op-Concrete-Group : is-group op-semigroup-Concrete-Group + pr1 is-abstract-group-op-Concrete-Group = + is-unital-op-semigroup-Concrete-Group + pr2 is-abstract-group-op-Concrete-Group = is-abstract-group-op-Concrete-Group' + op-abstract-group-Concrete-Group : Group l - pr1 (pr1 op-abstract-group-Concrete-Group) = set-Concrete-Group - pr1 (pr2 (pr1 op-abstract-group-Concrete-Group)) = mul-Concrete-Group' - pr2 (pr2 (pr1 op-abstract-group-Concrete-Group)) x y z = - inv (associative-mul-Concrete-Group z y x) - pr1 (pr1 (pr2 op-abstract-group-Concrete-Group)) = unit-Concrete-Group - pr1 (pr2 (pr1 (pr2 op-abstract-group-Concrete-Group))) = - right-unit-law-mul-Concrete-Group - pr2 (pr2 (pr1 (pr2 op-abstract-group-Concrete-Group))) = - left-unit-law-mul-Concrete-Group - pr1 (pr2 (pr2 op-abstract-group-Concrete-Group)) = inv-Concrete-Group - pr1 (pr2 (pr2 (pr2 op-abstract-group-Concrete-Group))) = - right-inverse-law-mul-Concrete-Group - pr2 (pr2 (pr2 (pr2 op-abstract-group-Concrete-Group))) = - left-inverse-law-mul-Concrete-Group + pr1 op-abstract-group-Concrete-Group = op-semigroup-Concrete-Group + pr2 op-abstract-group-Concrete-Group = is-abstract-group-op-Concrete-Group ``` diff --git a/src/group-theory/torsors.lagda.md b/src/group-theory/torsors.lagda.md index 0a00390f75..3f356d4a0d 100644 --- a/src/group-theory/torsors.lagda.md +++ b/src/group-theory/torsors.lagda.md @@ -42,12 +42,14 @@ open import higher-group-theory.higher-groups ## Idea -A torsor of `G` is a group action wich merely equivalent to the principal group -action of `G`. +A **torsor** of a [group](group-theory.groups.md) `G` is a +[group action](group-theory.group-actions.md) which is +[merely equivalent](foundation.mere-equivalences.md) to the +[principal group action](group-theory.principal-group-actions.md) of `G`. ## Definitions -### Torsors +### The predicate of being a torsor ```agda module _ @@ -66,7 +68,11 @@ module _ is-prop-is-torsor-Abstract-Group : is-prop is-torsor-Abstract-Group is-prop-is-torsor-Abstract-Group = is-prop-type-Prop is-torsor-Abstract-Group-Prop +``` + +### The type of torsors +```agda module _ {l1 : Level} (G : Group l1) where @@ -76,53 +82,51 @@ module _ Σ ( Abstract-Group-Action G l) ( is-torsor-Abstract-Group G) - action-Torsor-Abstract-Group : - {l : Level} → Torsor-Abstract-Group l → Abstract-Group-Action G l - action-Torsor-Abstract-Group = pr1 +module _ + {l1 l : Level} (G : Group l1) (X : Torsor-Abstract-Group G l) + where + + action-Torsor-Abstract-Group : Abstract-Group-Action G l + action-Torsor-Abstract-Group = pr1 X - set-Torsor-Abstract-Group : - {l : Level} → Torsor-Abstract-Group l → Set l - set-Torsor-Abstract-Group X = - set-Abstract-Group-Action G (action-Torsor-Abstract-Group X) + set-Torsor-Abstract-Group : Set l + set-Torsor-Abstract-Group = + set-Abstract-Group-Action G action-Torsor-Abstract-Group - type-Torsor-Abstract-Group : - {l : Level} → Torsor-Abstract-Group l → UU l - type-Torsor-Abstract-Group X = - type-Set (set-Torsor-Abstract-Group X) + type-Torsor-Abstract-Group : UU l + type-Torsor-Abstract-Group = type-Set set-Torsor-Abstract-Group - is-set-type-Torsor-Abstract-Group : - {l : Level} (X : Torsor-Abstract-Group l) → - is-set (type-Torsor-Abstract-Group X) - is-set-type-Torsor-Abstract-Group X = - is-set-type-Set (set-Torsor-Abstract-Group X) + is-set-type-Torsor-Abstract-Group : is-set type-Torsor-Abstract-Group + is-set-type-Torsor-Abstract-Group = is-set-type-Set set-Torsor-Abstract-Group mul-hom-Torsor-Abstract-Group : - {l : Level} (X : Torsor-Abstract-Group l) → - hom-Group G (symmetric-Group (set-Torsor-Abstract-Group X)) - mul-hom-Torsor-Abstract-Group X = pr2 (action-Torsor-Abstract-Group X) + hom-Group G (symmetric-Group set-Torsor-Abstract-Group) + mul-hom-Torsor-Abstract-Group = pr2 action-Torsor-Abstract-Group equiv-mul-Torsor-Abstract-Group : - {l : Level} (X : Torsor-Abstract-Group l) → type-Group G → - (type-Torsor-Abstract-Group X ≃ type-Torsor-Abstract-Group X) - equiv-mul-Torsor-Abstract-Group X = - equiv-mul-Abstract-Group-Action G (action-Torsor-Abstract-Group X) + type-Group G → + type-Torsor-Abstract-Group ≃ type-Torsor-Abstract-Group + equiv-mul-Torsor-Abstract-Group = + equiv-mul-Abstract-Group-Action G action-Torsor-Abstract-Group mul-Torsor-Abstract-Group : - {l : Level} (X : Torsor-Abstract-Group l) → - type-Group G → type-Torsor-Abstract-Group X → type-Torsor-Abstract-Group X - mul-Torsor-Abstract-Group X = - mul-Abstract-Group-Action G (action-Torsor-Abstract-Group X) + type-Group G → type-Torsor-Abstract-Group → type-Torsor-Abstract-Group + mul-Torsor-Abstract-Group = + mul-Abstract-Group-Action G action-Torsor-Abstract-Group is-torsor-action-Torsor-Abstract-Group : - {l : Level} (X : Torsor-Abstract-Group l) → - is-torsor-Abstract-Group G (action-Torsor-Abstract-Group X) - is-torsor-action-Torsor-Abstract-Group = pr2 + is-torsor-Abstract-Group G action-Torsor-Abstract-Group + is-torsor-action-Torsor-Abstract-Group = pr2 X ``` ### Principal torsor ```agda - principal-Torsor-Abstract-Group : Torsor-Abstract-Group l1 +module _ + {l1 : Level} (G : Group l1) + where + + principal-Torsor-Abstract-Group : Torsor-Abstract-Group G l1 pr1 principal-Torsor-Abstract-Group = principal-Abstract-Group-Action G pr2 principal-Torsor-Abstract-Group = unit-trunc-Prop @@ -190,8 +194,10 @@ module _ ```agda module _ - {l1 l2 l3 : Level} (G : Group l1) (X : Torsor-Abstract-Group G l2) - (Y : Torsor-Abstract-Group G l3) (e : equiv-Torsor-Abstract-Group G X Y) + {l1 l2 l3 : Level} (G : Group l1) + (X : Torsor-Abstract-Group G l2) + (Y : Torsor-Abstract-Group G l3) + (e : equiv-Torsor-Abstract-Group G X Y) where htpy-equiv-Torsor-Abstract-Group : @@ -202,7 +208,8 @@ module _ ( action-Torsor-Abstract-Group G Y) ( e) - refl-htpy-equiv-Torsor-Abstract-Group : htpy-equiv-Torsor-Abstract-Group e + refl-htpy-equiv-Torsor-Abstract-Group : + htpy-equiv-Torsor-Abstract-Group e refl-htpy-equiv-Torsor-Abstract-Group = refl-htpy-equiv-Abstract-Group-Action G ( action-Torsor-Abstract-Group G X) @@ -250,7 +257,8 @@ module _ ```agda module _ - {l1 l2 l3 : Level} (G : Group l1) (X : Torsor-Abstract-Group G l2) + {l1 l2 l3 : Level} (G : Group l1) + (X : Torsor-Abstract-Group G l2) (Y : Torsor-Abstract-Group G l3) where @@ -267,12 +275,14 @@ module _ module _ {l1 l2 l3 l4 : Level} (G : Group l1) - (X : Torsor-Abstract-Group G l2) (Y : Torsor-Abstract-Group G l3) + (X : Torsor-Abstract-Group G l2) + (Y : Torsor-Abstract-Group G l3) (Z : Torsor-Abstract-Group G l4) where comp-equiv-Torsor-Abstract-Group : - equiv-Torsor-Abstract-Group G Y Z → equiv-Torsor-Abstract-Group G X Y → + equiv-Torsor-Abstract-Group G Y Z → + equiv-Torsor-Abstract-Group G X Y → equiv-Torsor-Abstract-Group G X Z comp-equiv-Torsor-Abstract-Group = comp-equiv-Abstract-Group-Action G @@ -281,26 +291,31 @@ module _ ( action-Torsor-Abstract-Group G Z) comp-equiv-Torsor-Abstract-Group' : - equiv-Torsor-Abstract-Group G X Y → equiv-Torsor-Abstract-Group G Y Z → + equiv-Torsor-Abstract-Group G X Y → + equiv-Torsor-Abstract-Group G Y Z → equiv-Torsor-Abstract-Group G X Z comp-equiv-Torsor-Abstract-Group' e f = comp-equiv-Torsor-Abstract-Group f e module _ {l1 l2 l3 : Level} (G : Group l1) - (X : Torsor-Abstract-Group G l2) (Y : Torsor-Abstract-Group G l3) + (X : Torsor-Abstract-Group G l2) + (Y : Torsor-Abstract-Group G l3) where inv-equiv-Torsor-Abstract-Group : - equiv-Torsor-Abstract-Group G X Y → equiv-Torsor-Abstract-Group G Y X + equiv-Torsor-Abstract-Group G X Y → + equiv-Torsor-Abstract-Group G Y X inv-equiv-Torsor-Abstract-Group = inv-equiv-Abstract-Group-Action G ( action-Torsor-Abstract-Group G X) ( action-Torsor-Abstract-Group G Y) module _ - {l1 l2 l3 l4 l5 : Level} (G : Group l1) (X1 : Torsor-Abstract-Group G l2) - (X2 : Torsor-Abstract-Group G l3) (X3 : Torsor-Abstract-Group G l4) + {l1 l2 l3 l4 l5 : Level} (G : Group l1) + (X1 : Torsor-Abstract-Group G l2) + (X2 : Torsor-Abstract-Group G l3) + (X3 : Torsor-Abstract-Group G l4) (X4 : Torsor-Abstract-Group G l5) where @@ -324,7 +339,8 @@ module _ ( refl-htpy) module _ - {l1 l2 l3 : Level} (G : Group l1) (X : Torsor-Abstract-Group G l2) + {l1 l2 l3 : Level} (G : Group l1) + (X : Torsor-Abstract-Group G l2) (Y : Torsor-Abstract-Group G l3) where @@ -509,7 +525,7 @@ module _ (X : Torsor-Abstract-Group G l1) → equiv-Torsor-Abstract-Group G (principal-Torsor-Abstract-Group G) X → Eq-Torsor-Abstract-Group X - Eq-equiv-Torsor-Abstract-Group X (pair e H) = map-equiv e (unit-Group G) + Eq-equiv-Torsor-Abstract-Group X (e , H) = map-equiv e (unit-Group G) preserves-mul-Eq-equiv-Torsor-Abstract-Group : (e f : @@ -532,7 +548,7 @@ module _ ( Eq-equiv-Torsor-Abstract-Group ( principal-Torsor-Abstract-Group G) ( f))) - preserves-mul-Eq-equiv-Torsor-Abstract-Group (pair e H) (pair f K) = + preserves-mul-Eq-equiv-Torsor-Abstract-Group (e , H) (f , K) = ( ap ( map-equiv f) ( inv (right-unit-law-mul-Group G (map-equiv e (unit-Group G))))) ∙ @@ -591,8 +607,7 @@ module _ (X : Torsor-Abstract-Group G l1) → Id (principal-Torsor-Abstract-Group G) X ≃ Eq-Torsor-Abstract-Group X equiv-Eq-equiv-Torsor-Abstract-Group X = - ( pair - ( Eq-equiv-Torsor-Abstract-Group X) + ( ( Eq-equiv-Torsor-Abstract-Group X) , ( is-equiv-Eq-equiv-Torsor-Abstract-Group X)) ∘e ( extensionality-Torsor-Abstract-Group G ( principal-Torsor-Abstract-Group G) @@ -637,7 +652,7 @@ module _ ( q))) ``` -### From torsors to concrete group +### From torsors to concrete groups ```agda ∞-group-Group : ∞-Group (lsuc l1) @@ -670,12 +685,12 @@ module _ iso-equiv-Group ( abstract-group-Concrete-Group concrete-group-Group) ( G) - ( pair - ( equiv-Eq-equiv-Torsor-Abstract-Group - ( principal-Torsor-Abstract-Group G)) + ( ( equiv-Eq-equiv-Torsor-Abstract-Group + ( principal-Torsor-Abstract-Group G)) , ( preserves-mul-equiv-Eq-equiv-Torsor-Abstract-Group)) +``` -{- +```text module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) where @@ -685,5 +700,4 @@ module _ pr1 (pr1 (map-Torsor-Abstract-Group f X)) = {!!} pr2 (pr1 (map-Torsor-Abstract-Group f X)) = {!!} pr2 (map-Torsor-Abstract-Group f X) = {!!} --} ``` From a0a12749d42fcc613d21950d7970b79fad412662 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 1 Nov 2023 22:19:26 +0100 Subject: [PATCH 2/5] some more links --- src/group-theory/concrete-groups.lagda.md | 2 +- src/group-theory/principal-group-actions.lagda.md | 4 ++-- src/group-theory/principal-torsors-concrete-groups.lagda.md | 3 ++- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/group-theory/concrete-groups.lagda.md b/src/group-theory/concrete-groups.lagda.md index 72e6aeb5c5..b3b4c34c49 100644 --- a/src/group-theory/concrete-groups.lagda.md +++ b/src/group-theory/concrete-groups.lagda.md @@ -20,8 +20,8 @@ open import foundation.truncation-levels open import foundation.universe-levels open import group-theory.groups -open import group-theory.semigroups open import group-theory.monoids +open import group-theory.semigroups open import higher-group-theory.higher-groups diff --git a/src/group-theory/principal-group-actions.lagda.md b/src/group-theory/principal-group-actions.lagda.md index 6d2056791a..a2f2968408 100644 --- a/src/group-theory/principal-group-actions.lagda.md +++ b/src/group-theory/principal-group-actions.lagda.md @@ -19,8 +19,8 @@ open import group-theory.groups ## Idea -The principal group action is the action of a group on itself by multiplication -from the left +The **principal group action** is the [action](group-theory.group-actions.md) of +a [group](group-theory.groups.md) on itself by multiplication from the left ## Definition diff --git a/src/group-theory/principal-torsors-concrete-groups.lagda.md b/src/group-theory/principal-torsors-concrete-groups.lagda.md index 3b25ba5e8b..d90716ffd3 100644 --- a/src/group-theory/principal-torsors-concrete-groups.lagda.md +++ b/src/group-theory/principal-torsors-concrete-groups.lagda.md @@ -17,7 +17,8 @@ open import group-theory.concrete-groups ## Idea -The principal torsor of a concrete group `G` is the identity type of `BG`. +The **principal torsor** of a [concrete group](group-theory.concrete-groups.md) +`G` is the [identity type](foundation-core.identity-types.md) of `BG`. ## Definition From 7f41f279ac281e42a9e413a9fa8ddf0770d87f5c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 1 Nov 2023 22:22:52 +0100 Subject: [PATCH 3/5] fix a typo fix --- src/group-theory/torsors.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/group-theory/torsors.lagda.md b/src/group-theory/torsors.lagda.md index 27f2e72bfe..e7cd83e775 100644 --- a/src/group-theory/torsors.lagda.md +++ b/src/group-theory/torsors.lagda.md @@ -651,7 +651,7 @@ module _ ( q))) ``` -### From torsors to concrete groups +### From torsors to concrete group ```agda ∞-group-Group : ∞-Group (lsuc l1) From 25836719d0a1b486cf58578fceaf858729f8faf5 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 3 Nov 2023 23:49:25 +0100 Subject: [PATCH 4/5] opposite semigroups --- src/group-theory.lagda.md | 1 + src/group-theory/concrete-groups.lagda.md | 57 +++++++------------ src/group-theory/opposite-groups.lagda.md | 36 ++++++++---- src/group-theory/opposite-semigroups.lagda.md | 52 +++++++++++++++++ 4 files changed, 98 insertions(+), 48 deletions(-) create mode 100644 src/group-theory/opposite-semigroups.lagda.md diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index fb5f2a7565..5db11c554a 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -125,6 +125,7 @@ open import group-theory.normal-submonoids-commutative-monoids public open import group-theory.normalizer-subgroups public open import group-theory.nullifying-group-homomorphisms public open import group-theory.opposite-groups public +open import group-theory.opposite-semigroups public open import group-theory.orbit-stabilizer-theorem-concrete-groups public open import group-theory.orbits-concrete-group-actions public open import group-theory.orbits-group-actions public diff --git a/src/group-theory/concrete-groups.lagda.md b/src/group-theory/concrete-groups.lagda.md index b3b4c34c49..01941b4f68 100644 --- a/src/group-theory/concrete-groups.lagda.md +++ b/src/group-theory/concrete-groups.lagda.md @@ -21,6 +21,8 @@ open import foundation.universe-levels open import group-theory.groups open import group-theory.monoids +open import group-theory.opposite-groups +open import group-theory.opposite-semigroups open import group-theory.semigroups open import higher-group-theory.higher-groups @@ -181,21 +183,21 @@ module _ pr2 (pr2 is-unital-semigroup-Concrete-Group) = right-unit-law-mul-Concrete-Group - is-abstract-group-Concrete-Group' : + is-group-Concrete-Group' : is-group' semigroup-Concrete-Group is-unital-semigroup-Concrete-Group - pr1 is-abstract-group-Concrete-Group' = inv-Concrete-Group - pr1 (pr2 is-abstract-group-Concrete-Group') = + pr1 is-group-Concrete-Group' = inv-Concrete-Group + pr1 (pr2 is-group-Concrete-Group') = left-inverse-law-mul-Concrete-Group - pr2 (pr2 is-abstract-group-Concrete-Group') = + pr2 (pr2 is-group-Concrete-Group') = right-inverse-law-mul-Concrete-Group - is-abstract-group-Concrete-Group : is-group semigroup-Concrete-Group - pr1 is-abstract-group-Concrete-Group = is-unital-semigroup-Concrete-Group - pr2 is-abstract-group-Concrete-Group = is-abstract-group-Concrete-Group' + is-group-Concrete-Group : is-group semigroup-Concrete-Group + pr1 is-group-Concrete-Group = is-unital-semigroup-Concrete-Group + pr2 is-group-Concrete-Group = is-group-Concrete-Group' - abstract-group-Concrete-Group : Group l - pr1 abstract-group-Concrete-Group = semigroup-Concrete-Group - pr2 abstract-group-Concrete-Group = is-abstract-group-Concrete-Group + group-Concrete-Group : Group l + pr1 group-Concrete-Group = semigroup-Concrete-Group + pr2 group-Concrete-Group = is-group-Concrete-Group ``` ### The opposite abstract group associated to a concrete group @@ -206,33 +208,16 @@ module _ where op-semigroup-Concrete-Group : Semigroup l - pr1 op-semigroup-Concrete-Group = set-Concrete-Group G - pr1 (pr2 op-semigroup-Concrete-Group) = mul-Concrete-Group' G - pr2 (pr2 op-semigroup-Concrete-Group) x y z = - inv (associative-mul-Concrete-Group G z y x) + op-semigroup-Concrete-Group = op-Semigroup (semigroup-Concrete-Group G) is-unital-op-semigroup-Concrete-Group : is-unital-Semigroup op-semigroup-Concrete-Group - pr1 is-unital-op-semigroup-Concrete-Group = unit-Concrete-Group G - pr1 (pr2 is-unital-op-semigroup-Concrete-Group) = - right-unit-law-mul-Concrete-Group G - pr2 (pr2 is-unital-op-semigroup-Concrete-Group) = - left-unit-law-mul-Concrete-Group G - - is-abstract-group-op-Concrete-Group' : - is-group' op-semigroup-Concrete-Group is-unital-op-semigroup-Concrete-Group - pr1 is-abstract-group-op-Concrete-Group' = inv-Concrete-Group G - pr1 (pr2 is-abstract-group-op-Concrete-Group') = - right-inverse-law-mul-Concrete-Group G - pr2 (pr2 is-abstract-group-op-Concrete-Group') = - left-inverse-law-mul-Concrete-Group G - - is-abstract-group-op-Concrete-Group : is-group op-semigroup-Concrete-Group - pr1 is-abstract-group-op-Concrete-Group = - is-unital-op-semigroup-Concrete-Group - pr2 is-abstract-group-op-Concrete-Group = is-abstract-group-op-Concrete-Group' - - op-abstract-group-Concrete-Group : Group l - pr1 op-abstract-group-Concrete-Group = op-semigroup-Concrete-Group - pr2 op-abstract-group-Concrete-Group = is-abstract-group-op-Concrete-Group + is-unital-op-semigroup-Concrete-Group = + is-unital-op-Group (group-Concrete-Group G) + + is-group-op-Concrete-Group : is-group op-semigroup-Concrete-Group + is-group-op-Concrete-Group = is-group-op-Group (group-Concrete-Group G) + + op-group-Concrete-Group : Group l + op-group-Concrete-Group = op-Group (group-Concrete-Group G) ``` diff --git a/src/group-theory/opposite-groups.lagda.md b/src/group-theory/opposite-groups.lagda.md index 0acbf3b60b..f8ffda68ec 100644 --- a/src/group-theory/opposite-groups.lagda.md +++ b/src/group-theory/opposite-groups.lagda.md @@ -13,28 +13,40 @@ open import foundation.universe-levels open import group-theory.groups open import group-theory.isomorphisms-groups +open import group-theory.monoids +open import group-theory.opposite-semigroups +open import group-theory.semigroups ``` ## Idea -The opposite of a group `G` with multiplication `μ` is a group with the same -underlying set as `G` and multiplication given by `x y ↦ μ y x`. +The **opposite of a [group](group-theory.groups.md)** `G` with multiplication +`μ` is a group with the same underlying [set](foundation-core.sets.md) as `G` +and multiplication given by `x y ↦ μ y x`. ## Definition ```agda -op-Group : {l : Level} → Group l → Group l -pr1 (pr1 (op-Group G)) = set-Group G -pr1 (pr2 (pr1 (op-Group G))) x y = mul-Group G y x -pr2 (pr2 (pr1 (op-Group G))) x y z = inv (associative-mul-Group G z y x) -pr1 (pr1 (pr2 (op-Group G))) = unit-Group G -pr1 (pr2 (pr1 (pr2 (op-Group G)))) = right-unit-law-mul-Group G -pr2 (pr2 (pr1 (pr2 (op-Group G)))) = left-unit-law-mul-Group G -pr1 (pr2 (pr2 (op-Group G))) = inv-Group G -pr1 (pr2 (pr2 (pr2 (op-Group G)))) = right-inverse-law-mul-Group G -pr2 (pr2 (pr2 (pr2 (op-Group G)))) = left-inverse-law-mul-Group G +module _ + {l : Level} (G : Group l) + where + + is-unital-op-Group : is-unital-Semigroup (op-Semigroup (semigroup-Group G)) + pr1 is-unital-op-Group = unit-Group G + pr1 (pr2 is-unital-op-Group) = right-unit-law-mul-Group G + pr2 (pr2 is-unital-op-Group) = left-unit-law-mul-Group G + + is-group-op-Group : is-group (op-Semigroup (semigroup-Group G)) + pr1 is-group-op-Group = is-unital-op-Group + pr1 (pr2 is-group-op-Group) = inv-Group G + pr1 (pr2 (pr2 is-group-op-Group)) = right-inverse-law-mul-Group G + pr2 (pr2 (pr2 is-group-op-Group)) = left-inverse-law-mul-Group G + + op-Group : Group l + pr1 op-Group = op-Semigroup (semigroup-Group G) + pr2 op-Group = is-group-op-Group ``` ## Properties diff --git a/src/group-theory/opposite-semigroups.lagda.md b/src/group-theory/opposite-semigroups.lagda.md new file mode 100644 index 0000000000..860ad6a7de --- /dev/null +++ b/src/group-theory/opposite-semigroups.lagda.md @@ -0,0 +1,52 @@ +# The opposite of a semigroup + +```agda +module group-theory.opposite-semigroups where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.sets +open import foundation.universe-levels + +open import group-theory.semigroups +``` + +
+ +## Idea + +The **opposite of a [semigroup](group-theory.semigroups.md)** `G` with +multiplication `μ` is a semigroup with the same underlying +[set](foundation-core.sets.md) as `G` and multiplication given by `x y ↦ μ y x`. + +## Definition + +```agda +module _ + {l : Level} (G : Semigroup l) + where + + set-op-Semigroup : Set l + set-op-Semigroup = set-Semigroup G + + type-op-Semigroup : UU l + type-op-Semigroup = type-Set set-op-Semigroup + + mul-op-Semigroup : type-op-Semigroup → type-op-Semigroup → type-op-Semigroup + mul-op-Semigroup x y = mul-Semigroup G y x + + associative-mul-op-Semigroup : + (x y z : type-op-Semigroup) → + mul-Semigroup G z (mul-Semigroup G y x) ＝ + mul-Semigroup G (mul-Semigroup G z y) x + associative-mul-op-Semigroup x y z = inv (associative-mul-Semigroup G z y x) + + op-Semigroup : Semigroup l + pr1 op-Semigroup = set-op-Semigroup + pr1 (pr2 op-Semigroup) = mul-op-Semigroup + pr2 (pr2 op-Semigroup) = associative-mul-op-Semigroup +``` From efb3f54f647d3de999a7d05c4f47453c5f23e5c7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 3 Nov 2023 23:51:30 +0100 Subject: [PATCH 5/5] `abstract-group` -> `group` --- ...rtier-delooping-sign-homomorphism.lagda.md | 12 +-- .../delooping-sign-homomorphism.lagda.md | 96 +++++++++---------- .../finite-type-groups.lagda.md | 18 ++-- ...mpson-delooping-sign-homomorphism.lagda.md | 12 +-- ...artesian-products-concrete-groups.lagda.md | 40 ++++---- .../conjugation-concrete-groups.lagda.md | 2 +- .../homomorphisms-concrete-groups.lagda.md | 4 +- ...artesian-products-concrete-groups.lagda.md | 40 ++++---- src/group-theory/loop-groups-sets.lagda.md | 18 ++-- src/group-theory/symmetric-groups.lagda.md | 16 ++-- src/group-theory/torsors.lagda.md | 8 +- 11 files changed, 133 insertions(+), 133 deletions(-) diff --git a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md index 7a1ba6b3a1..b8d79226ec 100644 --- a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md @@ -146,28 +146,28 @@ module _ ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2)) ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2)) + ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l (n +ℕ 2)) ( UU-Fin-Group (lsuc l) 2) ( cartier-delooping-sign (n +ℕ 2))) ( hom-inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l (n +ℕ 2)))) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2)) ( symmetric-abstract-UU-fin-group-quotient-hom ( orientation-Complete-Undirected-Graph) ( even-difference-orientation-Complete-Undirected-Graph) diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md index b9f0763a29..5dc0be6bfb 100644 --- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md @@ -1085,16 +1085,16 @@ module _ ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set @@ -1104,17 +1104,17 @@ module _ ( quotient-delooping-sign-loop n)) ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l1 (n +ℕ 2)) ( UU-Fin-Group l4 2) ( quotient-delooping-sign (n +ℕ 2))) ( hom-iso-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2))))) eq-quotient-delooping-loop-UU-Fin-Group n = @@ -1298,21 +1298,21 @@ module _ ( eq-is-prop ( is-prop-preserves-mul-Semigroup ( semigroup-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) - ( semigroup-Group (abstract-group-Concrete-Group (UU-Fin-Group l4 2))) + ( semigroup-Group (group-Concrete-Group (UU-Fin-Group l4 2))) ( pr1 ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l1 (n +ℕ 2)) ( UU-Fin-Group l4 2) ( quotient-delooping-sign (n +ℕ 2))) ( hom-iso-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2)))))))) @@ -1320,25 +1320,25 @@ module _ (n : ℕ) → hom-Group ( symmetric-Group (Fin-Set 2)) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) symmetric-abstract-UU-fin-group-quotient-hom n = comp-hom-Group ( symmetric-Group (Fin-Set 2)) ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set @@ -1357,28 +1357,28 @@ module _ ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l1 (n +ℕ 2)) ( UU-Fin-Group l4 2) ( quotient-delooping-sign (n +ℕ 2))) ( hom-inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2)))) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( symmetric-abstract-UU-fin-group-quotient-hom n) ( sign-homomorphism ( n +ℕ 2) @@ -1393,7 +1393,7 @@ module _ comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( f) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) ( inv (eq-quotient-delooping-loop-UU-Fin-Group n))) ∙ @@ -1401,16 +1401,16 @@ module _ ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set @@ -1423,16 +1423,16 @@ module _ ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) ( iso-loop-group-equiv-Set @@ -1446,33 +1446,33 @@ module _ ( is-prop-preserves-mul-Semigroup ( semigroup-Group (symmetric-Group (raise-Fin-Set l1 (n +ℕ 2)))) ( semigroup-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2))) + ( group-Concrete-Group (UU-Fin-Group l4 2))) ( pr1 ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set 2)) ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-hom-Group ( symmetric-Group (quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( hom-iso-Group ( loop-group-Set (quotient-set-Fin (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( comp-iso-Group ( loop-group-Set ( quotient-set-Fin (n +ℕ 2))) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l4 2)) + ( group-Concrete-Group (UU-Fin-Group l4 2)) ( inv-iso-Group - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( UU-Fin-Group l4 2)) ( loop-group-Set (raise-Set l4 (Fin-Set 2))) ( iso-loop-group-fin-UU-Fin-Group l4 2)) @@ -1580,28 +1580,28 @@ module _ ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l1 (n +ℕ 2)) ( UU-Fin-Group (lsuc l2) 2) ( delooping-sign (n +ℕ 2))) ( hom-inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l1 (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l1 (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l1 (n +ℕ 2)))) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l1 (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc l2) 2)) ( symmetric-abstract-UU-fin-group-quotient-hom ( λ n X → type-UU-Fin 2 (Q n X)) ( λ n X → Id-Equivalence-Relation (set-UU-Fin 2 (Q n X))) diff --git a/src/finite-group-theory/finite-type-groups.lagda.md b/src/finite-group-theory/finite-type-groups.lagda.md index 8c02609a86..4b9ff73954 100644 --- a/src/finite-group-theory/finite-type-groups.lagda.md +++ b/src/finite-group-theory/finite-type-groups.lagda.md @@ -56,7 +56,7 @@ module _ hom-loop-group-fin-UU-Fin-Group : hom-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l n)) + ( group-Concrete-Group (UU-Fin-Group l n)) ( loop-group-Set (raise-Set l (Fin-Set n))) pr1 hom-loop-group-fin-UU-Fin-Group p = pr1 (pair-eq-Σ p) pr2 hom-loop-group-fin-UU-Fin-Group p q = @@ -65,7 +65,7 @@ module _ hom-inv-loop-group-fin-UU-Fin-Group : hom-Group ( loop-group-Set (raise-Set l (Fin-Set n))) - ( abstract-group-Concrete-Group (UU-Fin-Group l n)) + ( group-Concrete-Group (UU-Fin-Group l n)) pr1 hom-inv-loop-group-fin-UU-Fin-Group p = eq-pair-Σ p (eq-is-prop is-prop-type-trunc-Prop) pr2 hom-inv-loop-group-fin-UU-Fin-Group p q = @@ -82,7 +82,7 @@ module _ Id ( comp-hom-Group ( loop-group-Set (raise-Set l (Fin-Set n))) - ( abstract-group-Concrete-Group (UU-Fin-Group l n)) + ( group-Concrete-Group (UU-Fin-Group l n)) ( loop-group-Set (raise-Set l (Fin-Set n))) ( hom-loop-group-fin-UU-Fin-Group) ( hom-inv-loop-group-fin-UU-Fin-Group)) @@ -105,12 +105,12 @@ module _ is-retraction-hom-inv-loop-group-fin-UU-Fin-Group : Id ( comp-hom-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l n)) + ( group-Concrete-Group (UU-Fin-Group l n)) ( loop-group-Set (raise-Set l (Fin-Set n))) - ( abstract-group-Concrete-Group (UU-Fin-Group l n)) + ( group-Concrete-Group (UU-Fin-Group l n)) ( hom-inv-loop-group-fin-UU-Fin-Group) ( hom-loop-group-fin-UU-Fin-Group)) - ( id-hom-Group (abstract-group-Concrete-Group (UU-Fin-Group l n))) + ( id-hom-Group (group-Concrete-Group (UU-Fin-Group l n))) is-retraction-hom-inv-loop-group-fin-UU-Fin-Group = eq-pair-Σ ( eq-htpy @@ -121,13 +121,13 @@ module _ ( is-section-pair-eq-Σ (Fin-UU-Fin l n) (Fin-UU-Fin l n) p))) ( eq-is-prop ( is-prop-preserves-mul-Semigroup - ( semigroup-Group (abstract-group-Concrete-Group (UU-Fin-Group l n))) - ( semigroup-Group (abstract-group-Concrete-Group (UU-Fin-Group l n))) + ( semigroup-Group (group-Concrete-Group (UU-Fin-Group l n))) + ( semigroup-Group (group-Concrete-Group (UU-Fin-Group l n))) ( id))) iso-loop-group-fin-UU-Fin-Group : iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l n)) + ( group-Concrete-Group (UU-Fin-Group l n)) ( loop-group-Set (raise-Set l (Fin-Set n))) pr1 iso-loop-group-fin-UU-Fin-Group = hom-loop-group-fin-UU-Fin-Group diff --git a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md index 7a90598c0b..2bbed154ea 100644 --- a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md @@ -751,28 +751,28 @@ module _ ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc lzero ⊔ l) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc lzero ⊔ l) 2)) ( comp-hom-Group ( loop-group-Set (raise-Fin-Set l (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group l (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc lzero ⊔ l) 2)) + ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group (lsuc lzero ⊔ l) 2)) ( hom-group-hom-Concrete-Group ( UU-Fin-Group l (n +ℕ 2)) ( UU-Fin-Group (lsuc lzero ⊔ l) 2) ( simpson-delooping-sign (n +ℕ 2))) ( hom-inv-iso-Group - ( abstract-group-Concrete-Group (UU-Fin-Group l (n +ℕ 2))) + ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2))) ( loop-group-Set (raise-Fin-Set l (n +ℕ 2))) ( iso-loop-group-fin-UU-Fin-Group l (n +ℕ 2)))) ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l (n +ℕ 2)))) ( comp-hom-Group ( symmetric-Group (raise-Fin-Set l (n +ℕ 2))) ( symmetric-Group (Fin-Set (n +ℕ 2))) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc lzero ⊔ l) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc lzero ⊔ l) 2)) ( comp-hom-Group ( symmetric-Group (Fin-Set (n +ℕ 2))) ( symmetric-Group (Fin-Set 2)) - ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc lzero ⊔ l) 2)) + ( group-Concrete-Group (UU-Fin-Group (lsuc lzero ⊔ l) 2)) ( symmetric-abstract-UU-fin-group-quotient-hom ( λ n X → Fin n ≃ type-UU-Fin n X) ( sign-comp-Equivalence-Relation) diff --git a/src/group-theory/cartesian-products-concrete-groups.lagda.md b/src/group-theory/cartesian-products-concrete-groups.lagda.md index 5c6deb5bd2..ab365f3c0c 100644 --- a/src/group-theory/cartesian-products-concrete-groups.lagda.md +++ b/src/group-theory/cartesian-products-concrete-groups.lagda.md @@ -188,44 +188,44 @@ module _ right-inverse-law-mul-product-Concrete-Group = right-inverse-law-mul-∞-Group ∞-group-product-Concrete-Group - abstract-group-product-Concrete-Group : Group (l1 ⊔ l2) - pr1 (pr1 abstract-group-product-Concrete-Group) = + group-product-Concrete-Group : Group (l1 ⊔ l2) + pr1 (pr1 group-product-Concrete-Group) = set-product-Concrete-Group - pr1 (pr2 (pr1 abstract-group-product-Concrete-Group)) = + pr1 (pr2 (pr1 group-product-Concrete-Group)) = mul-product-Concrete-Group - pr2 (pr2 (pr1 abstract-group-product-Concrete-Group)) = + pr2 (pr2 (pr1 group-product-Concrete-Group)) = associative-mul-product-Concrete-Group - pr1 (pr1 (pr2 abstract-group-product-Concrete-Group)) = + pr1 (pr1 (pr2 group-product-Concrete-Group)) = unit-product-Concrete-Group - pr1 (pr2 (pr1 (pr2 abstract-group-product-Concrete-Group))) = + pr1 (pr2 (pr1 (pr2 group-product-Concrete-Group))) = left-unit-law-mul-product-Concrete-Group - pr2 (pr2 (pr1 (pr2 abstract-group-product-Concrete-Group))) = + pr2 (pr2 (pr1 (pr2 group-product-Concrete-Group))) = right-unit-law-mul-product-Concrete-Group - pr1 (pr2 (pr2 abstract-group-product-Concrete-Group)) = + pr1 (pr2 (pr2 group-product-Concrete-Group)) = inv-product-Concrete-Group - pr1 (pr2 (pr2 (pr2 abstract-group-product-Concrete-Group))) = + pr1 (pr2 (pr2 (pr2 group-product-Concrete-Group))) = left-inverse-law-mul-product-Concrete-Group - pr2 (pr2 (pr2 (pr2 abstract-group-product-Concrete-Group))) = + pr2 (pr2 (pr2 (pr2 group-product-Concrete-Group))) = right-inverse-law-mul-product-Concrete-Group - op-abstract-group-product-Concrete-Group : Group (l1 ⊔ l2) - pr1 (pr1 op-abstract-group-product-Concrete-Group) = + op-group-product-Concrete-Group : Group (l1 ⊔ l2) + pr1 (pr1 op-group-product-Concrete-Group) = set-product-Concrete-Group - pr1 (pr2 (pr1 op-abstract-group-product-Concrete-Group)) = + pr1 (pr2 (pr1 op-group-product-Concrete-Group)) = mul-product-Concrete-Group' - pr2 (pr2 (pr1 op-abstract-group-product-Concrete-Group)) x y z = + pr2 (pr2 (pr1 op-group-product-Concrete-Group)) x y z = inv (associative-mul-product-Concrete-Group z y x) - pr1 (pr1 (pr2 op-abstract-group-product-Concrete-Group)) = + pr1 (pr1 (pr2 op-group-product-Concrete-Group)) = unit-product-Concrete-Group - pr1 (pr2 (pr1 (pr2 op-abstract-group-product-Concrete-Group))) = + pr1 (pr2 (pr1 (pr2 op-group-product-Concrete-Group))) = right-unit-law-mul-product-Concrete-Group - pr2 (pr2 (pr1 (pr2 op-abstract-group-product-Concrete-Group))) = + pr2 (pr2 (pr1 (pr2 op-group-product-Concrete-Group))) = left-unit-law-mul-product-Concrete-Group - pr1 (pr2 (pr2 op-abstract-group-product-Concrete-Group)) = + pr1 (pr2 (pr2 op-group-product-Concrete-Group)) = inv-product-Concrete-Group - pr1 (pr2 (pr2 (pr2 op-abstract-group-product-Concrete-Group))) = + pr1 (pr2 (pr2 (pr2 op-group-product-Concrete-Group))) = right-inverse-law-mul-product-Concrete-Group - pr2 (pr2 (pr2 (pr2 op-abstract-group-product-Concrete-Group))) = + pr2 (pr2 (pr2 (pr2 op-group-product-Concrete-Group))) = left-inverse-law-mul-product-Concrete-Group ``` diff --git a/src/group-theory/conjugation-concrete-groups.lagda.md b/src/group-theory/conjugation-concrete-groups.lagda.md index 2c18d88dcd..4b3aa4c395 100644 --- a/src/group-theory/conjugation-concrete-groups.lagda.md +++ b/src/group-theory/conjugation-concrete-groups.lagda.md @@ -62,7 +62,7 @@ module _ map-hom-Concrete-Group G G conjugation-Concrete-Group compute-map-conjugation-Concrete-Group : - conjugation-Group' (abstract-group-Concrete-Group G) g ~ + conjugation-Group' (group-Concrete-Group G) g ~ map-conjugation-Concrete-Group compute-map-conjugation-Concrete-Group x = ( assoc (inv g) x g) ∙ diff --git a/src/group-theory/homomorphisms-concrete-groups.lagda.md b/src/group-theory/homomorphisms-concrete-groups.lagda.md index 1aadaafc67..3bc213099f 100644 --- a/src/group-theory/homomorphisms-concrete-groups.lagda.md +++ b/src/group-theory/homomorphisms-concrete-groups.lagda.md @@ -105,8 +105,8 @@ module _ hom-group-hom-Concrete-Group : hom-Concrete-Group → hom-Group - ( abstract-group-Concrete-Group G) - ( abstract-group-Concrete-Group H) + ( group-Concrete-Group G) + ( group-Concrete-Group H) hom-group-hom-Concrete-Group f = pair (map-hom-Concrete-Group f) (preserves-mul-map-hom-Concrete-Group f) ``` diff --git a/src/group-theory/iterated-cartesian-products-concrete-groups.lagda.md b/src/group-theory/iterated-cartesian-products-concrete-groups.lagda.md index 444472481c..48c6d10c6e 100644 --- a/src/group-theory/iterated-cartesian-products-concrete-groups.lagda.md +++ b/src/group-theory/iterated-cartesian-products-concrete-groups.lagda.md @@ -224,44 +224,44 @@ module _ right-inverse-law-mul-iterated-product-Concrete-Group = right-inverse-law-mul-∞-Group ∞-group-iterated-product-Concrete-Group - abstract-group-iterated-product-Concrete-Group : Group l - pr1 (pr1 abstract-group-iterated-product-Concrete-Group) = + group-iterated-product-Concrete-Group : Group l + pr1 (pr1 group-iterated-product-Concrete-Group) = set-iterated-product-Concrete-Group - pr1 (pr2 (pr1 abstract-group-iterated-product-Concrete-Group)) = + pr1 (pr2 (pr1 group-iterated-product-Concrete-Group)) = mul-iterated-product-Concrete-Group - pr2 (pr2 (pr1 abstract-group-iterated-product-Concrete-Group)) = + pr2 (pr2 (pr1 group-iterated-product-Concrete-Group)) = associative-mul-iterated-product-Concrete-Group - pr1 (pr1 (pr2 abstract-group-iterated-product-Concrete-Group)) = + pr1 (pr1 (pr2 group-iterated-product-Concrete-Group)) = unit-iterated-product-Concrete-Group - pr1 (pr2 (pr1 (pr2 abstract-group-iterated-product-Concrete-Group))) = + pr1 (pr2 (pr1 (pr2 group-iterated-product-Concrete-Group))) = left-unit-law-mul-iterated-product-Concrete-Group - pr2 (pr2 (pr1 (pr2 abstract-group-iterated-product-Concrete-Group))) = + pr2 (pr2 (pr1 (pr2 group-iterated-product-Concrete-Group))) = right-unit-law-mul-iterated-product-Concrete-Group - pr1 (pr2 (pr2 abstract-group-iterated-product-Concrete-Group)) = + pr1 (pr2 (pr2 group-iterated-product-Concrete-Group)) = inv-iterated-product-Concrete-Group - pr1 (pr2 (pr2 (pr2 abstract-group-iterated-product-Concrete-Group))) = + pr1 (pr2 (pr2 (pr2 group-iterated-product-Concrete-Group))) = left-inverse-law-mul-iterated-product-Concrete-Group - pr2 (pr2 (pr2 (pr2 abstract-group-iterated-product-Concrete-Group))) = + pr2 (pr2 (pr2 (pr2 group-iterated-product-Concrete-Group))) = right-inverse-law-mul-iterated-product-Concrete-Group - op-abstract-group-iterated-product-Concrete-Group : Group l - pr1 (pr1 op-abstract-group-iterated-product-Concrete-Group) = + op-group-iterated-product-Concrete-Group : Group l + pr1 (pr1 op-group-iterated-product-Concrete-Group) = set-iterated-product-Concrete-Group - pr1 (pr2 (pr1 op-abstract-group-iterated-product-Concrete-Group)) = + pr1 (pr2 (pr1 op-group-iterated-product-Concrete-Group)) = mul-iterated-product-Concrete-Group' - pr2 (pr2 (pr1 op-abstract-group-iterated-product-Concrete-Group)) x y z = + pr2 (pr2 (pr1 op-group-iterated-product-Concrete-Group)) x y z = inv (associative-mul-iterated-product-Concrete-Group z y x) - pr1 (pr1 (pr2 op-abstract-group-iterated-product-Concrete-Group)) = + pr1 (pr1 (pr2 op-group-iterated-product-Concrete-Group)) = unit-iterated-product-Concrete-Group - pr1 (pr2 (pr1 (pr2 op-abstract-group-iterated-product-Concrete-Group))) = + pr1 (pr2 (pr1 (pr2 op-group-iterated-product-Concrete-Group))) = right-unit-law-mul-iterated-product-Concrete-Group - pr2 (pr2 (pr1 (pr2 op-abstract-group-iterated-product-Concrete-Group))) = + pr2 (pr2 (pr1 (pr2 op-group-iterated-product-Concrete-Group))) = left-unit-law-mul-iterated-product-Concrete-Group - pr1 (pr2 (pr2 op-abstract-group-iterated-product-Concrete-Group)) = + pr1 (pr2 (pr2 op-group-iterated-product-Concrete-Group)) = inv-iterated-product-Concrete-Group - pr1 (pr2 (pr2 (pr2 op-abstract-group-iterated-product-Concrete-Group))) = + pr1 (pr2 (pr2 (pr2 op-group-iterated-product-Concrete-Group))) = right-inverse-law-mul-iterated-product-Concrete-Group - pr2 (pr2 (pr2 (pr2 op-abstract-group-iterated-product-Concrete-Group))) = + pr2 (pr2 (pr2 (pr2 op-group-iterated-product-Concrete-Group))) = left-inverse-law-mul-iterated-product-Concrete-Group ``` diff --git a/src/group-theory/loop-groups-sets.lagda.md b/src/group-theory/loop-groups-sets.lagda.md index 9273085a5e..6df02c2c82 100644 --- a/src/group-theory/loop-groups-sets.lagda.md +++ b/src/group-theory/loop-groups-sets.lagda.md @@ -205,7 +205,7 @@ module _ hom-abstract-automorphism-group-loop-group-Set : hom-Group ( loop-group-Set X) - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X)) pr1 hom-abstract-automorphism-group-loop-group-Set p = eq-pair-Σ @@ -239,7 +239,7 @@ module _ hom-inv-abstract-automorphism-group-loop-group-Set : hom-Group - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X)) ( loop-group-Set X) pr1 hom-inv-abstract-automorphism-group-loop-group-Set p = @@ -253,15 +253,15 @@ module _ is-section-hom-inv-abstract-automorphism-group-loop-group-Set : Id ( comp-hom-Group - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X)) ( loop-group-Set X) - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X)) ( hom-abstract-automorphism-group-loop-group-Set) ( hom-inv-abstract-automorphism-group-loop-group-Set)) ( id-hom-Group - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X))) is-section-hom-inv-abstract-automorphism-group-loop-group-Set = eq-pair-Σ @@ -284,10 +284,10 @@ module _ ( eq-is-prop ( is-prop-preserves-mul-Semigroup ( semigroup-Group - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X))) ( semigroup-Group - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X))) ( id))) @@ -295,7 +295,7 @@ module _ Id ( comp-hom-Group ( loop-group-Set X) - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X)) ( loop-group-Set X) ( hom-inv-abstract-automorphism-group-loop-group-Set) @@ -327,7 +327,7 @@ module _ iso-abstract-automorphism-group-loop-group-Set : iso-Group ( loop-group-Set X) - ( abstract-group-Concrete-Group + ( group-Concrete-Group ( Automorphism-Group (Set-1-Type l) X)) pr1 iso-abstract-automorphism-group-loop-group-Set = hom-abstract-automorphism-group-loop-group-Set diff --git a/src/group-theory/symmetric-groups.lagda.md b/src/group-theory/symmetric-groups.lagda.md index 62c371ed47..ca763dcc5a 100644 --- a/src/group-theory/symmetric-groups.lagda.md +++ b/src/group-theory/symmetric-groups.lagda.md @@ -181,7 +181,7 @@ module _ preserves-mul-compute-symmetric-Concrete-Group : preserves-mul-Group - ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A)) + ( op-group-Concrete-Group (symmetric-Concrete-Group A)) ( symmetric-Group A) ( map-compute-symmetric-Concrete-Group) preserves-mul-compute-symmetric-Concrete-Group = @@ -192,7 +192,7 @@ module _ equiv-group-compute-symmetric-Concrete-Group : equiv-Group - ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A)) + ( op-group-Concrete-Group (symmetric-Concrete-Group A)) ( symmetric-Group A) pr1 equiv-group-compute-symmetric-Concrete-Group = equiv-compute-symmetric-Concrete-Group @@ -201,24 +201,24 @@ module _ compute-symmetric-Concrete-Group' : iso-Group - ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A)) + ( op-group-Concrete-Group (symmetric-Concrete-Group A)) ( symmetric-Group A) compute-symmetric-Concrete-Group' = iso-equiv-Group - ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A)) + ( op-group-Concrete-Group (symmetric-Concrete-Group A)) ( symmetric-Group A) ( equiv-group-compute-symmetric-Concrete-Group) compute-symmetric-Concrete-Group : iso-Group - ( abstract-group-Concrete-Group (symmetric-Concrete-Group A)) + ( group-Concrete-Group (symmetric-Concrete-Group A)) ( symmetric-Group A) compute-symmetric-Concrete-Group = comp-iso-Group - ( abstract-group-Concrete-Group (symmetric-Concrete-Group A)) - ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A)) + ( group-Concrete-Group (symmetric-Concrete-Group A)) + ( op-group-Concrete-Group (symmetric-Concrete-Group A)) ( symmetric-Group A) ( compute-symmetric-Concrete-Group') ( iso-inv-Group - ( abstract-group-Concrete-Group (symmetric-Concrete-Group A))) + ( group-Concrete-Group (symmetric-Concrete-Group A))) ``` diff --git a/src/group-theory/torsors.lagda.md b/src/group-theory/torsors.lagda.md index e7cd83e775..871157b23e 100644 --- a/src/group-theory/torsors.lagda.md +++ b/src/group-theory/torsors.lagda.md @@ -678,11 +678,11 @@ module _ is-0-connected-classifying-type-Group = is-0-connected-classifying-type-Concrete-Group concrete-group-Group - abstract-group-concrete-group-Group : - iso-Group (abstract-group-Concrete-Group concrete-group-Group) G - abstract-group-concrete-group-Group = + group-concrete-group-Group : + iso-Group (group-Concrete-Group concrete-group-Group) G + group-concrete-group-Group = iso-equiv-Group - ( abstract-group-Concrete-Group concrete-group-Group) + ( group-Concrete-Group concrete-group-Group) ( G) ( ( equiv-Eq-equiv-Torsor-Abstract-Group ( principal-Torsor-Abstract-Group G)) ,