# Invertible elements in rings

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

Created on 2022-03-21.
Last modified on 2024-04-25.

module ring-theory.invertible-elements-rings where

Imports
open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import group-theory.invertible-elements-monoids

open import ring-theory.rings


## Idea

Invertible elements in a ring are elements that have a two-sided multiplicative inverse. Such elements are also called the (multiplicative) units of the ring.

The set of units of any ring forms a group, called the group of units. The group of units of a ring is constructed in ring-theory.groups-of-units-rings.

## Definitions

### Left invertible elements of rings

module _
{l : Level} (R : Ring l)
where

is-left-inverse-element-Ring : (x y : type-Ring R) → UU l
is-left-inverse-element-Ring =
is-left-inverse-element-Monoid (multiplicative-monoid-Ring R)

is-left-invertible-element-Ring : type-Ring R → UU l
is-left-invertible-element-Ring =
is-left-invertible-element-Monoid (multiplicative-monoid-Ring R)

module _
{l : Level} (R : Ring l) {x : type-Ring R}
where

retraction-is-left-invertible-element-Ring :
is-left-invertible-element-Ring R x → type-Ring R
retraction-is-left-invertible-element-Ring =
retraction-is-left-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-left-inverse-retraction-is-left-invertible-element-Ring :
(H : is-left-invertible-element-Ring R x) →
is-left-inverse-element-Ring R x
( retraction-is-left-invertible-element-Ring H)
is-left-inverse-retraction-is-left-invertible-element-Ring =
is-left-inverse-retraction-is-left-invertible-element-Monoid
( multiplicative-monoid-Ring R)


### Right invertible elements of rings

module _
{l : Level} (R : Ring l)
where

is-right-inverse-element-Ring : (x y : type-Ring R) → UU l
is-right-inverse-element-Ring =
is-right-inverse-element-Monoid (multiplicative-monoid-Ring R)

is-right-invertible-element-Ring : type-Ring R → UU l
is-right-invertible-element-Ring =
is-right-invertible-element-Monoid (multiplicative-monoid-Ring R)

module _
{l : Level} (R : Ring l) {x : type-Ring R}
where

section-is-right-invertible-element-Ring :
is-right-invertible-element-Ring R x → type-Ring R
section-is-right-invertible-element-Ring =
section-is-right-invertible-element-Monoid (multiplicative-monoid-Ring R)

is-right-inverse-section-is-right-invertible-element-Ring :
(H : is-right-invertible-element-Ring R x) →
is-right-inverse-element-Ring R x
( section-is-right-invertible-element-Ring H)
is-right-inverse-section-is-right-invertible-element-Ring =
is-right-inverse-section-is-right-invertible-element-Monoid
( multiplicative-monoid-Ring R)


### Invertible elements of rings

module _
{l : Level} (R : Ring l) (x : type-Ring R)
where

is-inverse-element-Ring : type-Ring R → UU l
is-inverse-element-Ring =
is-inverse-element-Monoid (multiplicative-monoid-Ring R) x

is-invertible-element-Ring : UU l
is-invertible-element-Ring =
is-invertible-element-Monoid (multiplicative-monoid-Ring R) x

module _
{l : Level} (R : Ring l) {x : type-Ring R}
where

inv-is-invertible-element-Ring :
is-invertible-element-Ring R x → type-Ring R
inv-is-invertible-element-Ring =
inv-is-invertible-element-Monoid (multiplicative-monoid-Ring R)

is-right-inverse-inv-is-invertible-element-Ring :
(H : is-invertible-element-Ring R x) →
is-right-inverse-element-Ring R x (inv-is-invertible-element-Ring H)
is-right-inverse-inv-is-invertible-element-Ring =
is-right-inverse-inv-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-left-inverse-inv-is-invertible-element-Ring :
(H : is-invertible-element-Ring R x) →
is-left-inverse-element-Ring R x (inv-is-invertible-element-Ring H)
is-left-inverse-inv-is-invertible-element-Ring =
is-left-inverse-inv-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)


## Properties

### Being an invertible element is a property

module _
{l : Level} (R : Ring l)
where

is-prop-is-invertible-element-Ring :
(x : type-Ring R) → is-prop (is-invertible-element-Ring R x)
is-prop-is-invertible-element-Ring =
is-prop-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-invertible-element-prop-Ring : type-Ring R → Prop l
is-invertible-element-prop-Ring =
is-invertible-element-prop-Monoid
( multiplicative-monoid-Ring R)


### Inverses are left/right inverses

module _
{l : Level} (R : Ring l)
where

is-left-invertible-is-invertible-element-Ring :
(x : type-Ring R) →
is-invertible-element-Ring R x → is-left-invertible-element-Ring R x
is-left-invertible-is-invertible-element-Ring =
is-left-invertible-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-right-invertible-is-invertible-element-Ring :
(x : type-Ring R) →
is-invertible-element-Ring R x → is-right-invertible-element-Ring R x
is-right-invertible-is-invertible-element-Ring =
is-right-invertible-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)


