This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The opposite of a group

module group-theory.opposite-groups where
Imports 
open import foundation.dependent-pair-types
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

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.

Definition

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-Semigroup (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

The opposite group of G is isomorphic to G

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

  equiv-inv-Group : equiv-Group G (op-Group G)
  pr1 equiv-inv-Group = equiv-equiv-inv-Group G
  pr2 equiv-inv-Group = distributive-inv-mul-Group G

  iso-inv-Group : iso-Group G (op-Group G)
  iso-inv-Group = iso-equiv-Group G (op-Group G) equiv-inv-Group