The group of multiplicative units of a ring

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-09-21.
Last modified on 2024-03-11.

module ring-theory.groups-of-units-rings where
Imports 
open import category-theory.functors-large-precategories

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

open import group-theory.cores-monoids
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.homomorphisms-monoids
open import group-theory.monoids
open import group-theory.precategory-of-groups
open import group-theory.semigroups
open import group-theory.submonoids

open import ring-theory.homomorphisms-rings
open import ring-theory.invertible-elements-rings
open import ring-theory.precategory-of-rings
open import ring-theory.rings

Idea

The group of units of a ring R is the group consisting of all the invertible elements in R. Equivalently, the group of units of R is the core of the multiplicative monoid of R.

Definitions

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

  subtype-group-of-units-Ring : type-Ring R → Prop l
  subtype-group-of-units-Ring = is-invertible-element-prop-Ring R

  submonoid-group-of-units-Ring : Submonoid l (multiplicative-monoid-Ring R)
  submonoid-group-of-units-Ring =
    submonoid-core-Monoid (multiplicative-monoid-Ring R)

  monoid-group-of-units-Ring : Monoid l
  monoid-group-of-units-Ring =
    monoid-core-Monoid (multiplicative-monoid-Ring R)

  semigroup-group-of-units-Ring : Semigroup l
  semigroup-group-of-units-Ring =
    semigroup-core-Monoid (multiplicative-monoid-Ring R)

  type-group-of-units-Ring : UU l
  type-group-of-units-Ring =
    type-core-Monoid (multiplicative-monoid-Ring R)

  mul-group-of-units-Ring :
    (x y : type-group-of-units-Ring) → type-group-of-units-Ring
  mul-group-of-units-Ring =
    mul-core-Monoid (multiplicative-monoid-Ring R)

  associative-mul-group-of-units-Ring :
    (x y z : type-group-of-units-Ring) →
    mul-group-of-units-Ring (mul-group-of-units-Ring x y) z ＝
    mul-group-of-units-Ring x (mul-group-of-units-Ring y z)
  associative-mul-group-of-units-Ring =
    associative-mul-core-Monoid (multiplicative-monoid-Ring R)

  unit-group-of-units-Ring : type-group-of-units-Ring
  unit-group-of-units-Ring =
    unit-core-Monoid (multiplicative-monoid-Ring R)

  left-unit-law-mul-group-of-units-Ring :
    (x : type-group-of-units-Ring) →
    mul-group-of-units-Ring unit-group-of-units-Ring x ＝ x
  left-unit-law-mul-group-of-units-Ring =
    left-unit-law-mul-core-Monoid (multiplicative-monoid-Ring R)

  right-unit-law-mul-group-of-units-Ring :
    (x : type-group-of-units-Ring) →
    mul-group-of-units-Ring x unit-group-of-units-Ring ＝ x
  right-unit-law-mul-group-of-units-Ring =
    right-unit-law-mul-core-Monoid (multiplicative-monoid-Ring R)

  is-unital-group-of-units-Ring :
    is-unital-Semigroup semigroup-group-of-units-Ring
  is-unital-group-of-units-Ring =
    is-unital-core-Monoid (multiplicative-monoid-Ring R)

  inv-group-of-units-Ring : type-group-of-units-Ring → type-group-of-units-Ring
  inv-group-of-units-Ring =
    inv-core-Monoid (multiplicative-monoid-Ring R)

  left-inverse-law-mul-group-of-units-Ring :
    (x : type-group-of-units-Ring) →
    mul-group-of-units-Ring (inv-group-of-units-Ring x) x ＝
    unit-group-of-units-Ring
  left-inverse-law-mul-group-of-units-Ring =
    left-inverse-law-mul-core-Monoid (multiplicative-monoid-Ring R)

  right-inverse-law-mul-group-of-units-Ring :
    (x : type-group-of-units-Ring) →
    mul-group-of-units-Ring x (inv-group-of-units-Ring x) ＝
    unit-group-of-units-Ring
  right-inverse-law-mul-group-of-units-Ring =
    right-inverse-law-mul-core-Monoid (multiplicative-monoid-Ring R)

  is-group-group-of-units-Ring' :
    is-group-is-unital-Semigroup
      ( semigroup-group-of-units-Ring)
      ( is-unital-group-of-units-Ring)
  is-group-group-of-units-Ring' =
    is-group-core-Monoid' (multiplicative-monoid-Ring R)

  is-group-group-of-units-Ring :
    is-group-Semigroup semigroup-group-of-units-Ring
  is-group-group-of-units-Ring =
    is-group-core-Monoid (multiplicative-monoid-Ring R)

  group-of-units-Ring : Group l
  group-of-units-Ring = core-Monoid (multiplicative-monoid-Ring R)

  inclusion-group-of-units-Ring :
    type-group-of-units-Ring → type-Ring R
  inclusion-group-of-units-Ring =
    inclusion-core-Monoid (multiplicative-monoid-Ring R)

  preserves-mul-inclusion-group-of-units-Ring :
    {x y : type-group-of-units-Ring} →
    inclusion-group-of-units-Ring (mul-group-of-units-Ring x y) ＝
    mul-Ring R
      ( inclusion-group-of-units-Ring x)
      ( inclusion-group-of-units-Ring y)
  preserves-mul-inclusion-group-of-units-Ring {x} {y} =
    preserves-mul-inclusion-core-Monoid (multiplicative-monoid-Ring R) {x} {y}

  hom-inclusion-group-of-units-Ring :
    hom-Monoid monoid-group-of-units-Ring (multiplicative-monoid-Ring R)
  hom-inclusion-group-of-units-Ring =
    hom-inclusion-core-Monoid (multiplicative-monoid-Ring R)