### The inverse invertible element

module _
{l : Level} (R : Ring l)
where

is-right-invertible-left-inverse-Ring :
(x : type-Ring R) (H : is-left-invertible-element-Ring R x) →
is-right-invertible-element-Ring R
( retraction-is-left-invertible-element-Ring R H)
is-right-invertible-left-inverse-Ring =
is-right-invertible-left-inverse-Monoid
( multiplicative-monoid-Ring R)

is-left-invertible-right-inverse-Ring :
(x : type-Ring R) (H : is-right-invertible-element-Ring R x) →
is-left-invertible-element-Ring R
( section-is-right-invertible-element-Ring R H)
is-left-invertible-right-inverse-Ring =
is-left-invertible-right-inverse-Monoid
( multiplicative-monoid-Ring R)

is-invertible-element-inverse-Ring :
(x : type-Ring R) (H : is-invertible-element-Ring R x) →
is-invertible-element-Ring R
( inv-is-invertible-element-Ring R H)
is-invertible-element-inverse-Ring =
is-invertible-element-inverse-Monoid
( multiplicative-monoid-Ring R)


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

module _
{l : Level} (R : Ring l)
where

is-contr-is-right-invertible-element-Ring :
(x : type-Ring R) → is-invertible-element-Ring R x →
is-contr (is-right-invertible-element-Ring R x)
is-contr-is-right-invertible-element-Ring =
is-contr-is-right-invertible-element-Monoid
( multiplicative-monoid-Ring R)


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

module _
{l : Level} (R : Ring l)
where

is-contr-is-left-invertible-Ring :
(x : type-Ring R) → is-invertible-element-Ring R x →
is-contr (is-left-invertible-element-Ring R x)
is-contr-is-left-invertible-Ring =
is-contr-is-left-invertible-Monoid
( multiplicative-monoid-Ring R)


### The unit of a monoid is invertible

module _
{l : Level} (R : Ring l)
where

is-left-invertible-element-one-Ring :
is-left-invertible-element-Ring R (one-Ring R)
is-left-invertible-element-one-Ring =
is-left-invertible-element-unit-Monoid
( multiplicative-monoid-Ring R)

is-right-invertible-element-one-Ring :
is-right-invertible-element-Ring R (one-Ring R)
is-right-invertible-element-one-Ring =
is-right-invertible-element-unit-Monoid
( multiplicative-monoid-Ring R)

is-invertible-element-one-Ring :
is-invertible-element-Ring R (one-Ring R)
is-invertible-element-one-Ring =
is-invertible-element-unit-Monoid
( multiplicative-monoid-Ring R)


### Invertible elements are closed under multiplication

module _
{l : Level} (R : Ring l)
where

is-left-invertible-element-mul-Ring :
(x y : type-Ring R) →
is-left-invertible-element-Ring R x →
is-left-invertible-element-Ring R y →
is-left-invertible-element-Ring R (mul-Ring R x y)
is-left-invertible-element-mul-Ring =
is-left-invertible-element-mul-Monoid
( multiplicative-monoid-Ring R)

is-right-invertible-element-mul-Ring :
(x y : type-Ring R) →
is-right-invertible-element-Ring R x →
is-right-invertible-element-Ring R y →
is-right-invertible-element-Ring R (mul-Ring R x y)
is-right-invertible-element-mul-Ring =
is-right-invertible-element-mul-Monoid
( multiplicative-monoid-Ring R)

is-invertible-element-mul-Ring :
(x y : type-Ring R) →
is-invertible-element-Ring R x →
is-invertible-element-Ring R y →
is-invertible-element-Ring R (mul-Ring R x y)
is-invertible-element-mul-Ring =
is-invertible-element-mul-Monoid
( multiplicative-monoid-Ring R)


### Invertible elements are closed under negatives

module _
{l : Level} (R : Ring l)
where

is-invertible-element-neg-Ring :
(x : type-Ring R) →
is-invertible-element-Ring R x →
is-invertible-element-Ring R (neg-Ring R x)
is-invertible-element-neg-Ring x =
map-Σ _
( neg-Ring R)
( λ y →
map-product
( mul-neg-Ring R x y ∙_)
( mul-neg-Ring R y x ∙_))

is-invertible-element-neg-Ring' :
(x : type-Ring R) →
is-invertible-element-Ring R (neg-Ring R x) →
is-invertible-element-Ring R x
is-invertible-element-neg-Ring' x H =
tr
( is-invertible-element-Ring R)
( neg-neg-Ring R x)
( is-invertible-element-neg-Ring (neg-Ring R x) H)


### The inverse of an invertible element is invertible

module _
{l : Level} (R : Ring l)
where

is-invertible-element-inv-is-invertible-element-Ring :
{x : type-Ring R} (H : is-invertible-element-Ring R x) →
is-invertible-element-Ring R (inv-is-invertible-element-Ring R H)
is-invertible-element-inv-is-invertible-element-Ring =
is-invertible-element-inv-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)


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

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

