# Invertible elements in monoids

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Gregor Perčič.

Created on 2022-03-17.

module group-theory.invertible-elements-monoids where

Imports
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.monoids


## Idea

An element x : M in a monoid M is said to be left invertible if there is an element y : M such that yx ＝ e, and it is said to be right invertible if there is an element y : M such that xy ＝ e. The element x is said to be invertible if it has a two-sided inverse, i.e., if if there is an element y : M such that xy = e and yx = e. Left inverses of elements are also called retractions and right inverses are also called sections.

## Definitions

### Right invertible elements

module _
{l : Level} (M : Monoid l) (x : type-Monoid M)
where

is-right-inverse-element-Monoid : type-Monoid M → UU l
is-right-inverse-element-Monoid y = mul-Monoid M x y ＝ unit-Monoid M

is-right-invertible-element-Monoid : UU l
is-right-invertible-element-Monoid =
Σ (type-Monoid M) is-right-inverse-element-Monoid

module _
{l : Level} (M : Monoid l) {x : type-Monoid M}
where

section-is-right-invertible-element-Monoid :
is-right-invertible-element-Monoid M x → type-Monoid M
section-is-right-invertible-element-Monoid = pr1

is-right-inverse-section-is-right-invertible-element-Monoid :
(H : is-right-invertible-element-Monoid M x) →
is-right-inverse-element-Monoid M x
( section-is-right-invertible-element-Monoid H)
is-right-inverse-section-is-right-invertible-element-Monoid = pr2


### Left invertible elements

module _
{l : Level} (M : Monoid l) (x : type-Monoid M)
where

is-left-inverse-element-Monoid : type-Monoid M → UU l
is-left-inverse-element-Monoid y = mul-Monoid M y x ＝ unit-Monoid M

is-left-invertible-element-Monoid : UU l
is-left-invertible-element-Monoid =
Σ (type-Monoid M) is-left-inverse-element-Monoid

module _
{l : Level} (M : Monoid l) {x : type-Monoid M}
where

retraction-is-left-invertible-element-Monoid :
is-left-invertible-element-Monoid M x → type-Monoid M
retraction-is-left-invertible-element-Monoid = pr1

is-left-inverse-retraction-is-left-invertible-element-Monoid :
(H : is-left-invertible-element-Monoid M x) →
is-left-inverse-element-Monoid M x
( retraction-is-left-invertible-element-Monoid H)
is-left-inverse-retraction-is-left-invertible-element-Monoid = pr2


### Invertible elements

module _
{l : Level} (M : Monoid l) (x : type-Monoid M)
where

is-inverse-element-Monoid : type-Monoid M → UU l
is-inverse-element-Monoid y =
is-right-inverse-element-Monoid M x y ×
is-left-inverse-element-Monoid M x y

is-invertible-element-Monoid : UU l
is-invertible-element-Monoid =
Σ (type-Monoid M) is-inverse-element-Monoid

module _
{l : Level} (M : Monoid l) {x : type-Monoid M}
where

inv-is-invertible-element-Monoid :
is-invertible-element-Monoid M x → type-Monoid M
inv-is-invertible-element-Monoid = pr1

is-right-inverse-inv-is-invertible-element-Monoid :
(H : is-invertible-element-Monoid M x) →
is-right-inverse-element-Monoid M x (inv-is-invertible-element-Monoid H)
is-right-inverse-inv-is-invertible-element-Monoid H = pr1 (pr2 H)

is-left-inverse-inv-is-invertible-element-Monoid :
(H : is-invertible-element-Monoid M x) →
is-left-inverse-element-Monoid M x (inv-is-invertible-element-Monoid H)
is-left-inverse-inv-is-invertible-element-Monoid H = pr2 (pr2 H)


## Properties

### Being an invertible element is a property

module _
{l : Level} (M : Monoid l)
where

