Torsors of abstract groups

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-07-09.
Last modified on 2023-11-24.

module group-theory.torsors where
Imports 
open import foundation.0-connected-types
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.mere-equality
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.retractions
open import foundation.sections
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import group-theory.concrete-groups
open import group-theory.equivalences-group-actions
open import group-theory.group-actions
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.isomorphisms-groups
open import group-theory.mere-equivalences-group-actions
open import group-theory.principal-group-actions
open import group-theory.symmetric-groups

open import higher-group-theory.higher-groups

Idea

A torsor of a group G is a group action which is merely equivalent to the principal group action of G.

Definitions

The predicate of being a torsor

module _
  {l1 l2 : Level} (G : Group l1) (X : action-Group G l2)
  where

  is-torsor-prop-action-Group : Prop (l1 ⊔ l2)
  is-torsor-prop-action-Group =
    mere-equiv-prop-action-Group G (principal-action-Group G) X

  is-torsor-Group : UU (l1 ⊔ l2)
  is-torsor-Group = type-Prop is-torsor-prop-action-Group

  is-prop-is-torsor-Group : is-prop is-torsor-Group
  is-prop-is-torsor-Group = is-prop-type-Prop is-torsor-prop-action-Group

The type of torsors

module _
  {l1 : Level} (G : Group l1)
  where

  Torsor-Group : (l : Level) → UU (l1 ⊔ lsuc l)
  Torsor-Group l = Σ (action-Group G l) (is-torsor-Group G)

module _
  {l1 l : Level} (G : Group l1) (X : Torsor-Group G l)
  where

  action-Torsor-Group : action-Group G l
  action-Torsor-Group = pr1 X

  set-Torsor-Group : Set l
  set-Torsor-Group = set-action-Group G action-Torsor-Group

  type-Torsor-Group : UU l
  type-Torsor-Group = type-Set set-Torsor-Group

  is-set-type-Torsor-Group : is-set type-Torsor-Group
  is-set-type-Torsor-Group = is-set-type-Set set-Torsor-Group

  mul-hom-Torsor-Group : hom-Group G (symmetric-Group set-Torsor-Group)
  mul-hom-Torsor-Group = pr2 action-Torsor-Group

  equiv-mul-Torsor-Group : type-Group G → type-Torsor-Group ≃ type-Torsor-Group
  equiv-mul-Torsor-Group = equiv-mul-action-Group G action-Torsor-Group

  mul-Torsor-Group : type-Group G → type-Torsor-Group → type-Torsor-Group
  mul-Torsor-Group = mul-action-Group G action-Torsor-Group

  is-torsor-action-Torsor-Group : is-torsor-Group G action-Torsor-Group
  is-torsor-action-Torsor-Group = pr2 X

Principal torsor

module _
  {l1 : Level} (G : Group l1)
  where

  principal-Torsor-Group : Torsor-Group G l1
  pr1 principal-Torsor-Group = principal-action-Group G
  pr2 principal-Torsor-Group =
    unit-trunc-Prop (id-equiv-action-Group G (principal-action-Group G))

Properties

Characterization of the identity type of Torsor-Group

