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)

See also

Recent changes