Properties

The group of units of a ring is a functor from rings to groups

The functorial action of group-of-units-Ring

module _
  {l1 l2 : Level} (R : Ring l1) (S : Ring l2) (f : hom-Ring R S)
  where

  map-group-of-units-hom-Ring :
    type-group-of-units-Ring R → type-group-of-units-Ring S
  map-group-of-units-hom-Ring =
    map-core-hom-Monoid
      ( multiplicative-monoid-Ring R)
      ( multiplicative-monoid-Ring S)
      ( hom-multiplicative-monoid-hom-Ring R S f)

  preserves-mul-hom-group-of-units-hom-Ring :
    {x y : type-group-of-units-Ring R} →
    map-group-of-units-hom-Ring (mul-group-of-units-Ring R x y) ＝
    mul-group-of-units-Ring S
      ( map-group-of-units-hom-Ring x)
      ( map-group-of-units-hom-Ring y)
  preserves-mul-hom-group-of-units-hom-Ring =
    preserves-mul-hom-core-hom-Monoid
      ( multiplicative-monoid-Ring R)
      ( multiplicative-monoid-Ring S)
      ( hom-multiplicative-monoid-hom-Ring R S f)

  hom-group-of-units-hom-Ring :
    hom-Group (group-of-units-Ring R) (group-of-units-Ring S)
  hom-group-of-units-hom-Ring =
    hom-core-hom-Monoid
      ( multiplicative-monoid-Ring R)
      ( multiplicative-monoid-Ring S)
      ( hom-multiplicative-monoid-hom-Ring R S f)

  preserves-unit-hom-group-of-units-hom-Ring :
    map-group-of-units-hom-Ring (unit-group-of-units-Ring R) ＝
    unit-group-of-units-Ring S
  preserves-unit-hom-group-of-units-hom-Ring =
    preserves-unit-hom-core-hom-Monoid
      ( multiplicative-monoid-Ring R)
      ( multiplicative-monoid-Ring S)
      ( hom-multiplicative-monoid-hom-Ring R S f)

  preserves-inv-hom-group-of-units-hom-Ring :
    {x : type-group-of-units-Ring R} →
    map-group-of-units-hom-Ring (inv-group-of-units-Ring R x) ＝
    inv-group-of-units-Ring S (map-group-of-units-hom-Ring x)
  preserves-inv-hom-group-of-units-hom-Ring =
    preserves-inv-hom-core-hom-Monoid
      ( multiplicative-monoid-Ring R)
      ( multiplicative-monoid-Ring S)
      ( hom-multiplicative-monoid-hom-Ring R S f)

The functorial laws of group-of-units-Ring

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

  preserves-id-hom-group-of-units-hom-Ring :
    hom-group-of-units-hom-Ring R R (id-hom-Ring R) ＝
    id-hom-Group (group-of-units-Ring R)
  preserves-id-hom-group-of-units-hom-Ring =
    preserves-id-hom-core-hom-Monoid (multiplicative-monoid-Ring R)

module _
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3)
  where

  preserves-comp-hom-group-of-units-hom-Ring :
    (g : hom-Ring S T) (f : hom-Ring R S) →
    hom-group-of-units-hom-Ring R T (comp-hom-Ring R S T g f) ＝
    comp-hom-Group
      ( group-of-units-Ring R)
      ( group-of-units-Ring S)
      ( group-of-units-Ring T)
      ( hom-group-of-units-hom-Ring S T g)
      ( hom-group-of-units-hom-Ring R S f)
  preserves-comp-hom-group-of-units-hom-Ring g f =
    preserves-comp-hom-core-hom-Monoid
      ( multiplicative-monoid-Ring R)
      ( multiplicative-monoid-Ring S)
      ( multiplicative-monoid-Ring T)
      ( hom-multiplicative-monoid-hom-Ring S T g)
      ( hom-multiplicative-monoid-hom-Ring R S f)

The functor group-of-units-Ring

group-of-units-ring-functor-Large-Precategory :
  functor-Large-Precategory
    ( λ l → l)
    ( Ring-Large-Precategory)
    ( Group-Large-Precategory)
obj-functor-Large-Precategory
  group-of-units-ring-functor-Large-Precategory =
  group-of-units-Ring
hom-functor-Large-Precategory
  group-of-units-ring-functor-Large-Precategory {X = R} {Y = S} =
  hom-group-of-units-hom-Ring R S
preserves-comp-functor-Large-Precategory
  group-of-units-ring-functor-Large-Precategory {X = R} {Y = S} {Z = T} =
  preserves-comp-hom-group-of-units-hom-Ring R S T
preserves-id-functor-Large-Precategory
  group-of-units-ring-functor-Large-Precategory {X = R} =
  preserves-id-hom-group-of-units-hom-Ring R

Recent changes