module _
  {l1 l2 : Level} (G : Group l1) (X : Torsor-Group G l2)
  where

  equiv-Torsor-Group :
    {l3 : Level} (Y : Torsor-Group G l3) → UU (l1 ⊔ l2 ⊔ l3)
  equiv-Torsor-Group Y =
    equiv-action-Group G (action-Torsor-Group G X) (action-Torsor-Group G Y)

  id-equiv-Torsor-Group : equiv-Torsor-Group X
  id-equiv-Torsor-Group = id-equiv-action-Group G (action-Torsor-Group G X)

  equiv-eq-Torsor-Group :
    (Y : Torsor-Group G l2) → X ＝ Y → equiv-Torsor-Group Y
  equiv-eq-Torsor-Group .X refl = id-equiv-Torsor-Group

  is-torsorial-equiv-Torsor-Group :
    is-torsorial equiv-Torsor-Group
  is-torsorial-equiv-Torsor-Group =
    is-torsorial-Eq-subtype
      ( is-torsorial-equiv-action-Group G (action-Torsor-Group G X))
      ( is-prop-is-torsor-Group G)
      ( action-Torsor-Group G X)
      ( id-equiv-Torsor-Group)
      ( is-torsor-action-Torsor-Group G X)

  is-equiv-equiv-eq-Torsor-Group :
    (Y : Torsor-Group G l2) →
    is-equiv (equiv-eq-Torsor-Group Y)
  is-equiv-equiv-eq-Torsor-Group =
    fundamental-theorem-id
      is-torsorial-equiv-Torsor-Group
      equiv-eq-Torsor-Group

  eq-equiv-Torsor-Group :
    (Y : Torsor-Group G l2) → equiv-Torsor-Group Y → X ＝ Y
  eq-equiv-Torsor-Group Y =
    map-inv-is-equiv (is-equiv-equiv-eq-Torsor-Group Y)

  extensionality-Torsor-Group :
    (Y : Torsor-Group G l2) → (X ＝ Y) ≃ equiv-Torsor-Group Y
  pr1 (extensionality-Torsor-Group Y) = equiv-eq-Torsor-Group Y
  pr2 (extensionality-Torsor-Group Y) = is-equiv-equiv-eq-Torsor-Group Y

Characterization of the identity type of equivalences between Torsor-Group

module _
  {l1 l2 l3 : Level} (G : Group l1)
  (X : Torsor-Group G l2)
  (Y : Torsor-Group G l3)
  (e : equiv-Torsor-Group G X Y)
  where

  htpy-equiv-Torsor-Group :
    equiv-Torsor-Group G X Y → UU (l2 ⊔ l3)
  htpy-equiv-Torsor-Group =
    htpy-equiv-action-Group G
      ( action-Torsor-Group G X)
      ( action-Torsor-Group G Y)
      ( e)

  refl-htpy-equiv-Torsor-Group :
    htpy-equiv-Torsor-Group e
  refl-htpy-equiv-Torsor-Group =
    refl-htpy-equiv-action-Group G
      ( action-Torsor-Group G X)
      ( action-Torsor-Group G Y)
      ( e)

  htpy-eq-equiv-Torsor-Group :
    (f : equiv-Torsor-Group G X Y) →
    e ＝ f → htpy-equiv-Torsor-Group f
  htpy-eq-equiv-Torsor-Group .e refl =
    refl-htpy-equiv-Torsor-Group

  is-torsorial-htpy-equiv-Torsor-Group :
    is-torsorial htpy-equiv-Torsor-Group
  is-torsorial-htpy-equiv-Torsor-Group =
    is-torsorial-htpy-equiv-action-Group G
      ( action-Torsor-Group G X)
      ( action-Torsor-Group G Y)
      ( e)

  is-equiv-htpy-eq-equiv-Torsor-Group :
    (f : equiv-Torsor-Group G X Y) →
    is-equiv (htpy-eq-equiv-Torsor-Group f)
  is-equiv-htpy-eq-equiv-Torsor-Group =
    fundamental-theorem-id
      is-torsorial-htpy-equiv-Torsor-Group
      htpy-eq-equiv-Torsor-Group

  extensionality-equiv-Torsor-Group :
    (f : equiv-Torsor-Group G X Y) →
    (e ＝ f) ≃ htpy-equiv-Torsor-Group f
  pr1 (extensionality-equiv-Torsor-Group f) =
    htpy-eq-equiv-Torsor-Group f
  pr2 (extensionality-equiv-Torsor-Group f) =
    is-equiv-htpy-eq-equiv-Torsor-Group f

  eq-htpy-equiv-Torsor-Group :
    (f : equiv-Torsor-Group G X Y) → htpy-equiv-Torsor-Group f → e ＝ f
  eq-htpy-equiv-Torsor-Group f =
    map-inv-is-equiv (is-equiv-htpy-eq-equiv-Torsor-Group f)

Definition of the group aut-principal-Torsor-Group from a Torsor-Group

