Invertible elements in commutative rings

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

Created on 2022-05-27.
Last modified on 2023-09-21.

module commutative-algebra.invertible-elements-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import ring-theory.invertible-elements-rings

Idea

An element of a commutative ring Ais said to be invertible if it has a two-sided inverse. However, since multiplication in commutative rings is commutative, any element is already invertible as soon as it has either a left or a right inverse. The invertible elements of a commutative ring A are also called the (multiplicative) units of A.

The abelian group of multiplicative units is constructed in commutative-algebra.groups-of-units-commutative-rings.

Definitions

Left invertible elements of commutative rings

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-left-inverse-element-Commutative-Ring :
    (x y : type-Commutative-Ring A) → UU l
  is-left-inverse-element-Commutative-Ring =
    is-left-inverse-element-Ring (ring-Commutative-Ring A)

  is-left-invertible-element-Commutative-Ring : type-Commutative-Ring A → UU l
  is-left-invertible-element-Commutative-Ring =
    is-left-invertible-element-Ring (ring-Commutative-Ring A)

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

  retraction-is-left-invertible-element-Commutative-Ring :
    is-left-invertible-element-Commutative-Ring A x → type-Commutative-Ring A
  retraction-is-left-invertible-element-Commutative-Ring =
    retraction-is-left-invertible-element-Ring
      ( ring-Commutative-Ring A)

  is-left-inverse-retraction-is-left-invertible-element-Commutative-Ring :
    (H : is-left-invertible-element-Commutative-Ring A x) →
    is-left-inverse-element-Commutative-Ring A x
      ( retraction-is-left-invertible-element-Commutative-Ring H)
  is-left-inverse-retraction-is-left-invertible-element-Commutative-Ring =
    is-left-inverse-retraction-is-left-invertible-element-Ring
      ( ring-Commutative-Ring A)

Aight invertible elements of commutative rings

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-right-inverse-element-Commutative-Ring :
    (x y : type-Commutative-Ring A) → UU l
  is-right-inverse-element-Commutative-Ring =
    is-right-inverse-element-Ring (ring-Commutative-Ring A)

  is-right-invertible-element-Commutative-Ring : type-Commutative-Ring A → UU l
  is-right-invertible-element-Commutative-Ring =
    is-right-invertible-element-Ring (ring-Commutative-Ring A)

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

  section-is-right-invertible-element-Commutative-Ring :
    is-right-invertible-element-Commutative-Ring A x → type-Commutative-Ring A
  section-is-right-invertible-element-Commutative-Ring =
    section-is-right-invertible-element-Ring (ring-Commutative-Ring A)

  is-right-inverse-section-is-right-invertible-element-Commutative-Ring :
    (H : is-right-invertible-element-Commutative-Ring A x) →
    is-right-inverse-element-Commutative-Ring A x
      ( section-is-right-invertible-element-Commutative-Ring H)
  is-right-inverse-section-is-right-invertible-element-Commutative-Ring =
    is-right-inverse-section-is-right-invertible-element-Ring
      ( ring-Commutative-Ring A)

