Invertible elements in commutative rings

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

Created on 2022-05-27.
Last modified on 2023-05-04.

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

open import foundation.propositions
open import foundation.universe-levels

open import ring-theory.invertible-elements-rings

Idea

Invertible elements are elements that have a two-sided multiplicative inverse. Such elements are also called the units of the Ring. The set of units of any ring forms a group.

Definition

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

  has-left-inverse-Commutative-Ring : type-Commutative-Ring A → UU l
  has-left-inverse-Commutative-Ring =
    has-left-inverse-Ring (ring-Commutative-Ring A)

  has-right-inverse-Commutative-Ring : type-Commutative-Ring A → UU l
  has-right-inverse-Commutative-Ring =
    has-right-inverse-Ring (ring-Commutative-Ring A)

  has-two-sided-inverse-Commutative-Ring : type-Commutative-Ring A → UU l
  has-two-sided-inverse-Commutative-Ring =
    has-two-sided-inverse-Ring (ring-Commutative-Ring A)

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

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

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

Recent changes