module _
  {l1 l2 l3 : Level} (G : Group l1)
  (X : Torsor-Group G l2)
  (Y : Torsor-Group G l3)
  where

  is-set-equiv-Torsor-Group :
    is-set (equiv-Torsor-Group G X Y)
  is-set-equiv-Torsor-Group e f =
    is-prop-equiv
      ( extensionality-equiv-Torsor-Group G X Y e f)
      ( is-prop-Π
        ( λ x →
          is-set-type-Torsor-Group G Y
            ( map-equiv (pr1 e) x)
            ( map-equiv (pr1 f) x)))

module _
  {l1 l2 l3 l4 : Level} (G : Group l1)
  (X : Torsor-Group G l2)
  (Y : Torsor-Group G l3)
  (Z : Torsor-Group G l4)
  where

  comp-equiv-Torsor-Group :
    equiv-Torsor-Group G Y Z →
    equiv-Torsor-Group G X Y →
    equiv-Torsor-Group G X Z
  comp-equiv-Torsor-Group =
    comp-equiv-action-Group G
      ( action-Torsor-Group G X)
      ( action-Torsor-Group G Y)
      ( action-Torsor-Group G Z)

  comp-equiv-Torsor-Group' :
    equiv-Torsor-Group G X Y →
    equiv-Torsor-Group G Y Z →
    equiv-Torsor-Group G X Z
  comp-equiv-Torsor-Group' e f =
    comp-equiv-Torsor-Group f e

module _
  {l1 l2 l3 : Level} (G : Group l1)
  (X : Torsor-Group G l2)
  (Y : Torsor-Group G l3)
  where

  inv-equiv-Torsor-Group :
    equiv-Torsor-Group G X Y →
    equiv-Torsor-Group G Y X
  inv-equiv-Torsor-Group =
    inv-equiv-action-Group G
      ( action-Torsor-Group G X)
      ( action-Torsor-Group G Y)

module _
  {l1 l2 l3 l4 l5 : Level} (G : Group l1)
  (X1 : Torsor-Group G l2)
  (X2 : Torsor-Group G l3)
  (X3 : Torsor-Group G l4)
  (X4 : Torsor-Group G l5)
  where

  associative-comp-equiv-Torsor-Group :
    (h : equiv-Torsor-Group G X3 X4)
    (g : equiv-Torsor-Group G X2 X3)
    (f : equiv-Torsor-Group G X1 X2) →
    ( comp-equiv-Torsor-Group G X1 X2 X4
      ( comp-equiv-Torsor-Group G X2 X3 X4 h g)
      ( f)) ＝
    ( comp-equiv-Torsor-Group G X1 X3 X4 h
      ( comp-equiv-Torsor-Group G X1 X2 X3 g f))
  associative-comp-equiv-Torsor-Group h g f =
    eq-htpy-equiv-Torsor-Group G X1 X4
      ( comp-equiv-Torsor-Group G X1 X2 X4
        ( comp-equiv-Torsor-Group G X2 X3 X4 h g)
        ( f))
      ( comp-equiv-Torsor-Group G X1 X3 X4 h
        ( comp-equiv-Torsor-Group G X1 X2 X3 g f))
      ( refl-htpy)