Invertible elements of commutative rings

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

  is-inverse-element-Commutative-Ring : type-Commutative-Ring A → UU l
  is-inverse-element-Commutative-Ring =
    is-inverse-element-Ring (ring-Commutative-Ring A) x

  is-invertible-element-Commutative-Ring : UU l
  is-invertible-element-Commutative-Ring =
    is-invertible-element-Ring (ring-Commutative-Ring A) x

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

  inv-is-invertible-element-Commutative-Ring :
    is-invertible-element-Commutative-Ring A x → type-Commutative-Ring A
  inv-is-invertible-element-Commutative-Ring =
    inv-is-invertible-element-Ring (ring-Commutative-Ring A)

  is-right-inverse-inv-is-invertible-element-Commutative-Ring :
    (H : is-invertible-element-Commutative-Ring A x) →
    is-right-inverse-element-Commutative-Ring A x
      ( inv-is-invertible-element-Commutative-Ring H)
  is-right-inverse-inv-is-invertible-element-Commutative-Ring =
    is-right-inverse-inv-is-invertible-element-Ring
      ( ring-Commutative-Ring A)

  is-left-inverse-inv-is-invertible-element-Commutative-Ring :
    (H : is-invertible-element-Commutative-Ring A x) →
    is-left-inverse-element-Commutative-Ring A x
      ( inv-is-invertible-element-Commutative-Ring H)
  is-left-inverse-inv-is-invertible-element-Commutative-Ring =
    is-left-inverse-inv-is-invertible-element-Ring
      ( ring-Commutative-Ring A)

  is-invertible-is-left-invertible-element-Commutative-Ring :
    is-left-invertible-element-Commutative-Ring A x →
    is-invertible-element-Commutative-Ring A x
  pr1 (is-invertible-is-left-invertible-element-Commutative-Ring H) =
    retraction-is-left-invertible-element-Commutative-Ring A H
  pr1 (pr2 (is-invertible-is-left-invertible-element-Commutative-Ring H)) =
    commutative-mul-Commutative-Ring A _ _ ∙
    is-left-inverse-retraction-is-left-invertible-element-Commutative-Ring A H
  pr2 (pr2 (is-invertible-is-left-invertible-element-Commutative-Ring H)) =
    is-left-inverse-retraction-is-left-invertible-element-Commutative-Ring A H

  is-invertible-is-right-invertible-element-Commutative-Ring :
    is-right-invertible-element-Commutative-Ring A x →
    is-invertible-element-Commutative-Ring A x
  pr1 (is-invertible-is-right-invertible-element-Commutative-Ring H) =
    section-is-right-invertible-element-Commutative-Ring A H
  pr1 (pr2 (is-invertible-is-right-invertible-element-Commutative-Ring H)) =
    is-right-inverse-section-is-right-invertible-element-Commutative-Ring A H
  pr2 (pr2 (is-invertible-is-right-invertible-element-Commutative-Ring H)) =
    commutative-mul-Commutative-Ring A _ _ ∙
    is-right-inverse-section-is-right-invertible-element-Commutative-Ring A H

Properties

Being an invertible element is a property

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-prop-is-invertible-element-Commutative-Ring :
    (x : type-Commutative-Ring A) →
    is-prop (is-invertible-element-Commutative-Ring A x)
  is-prop-is-invertible-element-Commutative-Ring =
    is-prop-is-invertible-element-Ring (ring-Commutative-Ring A)

  is-invertible-element-prop-Commutative-Ring : type-Commutative-Ring A → Prop l
  is-invertible-element-prop-Commutative-Ring =
    is-invertible-element-prop-Ring (ring-Commutative-Ring A)

Inverses are left/right inverses

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-left-invertible-is-invertible-element-Commutative-Ring :
    (x : type-Commutative-Ring A) →
    is-invertible-element-Commutative-Ring A x →
    is-left-invertible-element-Commutative-Ring A x
  is-left-invertible-is-invertible-element-Commutative-Ring =
    is-left-invertible-is-invertible-element-Ring (ring-Commutative-Ring A)

  is-right-invertible-is-invertible-element-Commutative-Ring :
    (x : type-Commutative-Ring A) →
    is-invertible-element-Commutative-Ring A x →
    is-right-invertible-element-Commutative-Ring A x
  is-right-invertible-is-invertible-element-Commutative-Ring =
    is-right-invertible-is-invertible-element-Ring (ring-Commutative-Ring A)