module _
{l : Level} (R : Ring l) {x : type-Ring R}
where

inv-is-invertible-element-is-equiv-mul-Ring :
is-equiv (mul-Ring R x) → type-Ring R
inv-is-invertible-element-is-equiv-mul-Ring =
inv-is-invertible-element-is-equiv-mul-Monoid
( multiplicative-monoid-Ring R)

is-right-inverse-inv-is-invertible-element-is-equiv-mul-Ring :
(H : is-equiv (mul-Ring R x)) →
mul-Ring R x (inv-is-invertible-element-is-equiv-mul-Ring H) ＝
one-Ring R
is-right-inverse-inv-is-invertible-element-is-equiv-mul-Ring =
is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid
( multiplicative-monoid-Ring R)

is-left-inverse-inv-is-invertible-element-is-equiv-mul-Ring :
(H : is-equiv (mul-Ring R x)) →
mul-Ring R (inv-is-invertible-element-is-equiv-mul-Ring H) x ＝
one-Ring R
is-left-inverse-inv-is-invertible-element-is-equiv-mul-Ring =
is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid
( multiplicative-monoid-Ring R)

is-invertible-element-is-equiv-mul-Ring :
is-equiv (mul-Ring R x) → is-invertible-element-Ring R x
is-invertible-element-is-equiv-mul-Ring =
is-invertible-element-is-equiv-mul-Monoid
( multiplicative-monoid-Ring R)

left-div-is-invertible-element-Ring :
is-invertible-element-Ring R x → type-Ring R → type-Ring R
left-div-is-invertible-element-Ring =
left-div-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-section-left-div-is-invertible-element-Ring :
(H : is-invertible-element-Ring R x) →
mul-Ring R x ∘ left-div-is-invertible-element-Ring H ~ id
is-section-left-div-is-invertible-element-Ring =
is-section-left-div-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-retraction-left-div-is-invertible-element-Ring :
(H : is-invertible-element-Ring R x) →
left-div-is-invertible-element-Ring H ∘ mul-Ring R x ~ id
is-retraction-left-div-is-invertible-element-Ring =
is-retraction-left-div-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-equiv-mul-is-invertible-element-Ring :
is-invertible-element-Ring R x → is-equiv (mul-Ring R x)
is-equiv-mul-is-invertible-element-Ring =
is-equiv-mul-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)


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

module _
{l : Level} (R : Ring l) {x : type-Ring R}
where

inv-is-invertible-element-is-equiv-mul-Ring' :
is-equiv (mul-Ring' R x) → type-Ring R
inv-is-invertible-element-is-equiv-mul-Ring' =
inv-is-invertible-element-is-equiv-mul-Monoid'
( multiplicative-monoid-Ring R)

is-left-inverse-inv-is-invertible-element-is-equiv-mul-Ring' :
(H : is-equiv (mul-Ring' R x)) →
mul-Ring R (inv-is-invertible-element-is-equiv-mul-Ring' H) x ＝
one-Ring R
is-left-inverse-inv-is-invertible-element-is-equiv-mul-Ring' =
is-left-inverse-inv-is-invertible-element-is-equiv-mul-Monoid'
( multiplicative-monoid-Ring R)

is-right-inverse-inv-is-invertible-element-is-equiv-mul-Ring' :
(H : is-equiv (mul-Ring' R x)) →
mul-Ring R x (inv-is-invertible-element-is-equiv-mul-Ring' H) ＝
one-Ring R
is-right-inverse-inv-is-invertible-element-is-equiv-mul-Ring' =
is-right-inverse-inv-is-invertible-element-is-equiv-mul-Monoid'
( multiplicative-monoid-Ring R)

is-invertible-element-is-equiv-mul-Ring' :
is-equiv (mul-Ring' R x) → is-invertible-element-Ring R x
is-invertible-element-is-equiv-mul-Ring' =
is-invertible-element-is-equiv-mul-Monoid'
( multiplicative-monoid-Ring R)

right-div-is-invertible-element-Ring :
is-invertible-element-Ring R x → type-Ring R → type-Ring R
right-div-is-invertible-element-Ring =
right-div-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-section-right-div-is-invertible-element-Ring :
(H : is-invertible-element-Ring R x) →
mul-Ring' R x ∘ right-div-is-invertible-element-Ring H ~ id
is-section-right-div-is-invertible-element-Ring =
is-section-right-div-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-retraction-right-div-is-invertible-element-Ring :
(H : is-invertible-element-Ring R x) →
right-div-is-invertible-element-Ring H ∘ mul-Ring' R x ~ id
is-retraction-right-div-is-invertible-element-Ring =
is-retraction-right-div-is-invertible-element-Monoid
( multiplicative-monoid-Ring R)

is-equiv-mul-is-invertible-element-Ring' :
is-invertible-element-Ring R x → is-equiv (mul-Ring' R x)
is-equiv-mul-is-invertible-element-Ring' =
is-equiv-mul-is-invertible-element-Monoid'
( multiplicative-monoid-Ring R)