all-elements-equal-is-invertible-element-Monoid :
(x : type-Monoid M) → all-elements-equal (is-invertible-element-Monoid M x)
all-elements-equal-is-invertible-element-Monoid x (y , p , q) (y' , p' , q') =
eq-type-subtype
( λ z →
product-Prop
( Id-Prop (set-Monoid M) (mul-Monoid M x z) (unit-Monoid M))
( Id-Prop (set-Monoid M) (mul-Monoid M z x) (unit-Monoid M)))
( ( inv (left-unit-law-mul-Monoid M y)) ∙
( inv (ap (λ z → mul-Monoid M z y) q')) ∙
( associative-mul-Monoid M y' x y) ∙
( ap (mul-Monoid M y') p) ∙
( right-unit-law-mul-Monoid M y'))

is-prop-is-invertible-element-Monoid :
(x : type-Monoid M) → is-prop (is-invertible-element-Monoid M x)
is-prop-is-invertible-element-Monoid x =
is-prop-all-elements-equal
( all-elements-equal-is-invertible-element-Monoid x)

is-invertible-element-prop-Monoid : type-Monoid M → Prop l
pr1 (is-invertible-element-prop-Monoid x) =
is-invertible-element-Monoid M x
pr2 (is-invertible-element-prop-Monoid x) =
is-prop-is-invertible-element-Monoid x


### Inverses are left/right inverses

module _
{l : Level} (M : Monoid l)
where

is-left-invertible-is-invertible-element-Monoid :
(x : type-Monoid M) →
is-invertible-element-Monoid M x → is-left-invertible-element-Monoid M x
pr1 (is-left-invertible-is-invertible-element-Monoid x is-invertible-x) =
pr1 is-invertible-x
pr2 (is-left-invertible-is-invertible-element-Monoid x is-invertible-x) =
pr2 (pr2 is-invertible-x)

is-right-invertible-is-invertible-element-Monoid :
(x : type-Monoid M) →
is-invertible-element-Monoid M x → is-right-invertible-element-Monoid M x
pr1 (is-right-invertible-is-invertible-element-Monoid x is-invertible-x) =
pr1 is-invertible-x
pr2 (is-right-invertible-is-invertible-element-Monoid x is-invertible-x) =
pr1 (pr2 is-invertible-x)


### The inverse invertible element

module _
{l : Level} (M : Monoid l)
where

is-right-invertible-left-inverse-Monoid :
(x : type-Monoid M) (lx : is-left-invertible-element-Monoid M x) →
is-right-invertible-element-Monoid M (pr1 lx)
pr1 (is-right-invertible-left-inverse-Monoid x lx) = x
pr2 (is-right-invertible-left-inverse-Monoid x lx) = pr2 lx

is-left-invertible-right-inverse-Monoid :
(x : type-Monoid M) (rx : is-right-invertible-element-Monoid M x) →
is-left-invertible-element-Monoid M (pr1 rx)
pr1 (is-left-invertible-right-inverse-Monoid x rx) = x
pr2 (is-left-invertible-right-inverse-Monoid x rx) = pr2 rx

is-invertible-element-inverse-Monoid :
(x : type-Monoid M) (x' : is-invertible-element-Monoid M x) →
is-invertible-element-Monoid M (pr1 x')
pr1 (is-invertible-element-inverse-Monoid x x') = x
pr1 (pr2 (is-invertible-element-inverse-Monoid x x')) = pr2 (pr2 x')
pr2 (pr2 (is-invertible-element-inverse-Monoid x x')) = pr1 (pr2 x')


### Any invertible element of a monoid has a contractible type of right inverses

module _
{l : Level} (M : Monoid l)
where

is-contr-is-right-invertible-element-Monoid :
(x : type-Monoid M) → is-invertible-element-Monoid M x →
is-contr (is-right-invertible-element-Monoid M x)
pr1 (pr1 (is-contr-is-right-invertible-element-Monoid x (y , p , q))) = y
pr2 (pr1 (is-contr-is-right-invertible-element-Monoid x (y , p , q))) = p
pr2 (is-contr-is-right-invertible-element-Monoid x (y , p , q)) (y' , q') =
eq-type-subtype
( λ u → Id-Prop (set-Monoid M) (mul-Monoid M x u) (unit-Monoid M))
( ( inv (right-unit-law-mul-Monoid M y)) ∙
( ap (mul-Monoid M y) (inv q')) ∙
( inv (associative-mul-Monoid M y x y')) ∙
( ap (mul-Monoid' M y') q) ∙
( left-unit-law-mul-Monoid M y'))


### Any invertible element of a monoid has a contractible type of left inverses

module _
{l : Level} (M : Monoid l)
where

is-contr-is-left-invertible-Monoid :
(x : type-Monoid M) → is-invertible-element-Monoid M x →
is-contr (is-left-invertible-element-Monoid M x)
pr1 (pr1 (is-contr-is-left-invertible-Monoid x (y , p , q))) = y
pr2 (pr1 (is-contr-is-left-invertible-Monoid x (y , p , q))) = q
pr2 (is-contr-is-left-invertible-Monoid x (y , p , q)) (y' , p') =
eq-type-subtype
( λ u → Id-Prop (set-Monoid M) (mul-Monoid M u x) (unit-Monoid M))
( ( inv (left-unit-law-mul-Monoid M y)) ∙
( ap (mul-Monoid' M y) (inv p')) ∙
( associative-mul-Monoid M y' x y) ∙
( ap (mul-Monoid M y') p) ∙
( right-unit-law-mul-Monoid M y'))


### The unit of a monoid is invertible

module _
{l : Level} (M : Monoid l)
where

is-left-invertible-element-unit-Monoid :
is-left-invertible-element-Monoid M (unit-Monoid M)
pr1 is-left-invertible-element-unit-Monoid = unit-Monoid M
pr2 is-left-invertible-element-unit-Monoid =
left-unit-law-mul-Monoid M (unit-Monoid M)

is-right-invertible-element-unit-Monoid :
is-right-invertible-element-Monoid M (unit-Monoid M)
pr1 is-right-invertible-element-unit-Monoid = unit-Monoid M
pr2 is-right-invertible-element-unit-Monoid =
left-unit-law-mul-Monoid M (unit-Monoid M)

is-invertible-element-unit-Monoid :
is-invertible-element-Monoid M (unit-Monoid M)
pr1 is-invertible-element-unit-Monoid =
unit-Monoid M
pr1 (pr2 is-invertible-element-unit-Monoid) =
left-unit-law-mul-Monoid M (unit-Monoid M)
pr2 (pr2 is-invertible-element-unit-Monoid) =
left-unit-law-mul-Monoid M (unit-Monoid M)


### Invertible elements are closed under multiplication

module _
{l : Level} (M : Monoid l)
where

is-left-invertible-element-mul-Monoid :
(x y : type-Monoid M) →
is-left-invertible-element-Monoid M x →
is-left-invertible-element-Monoid M y →
is-left-invertible-element-Monoid M (mul-Monoid M x y)
pr1 (is-left-invertible-element-mul-Monoid x y (lx , H) (ly , I)) =
mul-Monoid M ly lx
pr2 (is-left-invertible-element-mul-Monoid x y (lx , H) (ly , I)) =
( associative-mul-Monoid M ly lx (mul-Monoid M x y)) ∙
( ap
( mul-Monoid M ly)
( ( inv (associative-mul-Monoid M lx x y)) ∙
( ap (λ z → mul-Monoid M z y) H) ∙
( left-unit-law-mul-Monoid M y))) ∙
( I)

is-right-invertible-element-mul-Monoid :
(x y : type-Monoid M) →
is-right-invertible-element-Monoid M x →
is-right-invertible-element-Monoid M y →
is-right-invertible-element-Monoid M (mul-Monoid M x y)
pr1 (is-right-invertible-element-mul-Monoid x y (rx , H) (ry , I)) =
mul-Monoid M ry rx
pr2 (is-right-invertible-element-mul-Monoid x y (rx , H) (ry , I)) =
( associative-mul-Monoid M x y (mul-Monoid M ry rx)) ∙
( ap
( mul-Monoid M x)
( ( inv (associative-mul-Monoid M y ry rx)) ∙
( ap (λ z → mul-Monoid M z rx) I) ∙
( left-unit-law-mul-Monoid M rx))) ∙
( H)

is-invertible-element-mul-Monoid :
(x y : type-Monoid M) →
is-invertible-element-Monoid M x →
is-invertible-element-Monoid M y →
is-invertible-element-Monoid M (mul-Monoid M x y)
pr1 (is-invertible-element-mul-Monoid x y (x' , Lx , Rx) (y' , Ly , Ry)) =
mul-Monoid M y' x'
pr1 (pr2 (is-invertible-element-mul-Monoid x y H K)) =
pr2
( is-right-invertible-element-mul-Monoid x y
( is-right-invertible-is-invertible-element-Monoid M x H)
( is-right-invertible-is-invertible-element-Monoid M y K))
pr2 (pr2 (is-invertible-element-mul-Monoid x y H K)) =
pr2
( is-left-invertible-element-mul-Monoid x y
( is-left-invertible-is-invertible-element-Monoid M x H)
( is-left-invertible-is-invertible-element-Monoid M y K))


### The inverse of an invertible element is invertible

module _
{l : Level} (M : Monoid l)
where

is-invertible-element-inv-is-invertible-element-Monoid :
{x : type-Monoid M} (H : is-invertible-element-Monoid M x) →
is-invertible-element-Monoid M (inv-is-invertible-element-Monoid M H)
pr1 (is-invertible-element-inv-is-invertible-element-Monoid {x} H) = x
pr1 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) =
is-left-inverse-inv-is-invertible-element-Monoid M H
pr2 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) =
is-right-inverse-inv-is-invertible-element-Monoid M H


### An element is invertible if and only if multiplying by it is an equivalence

Proof: Suppose that the map z ↦ xz is an equivalence. Then there is a unique element y such that xy ＝ 1. Thus we have a right inverse of x. To see that y is also a left inverse of x, note that the map z ↦ xz is injective by the assumption that it is an equivalence. Therefore it suffices to show that x(yx) ＝ x1. This follows from the following calculation:

  x(yx) ＝ (xy)x ＝ 1x ＝ x ＝ x1.


This completes the proof that if z ↦ xz is an equivalence, then x is invertible. The converse is straightfoward.

In the following code we give the above proof, as well as the analogous proof that x is invertible if z ↦ zx is an equivalence, and the converse of both statements.

#### An element x is invertible if and only if z ↦ xz is an equivalence

module _
{l : Level} (M : Monoid l) {x : type-Monoid M}
where

inv-is-invertible-element-is-equiv-mul-Monoid :
is-equiv (mul-Monoid M x) → type-Monoid M
inv-is-invertible-element-is-equiv-mul-Monoid H =
map-inv-is-equiv H (unit-Monoid M)

is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
(H : is-equiv (mul-Monoid M x)) →
mul-Monoid M x (inv-is-invertible-element-is-equiv-mul-Monoid H) ＝
unit-Monoid M
is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
is-section-map-inv-is-equiv H (unit-Monoid M)

is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid :
(H : is-equiv (mul-Monoid M x)) →
mul-Monoid M (inv-is-invertible-element-is-equiv-mul-Monoid H) x ＝
unit-Monoid M
is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H =
is-injective-is-equiv H
( ( inv (associative-mul-Monoid M _ _ _)) ∙
( ap
( mul-Monoid' M x)
( is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H)) ∙
( left-unit-law-mul-Monoid M x) ∙
( inv (right-unit-law-mul-Monoid M x)))

is-invertible-element-is-equiv-mul-Monoid :
is-equiv (mul-Monoid M x) → is-invertible-element-Monoid M x
pr1 (is-invertible-element-is-equiv-mul-Monoid H) =
inv-is-invertible-element-is-equiv-mul-Monoid H
pr1 (pr2 (is-invertible-element-is-equiv-mul-Monoid H)) =
is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H
pr2 (pr2 (is-invertible-element-is-equiv-mul-Monoid H)) =
is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid H

left-div-is-invertible-element-Monoid :
is-invertible-element-Monoid M x → type-Monoid M → type-Monoid M
left-div-is-invertible-element-Monoid H =
mul-Monoid M (inv-is-invertible-element-Monoid M H)

is-section-left-div-is-invertible-element-Monoid :
(H : is-invertible-element-Monoid M x) →
mul-Monoid M x ∘ left-div-is-invertible-element-Monoid H ~ id
is-section-left-div-is-invertible-element-Monoid H y =
( inv (associative-mul-Monoid M _ _ _)) ∙
( ap
( mul-Monoid' M y)
( is-right-inverse-inv-is-invertible-element-Monoid M H)) ∙
( left-unit-law-mul-Monoid M y)

is-retraction-left-div-is-invertible-element-Monoid :
(H : is-invertible-element-Monoid M x) →
left-div-is-invertible-element-Monoid H ∘ mul-Monoid M x ~ id
is-retraction-left-div-is-invertible-element-Monoid H y =
( inv (associative-mul-Monoid M _ _ _)) ∙
( ap
( mul-Monoid' M y)
( is-left-inverse-inv-is-invertible-element-Monoid M H)) ∙
( left-unit-law-mul-Monoid M y)

is-equiv-mul-is-invertible-element-Monoid :
is-invertible-element-Monoid M x → is-equiv (mul-Monoid M x)
is-equiv-mul-is-invertible-element-Monoid H =
is-equiv-is-invertible
( left-div-is-invertible-element-Monoid H)
( is-section-left-div-is-invertible-element-Monoid H)
( is-retraction-left-div-is-invertible-element-Monoid H)


#### An element x is invertible if and only if z ↦ zx is an equivalence

module _
{l : Level} (M : Monoid l) {x : type-Monoid M}
where

inv-is-invertible-element-is-equiv-mul-Monoid' :
is-equiv (mul-Monoid' M x) → type-Monoid M
inv-is-invertible-element-is-equiv-mul-Monoid' H =
map-inv-is-equiv H (unit-Monoid M)

is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' :
(H : is-equiv (mul-Monoid' M x)) →
mul-Monoid M (inv-is-invertible-element-is-equiv-mul-Monoid' H) x ＝
unit-Monoid M
is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H =
is-section-map-inv-is-equiv H (unit-Monoid M)

is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' :
(H : is-equiv (mul-Monoid' M x)) →
mul-Monoid M x (inv-is-invertible-element-is-equiv-mul-Monoid' H) ＝
unit-Monoid M
is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H =
is-injective-is-equiv H
( ( associative-mul-Monoid M _ _ _) ∙
( ap
( mul-Monoid M x)
( is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H)) ∙
( right-unit-law-mul-Monoid M x) ∙
( inv (left-unit-law-mul-Monoid M x)))

is-invertible-element-is-equiv-mul-Monoid' :
is-equiv (mul-Monoid' M x) → is-invertible-element-Monoid M x
pr1 (is-invertible-element-is-equiv-mul-Monoid' H) =
inv-is-invertible-element-is-equiv-mul-Monoid' H
pr1 (pr2 (is-invertible-element-is-equiv-mul-Monoid' H)) =
is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H
pr2 (pr2 (is-invertible-element-is-equiv-mul-Monoid' H)) =
is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid' H

right-div-is-invertible-element-Monoid :
is-invertible-element-Monoid M x → type-Monoid M → type-Monoid M
right-div-is-invertible-element-Monoid H =
mul-Monoid' M (inv-is-invertible-element-Monoid M H)

is-section-right-div-is-invertible-element-Monoid :
(H : is-invertible-element-Monoid M x) →
mul-Monoid' M x ∘ right-div-is-invertible-element-Monoid H ~ id
is-section-right-div-is-invertible-element-Monoid H y =
( associative-mul-Monoid M _ _ _) ∙
( ap
( mul-Monoid M y)
( is-left-inverse-inv-is-invertible-element-Monoid M H)) ∙
( right-unit-law-mul-Monoid M y)

is-retraction-right-div-is-invertible-element-Monoid :
(H : is-invertible-element-Monoid M x) →
right-div-is-invertible-element-Monoid H ∘ mul-Monoid' M x ~ id
is-retraction-right-div-is-invertible-element-Monoid H y =
( associative-mul-Monoid M _ _ _) ∙
( ap
( mul-Monoid M y)
( is-right-inverse-inv-is-invertible-element-Monoid M H)) ∙
( right-unit-law-mul-Monoid M y)

is-equiv-mul-is-invertible-element-Monoid' :
is-invertible-element-Monoid M x → is-equiv (mul-Monoid' M x)
is-equiv-mul-is-invertible-element-Monoid' H =
is-equiv-is-invertible
( right-div-is-invertible-element-Monoid H)
( is-section-right-div-is-invertible-element-Monoid H)
( is-retraction-right-div-is-invertible-element-Monoid H)