The inverse invertible element

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-right-invertible-left-inverse-Commutative-Ring :
    (x : type-Commutative-Ring A)
    (H : is-left-invertible-element-Commutative-Ring A x) →
    is-right-invertible-element-Commutative-Ring A
      ( retraction-is-left-invertible-element-Commutative-Ring A H)
  is-right-invertible-left-inverse-Commutative-Ring =
    is-right-invertible-left-inverse-Ring (ring-Commutative-Ring A)

  is-left-invertible-right-inverse-Commutative-Ring :
    (x : type-Commutative-Ring A)
    (H : is-right-invertible-element-Commutative-Ring A x) →
    is-left-invertible-element-Commutative-Ring A
      ( section-is-right-invertible-element-Commutative-Ring A H)
  is-left-invertible-right-inverse-Commutative-Ring =
    is-left-invertible-right-inverse-Ring (ring-Commutative-Ring A)

  is-invertible-element-inverse-Commutative-Ring :
    (x : type-Commutative-Ring A)
    (H : is-invertible-element-Commutative-Ring A x) →
    is-invertible-element-Commutative-Ring A
      ( inv-is-invertible-element-Commutative-Ring A H)
  is-invertible-element-inverse-Commutative-Ring =
    is-invertible-element-inverse-Ring (ring-Commutative-Ring A)

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

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-contr-is-right-invertible-element-Commutative-Ring :
    (x : type-Commutative-Ring A) → is-invertible-element-Commutative-Ring A x →
    is-contr (is-right-invertible-element-Commutative-Ring A x)
  is-contr-is-right-invertible-element-Commutative-Ring =
    is-contr-is-right-invertible-element-Ring (ring-Commutative-Ring A)

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

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-contr-is-left-invertible-Commutative-Ring :
    (x : type-Commutative-Ring A) → is-invertible-element-Commutative-Ring A x →
    is-contr (is-left-invertible-element-Commutative-Ring A x)
  is-contr-is-left-invertible-Commutative-Ring =
    is-contr-is-left-invertible-Ring (ring-Commutative-Ring A)

The unit of a monoid is invertible

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-left-invertible-element-one-Commutative-Ring :
    is-left-invertible-element-Commutative-Ring A (one-Commutative-Ring A)
  is-left-invertible-element-one-Commutative-Ring =
    is-left-invertible-element-one-Ring (ring-Commutative-Ring A)

  is-right-invertible-element-one-Commutative-Ring :
    is-right-invertible-element-Commutative-Ring A (one-Commutative-Ring A)
  is-right-invertible-element-one-Commutative-Ring =
    is-right-invertible-element-one-Ring (ring-Commutative-Ring A)

  is-invertible-element-one-Commutative-Ring :
    is-invertible-element-Commutative-Ring A (one-Commutative-Ring A)
  is-invertible-element-one-Commutative-Ring =
    is-invertible-element-one-Ring (ring-Commutative-Ring A)

Invertible elements are closed under multiplication

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-left-invertible-element-mul-Commutative-Ring :
    (x y : type-Commutative-Ring A) →
    is-left-invertible-element-Commutative-Ring A x →
    is-left-invertible-element-Commutative-Ring A y →
    is-left-invertible-element-Commutative-Ring A (mul-Commutative-Ring A x y)
  is-left-invertible-element-mul-Commutative-Ring =
    is-left-invertible-element-mul-Ring (ring-Commutative-Ring A)

  is-right-invertible-element-mul-Commutative-Ring :
    (x y : type-Commutative-Ring A) →
    is-right-invertible-element-Commutative-Ring A x →
    is-right-invertible-element-Commutative-Ring A y →
    is-right-invertible-element-Commutative-Ring A (mul-Commutative-Ring A x y)
  is-right-invertible-element-mul-Commutative-Ring =
    is-right-invertible-element-mul-Ring (ring-Commutative-Ring A)

  is-invertible-element-mul-Commutative-Ring :
    (x y : type-Commutative-Ring A) →
    is-invertible-element-Commutative-Ring A x →
    is-invertible-element-Commutative-Ring A y →
    is-invertible-element-Commutative-Ring A (mul-Commutative-Ring A x y)
  is-invertible-element-mul-Commutative-Ring =
    is-invertible-element-mul-Ring (ring-Commutative-Ring A)

The inverse of an invertible element is invertible

module _
  {l : Level} (A : Commutative-Ring l)
  where

  is-invertible-element-inv-is-invertible-element-Commutative-Ring :
    {x : type-Commutative-Ring A}
    (H : is-invertible-element-Commutative-Ring A x) →
    is-invertible-element-Commutative-Ring A
      ( inv-is-invertible-element-Commutative-Ring A H)
  is-invertible-element-inv-is-invertible-element-Commutative-Ring =
    is-invertible-element-inv-is-invertible-element-Ring
      ( ring-Commutative-Ring A)

See also

Recent changes