module _
  {l1 l2 l3 : Level} (G : Group l1)
  (X : Torsor-Group G l2)
  (Y : Torsor-Group G l3)
  where

  left-unit-law-comp-equiv-Torsor-Group :
    (f : equiv-Torsor-Group G X Y) →
    ( comp-equiv-Torsor-Group G X Y Y (id-equiv-Torsor-Group G Y) f) ＝ f
  left-unit-law-comp-equiv-Torsor-Group f =
    eq-htpy-equiv-Torsor-Group G X Y
      ( comp-equiv-Torsor-Group G X Y Y
        ( id-equiv-Torsor-Group G Y)
        ( f))
      ( f)
      ( refl-htpy)

  right-unit-law-comp-equiv-Torsor-Group :
    (f : equiv-Torsor-Group G X Y) →
    ( comp-equiv-Torsor-Group G X X Y f (id-equiv-Torsor-Group G X)) ＝ f
  right-unit-law-comp-equiv-Torsor-Group f =
    eq-htpy-equiv-Torsor-Group G X Y
      ( comp-equiv-Torsor-Group G X X Y f
        ( id-equiv-Torsor-Group G X))
      ( f)
      ( refl-htpy)

  left-inverse-law-comp-equiv-Torsor-Group :
    (f : equiv-Torsor-Group G X Y) →
    ( comp-equiv-Torsor-Group G X Y X (inv-equiv-Torsor-Group G X Y f) f) ＝
    ( id-equiv-Torsor-Group G X)
  left-inverse-law-comp-equiv-Torsor-Group f =
    eq-htpy-equiv-Torsor-Group G X X
      ( comp-equiv-Torsor-Group G X Y X
        ( inv-equiv-Torsor-Group G X Y f)
        ( f))
      ( id-equiv-Torsor-Group G X)
      ( is-retraction-map-inv-equiv (pr1 f))

  right-inverse-law-comp-equiv-Torsor-Group :
    (f : equiv-Torsor-Group G X Y) →
    ( comp-equiv-Torsor-Group G Y X Y f (inv-equiv-Torsor-Group G X Y f)) ＝
    ( id-equiv-Torsor-Group G Y)
  right-inverse-law-comp-equiv-Torsor-Group f =
    eq-htpy-equiv-Torsor-Group G Y Y
      ( comp-equiv-Torsor-Group G Y X Y f (inv-equiv-Torsor-Group G X Y f))
      ( id-equiv-Torsor-Group G Y)
      ( is-section-map-inv-equiv (pr1 f))

module _
  {l1 : Level} (G : Group l1)
  where

  preserves-mul-equiv-eq-Torsor-Group :
    {l2 : Level} (X Y Z : Torsor-Group G l2)
    (p : X ＝ Y) (q : Y ＝ Z) →
    ( equiv-eq-Torsor-Group G X Z (p ∙ q)) ＝
    ( comp-equiv-Torsor-Group G X Y Z
      ( equiv-eq-Torsor-Group G Y Z q)
      ( equiv-eq-Torsor-Group G X Y p))
  preserves-mul-equiv-eq-Torsor-Group X .X Z refl q =
    inv
      ( right-unit-law-comp-equiv-Torsor-Group G X Z
        ( equiv-eq-Torsor-Group G X Z q))

module _
  {l1 : Level} (G : Group l1)
  where

  aut-principal-Torsor-Group : Group l1
  pr1 (pr1 (pr1 aut-principal-Torsor-Group)) =
    equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr2 (pr1 (pr1 aut-principal-Torsor-Group)) =
    is-set-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr1 (pr2 (pr1 aut-principal-Torsor-Group)) =
    comp-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr2 (pr2 (pr1 aut-principal-Torsor-Group)) =
    associative-comp-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr1 (pr1 (pr2 aut-principal-Torsor-Group)) =
    id-equiv-Torsor-Group G (principal-Torsor-Group G)
  pr1 (pr2 (pr1 (pr2 aut-principal-Torsor-Group))) =
    left-unit-law-comp-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr2 (pr2 (pr1 (pr2 aut-principal-Torsor-Group))) =
    right-unit-law-comp-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr1 (pr2 (pr2 aut-principal-Torsor-Group)) =
    inv-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr1 (pr2 (pr2 (pr2 aut-principal-Torsor-Group))) =
    left-inverse-law-comp-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr2 (pr2 (pr2 (pr2 aut-principal-Torsor-Group))) =
    right-inverse-law-comp-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)

The type Torsor-Group is 0-connected

