# The opposite of a group

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

Created on 2022-09-20.

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