module _
  {l1 l2 : Level} (G : Group l1) (X : Torsor-Group G l2)
  where

  mere-eq-Torsor-Group :
    (Y : Torsor-Group G l2) → mere-eq X Y
  mere-eq-Torsor-Group Y =
    apply-universal-property-trunc-Prop
      ( pr2 X)
      ( mere-eq-Prop X Y)
      ( λ e →
        apply-universal-property-trunc-Prop
          ( pr2 Y)
          ( mere-eq-Prop X Y)
          ( λ f →
            unit-trunc-Prop
              ( eq-equiv-Torsor-Group G X Y
                ( comp-equiv-Torsor-Group G
                  ( X)
                  ( principal-Torsor-Group G)
                  ( Y)
                  ( f)
                  ( inv-equiv-Torsor-Group G
                    ( principal-Torsor-Group G)
                    ( X)
                    ( e))))))

module _
  {l1 : Level} (G : Group l1)
  where

  is-0-connected-Torsor-Group :
    is-0-connected (Torsor-Group G l1)
  is-0-connected-Torsor-Group =
    is-0-connected-mere-eq
      ( principal-Torsor-Group G)
      ( mere-eq-Torsor-Group G (principal-Torsor-Group G))

The group aut-principal-Torsor-Group is isomorphic to G

module _
  {l1 : Level} (G : Group l1)
  where

  Eq-Torsor-Group :
    (X : Torsor-Group G l1) → UU l1
  Eq-Torsor-Group X = type-Torsor-Group G X

  refl-Eq-Torsor-Group :
    Eq-Torsor-Group (principal-Torsor-Group G)
  refl-Eq-Torsor-Group = unit-Group G

  Eq-equiv-Torsor-Group :
    (X : Torsor-Group G l1) →
    equiv-Torsor-Group G (principal-Torsor-Group G) X →
    Eq-Torsor-Group X
  Eq-equiv-Torsor-Group X (e , H) = map-equiv e (unit-Group G)

  preserves-mul-Eq-equiv-Torsor-Group :
    ( e f :
      equiv-Torsor-Group G
        ( principal-Torsor-Group G)
        ( principal-Torsor-Group G)) →
    ( Eq-equiv-Torsor-Group
      ( principal-Torsor-Group G)
      ( comp-equiv-Torsor-Group G
        ( principal-Torsor-Group G)
        ( principal-Torsor-Group G)
        ( principal-Torsor-Group G)
        ( f)
        ( e))) ＝
    ( mul-Group G
      ( Eq-equiv-Torsor-Group
        ( principal-Torsor-Group G)
        ( e))
      ( Eq-equiv-Torsor-Group
        ( principal-Torsor-Group G)
        ( f)))
  preserves-mul-Eq-equiv-Torsor-Group (e , H) (f , K) =
    ( ap
      ( map-equiv f)
      ( inv (right-unit-law-mul-Group G (map-equiv e (unit-Group G))))) ∙
    ( K (map-equiv e (unit-Group G)) (unit-Group G))

  equiv-Eq-Torsor-Group :
    Eq-Torsor-Group (principal-Torsor-Group G) →
    equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
  pr1 (equiv-Eq-Torsor-Group u) = equiv-mul-Group' G u
  pr2 (equiv-Eq-Torsor-Group u) g x = associative-mul-Group G g x u

  is-section-equiv-Eq-Torsor-Group :
    ( Eq-equiv-Torsor-Group (principal-Torsor-Group G) ∘
      equiv-Eq-Torsor-Group) ~
    ( id)
  is-section-equiv-Eq-Torsor-Group u = left-unit-law-mul-Group G u

  is-retraction-equiv-Eq-Torsor-Group :
    is-retraction
      ( Eq-equiv-Torsor-Group (principal-Torsor-Group G))
      ( equiv-Eq-Torsor-Group)
  is-retraction-equiv-Eq-Torsor-Group e =
    eq-htpy-equiv-Torsor-Group G
      ( principal-Torsor-Group G)
      ( principal-Torsor-Group G)
      ( equiv-Eq-Torsor-Group
        ( Eq-equiv-Torsor-Group (principal-Torsor-Group G) e))
      ( e)
      ( λ g →
        ( inv (pr2 e g (unit-Group G))) ∙
        ( ap (map-equiv (pr1 e)) (right-unit-law-mul-Group G g)))

  abstract
    is-equiv-Eq-equiv-Torsor-Group :
      (X : Torsor-Group G l1) →
      is-equiv (Eq-equiv-Torsor-Group X)
    is-equiv-Eq-equiv-Torsor-Group X =
      apply-universal-property-trunc-Prop
        ( is-torsor-action-Torsor-Group G X)
        ( is-equiv-Prop (Eq-equiv-Torsor-Group X))
        ( λ e →
          tr
            ( λ Y → is-equiv (Eq-equiv-Torsor-Group Y))
            ( eq-equiv-Torsor-Group G (principal-Torsor-Group G) X e)
            ( is-equiv-is-invertible
                equiv-Eq-Torsor-Group
                is-section-equiv-Eq-Torsor-Group
                is-retraction-equiv-Eq-Torsor-Group))

  equiv-Eq-equiv-Torsor-Group :
    (X : Torsor-Group G l1) →
    (principal-Torsor-Group G ＝ X) ≃ Eq-Torsor-Group X
  equiv-Eq-equiv-Torsor-Group X =
    ( Eq-equiv-Torsor-Group X , is-equiv-Eq-equiv-Torsor-Group X) ∘e
    ( extensionality-Torsor-Group G (principal-Torsor-Group G) X)

  preserves-mul-equiv-Eq-equiv-Torsor-Group :
    { p q : principal-Torsor-Group G ＝ principal-Torsor-Group G} →
    Id
      ( map-equiv
        ( equiv-Eq-equiv-Torsor-Group (principal-Torsor-Group G))
        ( p ∙ q))
      ( mul-Group G
        ( map-equiv
          ( equiv-Eq-equiv-Torsor-Group (principal-Torsor-Group G))
          ( p))
        ( map-equiv
          ( equiv-Eq-equiv-Torsor-Group (principal-Torsor-Group G))
          ( q)))
  preserves-mul-equiv-Eq-equiv-Torsor-Group {p} {q} =
    ( ap
      ( Eq-equiv-Torsor-Group (principal-Torsor-Group G))
      ( preserves-mul-equiv-eq-Torsor-Group G
        ( principal-Torsor-Group G)
        ( principal-Torsor-Group G)
        ( principal-Torsor-Group G)
        ( p)
        ( q))) ∙
    ( preserves-mul-Eq-equiv-Torsor-Group
      ( equiv-eq-Torsor-Group G
        ( principal-Torsor-Group G)
        ( principal-Torsor-Group G)
        ( p))
      ( equiv-eq-Torsor-Group G
        ( principal-Torsor-Group G)
        ( principal-Torsor-Group G)
        ( q)))

From torsors to concrete group

  ∞-group-Group : ∞-Group (lsuc l1)
  pr1 (pr1 ∞-group-Group) = Torsor-Group G l1
  pr2 (pr1 ∞-group-Group) = principal-Torsor-Group G
  pr2 ∞-group-Group = is-0-connected-Torsor-Group G

  concrete-group-Group : Concrete-Group (lsuc l1)
  pr1 concrete-group-Group = ∞-group-Group
  pr2 concrete-group-Group =
    is-set-equiv
      ( type-Group G)
      ( equiv-Eq-equiv-Torsor-Group (principal-Torsor-Group G))
      ( is-set-type-Group G)

  classifying-type-Group : UU (lsuc l1)
  classifying-type-Group = classifying-type-Concrete-Group concrete-group-Group

  shape-Group : classifying-type-Group
  shape-Group = shape-Concrete-Group concrete-group-Group

  is-0-connected-classifying-type-Group : is-0-connected classifying-type-Group
  is-0-connected-classifying-type-Group =
    is-0-connected-classifying-type-Concrete-Group concrete-group-Group

  group-concrete-group-Group :
    iso-Group (group-Concrete-Group concrete-group-Group) G
  group-concrete-group-Group =
    iso-equiv-Group
      ( group-Concrete-Group concrete-group-Group)
      ( G)
      ( ( equiv-Eq-equiv-Torsor-Group (principal-Torsor-Group G)) ,
        ( λ {p} {q} → preserves-mul-equiv-Eq-equiv-Torsor-Group {p} {q}))

Recent changes