The group of multiplicative units of a commutative ring

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

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

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

open import commutative-algebra.commutative-rings
open import commutative-algebra.homomorphisms-commutative-rings
open import commutative-algebra.precategory-of-commutative-rings

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

open import group-theory.abelian-groups
open import group-theory.category-of-abelian-groups
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.semigroups
open import group-theory.submonoids

open import ring-theory.groups-of-units-rings

Idea

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

Definitions

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

  subtype-group-of-units-Commutative-Ring :
    type-Commutative-Ring A → Prop l
  subtype-group-of-units-Commutative-Ring =
    subtype-group-of-units-Ring (ring-Commutative-Ring A)

  submonoid-group-of-units-Commutative-Ring :
    Submonoid l (multiplicative-monoid-Commutative-Ring A)
  submonoid-group-of-units-Commutative-Ring =
    submonoid-group-of-units-Ring (ring-Commutative-Ring A)

  monoid-group-of-units-Commutative-Ring : Monoid l
  monoid-group-of-units-Commutative-Ring =
    monoid-group-of-units-Ring (ring-Commutative-Ring A)

  semigroup-group-of-units-Commutative-Ring : Semigroup l
  semigroup-group-of-units-Commutative-Ring =
    semigroup-group-of-units-Ring (ring-Commutative-Ring A)

  type-group-of-units-Commutative-Ring : UU l
  type-group-of-units-Commutative-Ring =
    type-group-of-units-Ring (ring-Commutative-Ring A)

  mul-group-of-units-Commutative-Ring :
    (x y : type-group-of-units-Commutative-Ring) →
    type-group-of-units-Commutative-Ring
  mul-group-of-units-Commutative-Ring =
    mul-group-of-units-Ring (ring-Commutative-Ring A)

  associative-mul-group-of-units-Commutative-Ring :
    (x y z : type-group-of-units-Commutative-Ring) →
    mul-group-of-units-Commutative-Ring
      ( mul-group-of-units-Commutative-Ring x y)
      ( z) ＝
    mul-group-of-units-Commutative-Ring x
      ( mul-group-of-units-Commutative-Ring y z)
  associative-mul-group-of-units-Commutative-Ring =
    associative-mul-group-of-units-Ring (ring-Commutative-Ring A)

  unit-group-of-units-Commutative-Ring :
    type-group-of-units-Commutative-Ring
  unit-group-of-units-Commutative-Ring =
    unit-group-of-units-Ring (ring-Commutative-Ring A)

  left-unit-law-mul-group-of-units-Commutative-Ring :
    (x : type-group-of-units-Commutative-Ring) →
    mul-group-of-units-Commutative-Ring
      ( unit-group-of-units-Commutative-Ring)
      ( x) ＝
    x
  left-unit-law-mul-group-of-units-Commutative-Ring =
    left-unit-law-mul-group-of-units-Ring (ring-Commutative-Ring A)

  right-unit-law-mul-group-of-units-Commutative-Ring :
    (x : type-group-of-units-Commutative-Ring) →
    mul-group-of-units-Commutative-Ring
      ( x)
      ( unit-group-of-units-Commutative-Ring) ＝
    x
  right-unit-law-mul-group-of-units-Commutative-Ring =
    right-unit-law-mul-group-of-units-Ring (ring-Commutative-Ring A)

  is-unital-group-of-units-Commutative-Ring :
    is-unital-Semigroup semigroup-group-of-units-Commutative-Ring
  is-unital-group-of-units-Commutative-Ring =
    is-unital-group-of-units-Ring (ring-Commutative-Ring A)

  inv-group-of-units-Commutative-Ring :
    type-group-of-units-Commutative-Ring →
    type-group-of-units-Commutative-Ring
  inv-group-of-units-Commutative-Ring =
    inv-group-of-units-Ring (ring-Commutative-Ring A)

  left-inverse-law-mul-group-of-units-Commutative-Ring :
    (x : type-group-of-units-Commutative-Ring) →
    mul-group-of-units-Commutative-Ring
      ( inv-group-of-units-Commutative-Ring x)
      ( x) ＝
    unit-group-of-units-Commutative-Ring
  left-inverse-law-mul-group-of-units-Commutative-Ring =
    left-inverse-law-mul-group-of-units-Ring (ring-Commutative-Ring A)

  right-inverse-law-mul-group-of-units-Commutative-Ring :
    (x : type-group-of-units-Commutative-Ring) →
    mul-group-of-units-Commutative-Ring
      ( x)
      ( inv-group-of-units-Commutative-Ring x) ＝
    unit-group-of-units-Commutative-Ring
  right-inverse-law-mul-group-of-units-Commutative-Ring =
    right-inverse-law-mul-group-of-units-Ring
      ( ring-Commutative-Ring A)

  commutative-mul-group-of-units-Commutative-Ring :
    (x y : type-group-of-units-Commutative-Ring) →
    mul-group-of-units-Commutative-Ring x y ＝
    mul-group-of-units-Commutative-Ring y x
  commutative-mul-group-of-units-Commutative-Ring x y =
    eq-type-subtype
      ( subtype-group-of-units-Commutative-Ring)
      ( commutative-mul-Commutative-Ring A (pr1 x) (pr1 y))

  is-group-group-of-units-Commutative-Ring' :
    is-group-is-unital-Semigroup
      ( semigroup-group-of-units-Commutative-Ring)
      ( is-unital-group-of-units-Commutative-Ring)
  is-group-group-of-units-Commutative-Ring' =
    is-group-group-of-units-Ring' (ring-Commutative-Ring A)

  is-group-group-of-units-Commutative-Ring :
    is-group-Semigroup semigroup-group-of-units-Commutative-Ring
  is-group-group-of-units-Commutative-Ring =
    is-group-group-of-units-Ring (ring-Commutative-Ring A)

  group-of-units-Commutative-Ring : Group l
  group-of-units-Commutative-Ring =
    group-of-units-Ring (ring-Commutative-Ring A)

  abelian-group-of-units-Commutative-Ring : Ab l
  pr1 abelian-group-of-units-Commutative-Ring =
    group-of-units-Commutative-Ring
  pr2 abelian-group-of-units-Commutative-Ring =
    commutative-mul-group-of-units-Commutative-Ring

  inclusion-group-of-units-Commutative-Ring :
    type-group-of-units-Commutative-Ring → type-Commutative-Ring A
  inclusion-group-of-units-Commutative-Ring =
    inclusion-group-of-units-Ring (ring-Commutative-Ring A)

  preserves-mul-inclusion-group-of-units-Commutative-Ring :
    {x y : type-group-of-units-Commutative-Ring} →
    inclusion-group-of-units-Commutative-Ring
      ( mul-group-of-units-Commutative-Ring x y) ＝
    mul-Commutative-Ring A
      ( inclusion-group-of-units-Commutative-Ring x)
      ( inclusion-group-of-units-Commutative-Ring y)
  preserves-mul-inclusion-group-of-units-Commutative-Ring {x} {y} =
    preserves-mul-inclusion-group-of-units-Ring
      ( ring-Commutative-Ring A)
      { x}
      { y}

  hom-inclusion-group-of-units-Commutative-Ring :
    hom-Monoid monoid-group-of-units-Commutative-Ring
      ( multiplicative-monoid-Commutative-Ring A)
  hom-inclusion-group-of-units-Commutative-Ring =
    hom-inclusion-group-of-units-Ring (ring-Commutative-Ring A)

Properties

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

The functorial action of group-of-units-Commutative-Ring

module _
  {l1 l2 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2)
  (f : hom-Commutative-Ring A B)
  where

  map-group-of-units-hom-Commutative-Ring :
    type-group-of-units-Commutative-Ring A →
    type-group-of-units-Commutative-Ring B
  map-group-of-units-hom-Commutative-Ring =
    map-group-of-units-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  preserves-mul-hom-group-of-units-hom-Commutative-Ring :
    {x y : type-group-of-units-Commutative-Ring A} →
    map-group-of-units-hom-Commutative-Ring
      ( mul-group-of-units-Commutative-Ring A x y) ＝
    mul-group-of-units-Commutative-Ring B
      ( map-group-of-units-hom-Commutative-Ring x)
      ( map-group-of-units-hom-Commutative-Ring y)
  preserves-mul-hom-group-of-units-hom-Commutative-Ring =
    preserves-mul-hom-group-of-units-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  hom-group-of-units-hom-Commutative-Ring :
    hom-Group
      ( group-of-units-Commutative-Ring A)
      ( group-of-units-Commutative-Ring B)
  hom-group-of-units-hom-Commutative-Ring =
    hom-group-of-units-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  preserves-unit-hom-group-of-units-hom-Commutative-Ring :
    map-group-of-units-hom-Commutative-Ring
      ( unit-group-of-units-Commutative-Ring A) ＝
    unit-group-of-units-Commutative-Ring B
  preserves-unit-hom-group-of-units-hom-Commutative-Ring =
    preserves-unit-hom-group-of-units-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  preserves-inv-hom-group-of-units-hom-Commutative-Ring :
    {x : type-group-of-units-Commutative-Ring A} →
    map-group-of-units-hom-Commutative-Ring
      ( inv-group-of-units-Commutative-Ring A x) ＝
    inv-group-of-units-Commutative-Ring B
      ( map-group-of-units-hom-Commutative-Ring x)
  preserves-inv-hom-group-of-units-hom-Commutative-Ring =
    preserves-inv-hom-group-of-units-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

The functorial laws of group-of-units-Commutative-Ring

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

  preserves-id-hom-group-of-units-hom-Commutative-Ring :
    hom-group-of-units-hom-Commutative-Ring A A (id-hom-Commutative-Ring A) ＝
    id-hom-Group (group-of-units-Commutative-Ring A)
  preserves-id-hom-group-of-units-hom-Commutative-Ring =
    preserves-id-hom-group-of-units-hom-Ring (ring-Commutative-Ring A)

module _
  {l1 l2 l3 : Level}
  (A : Commutative-Ring l1) (B : Commutative-Ring l2) (C : Commutative-Ring l3)
  where

  preserves-comp-hom-group-of-units-hom-Commutative-Ring :
    (g : hom-Commutative-Ring B C) (f : hom-Commutative-Ring A B) →
    hom-group-of-units-hom-Commutative-Ring A C
      ( comp-hom-Commutative-Ring A B C g f) ＝
    comp-hom-Group
      ( group-of-units-Commutative-Ring A)
      ( group-of-units-Commutative-Ring B)
      ( group-of-units-Commutative-Ring C)
      ( hom-group-of-units-hom-Commutative-Ring B C g)
      ( hom-group-of-units-hom-Commutative-Ring A B f)
  preserves-comp-hom-group-of-units-hom-Commutative-Ring g f =
    preserves-comp-hom-group-of-units-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( ring-Commutative-Ring C)
      ( g)
      ( f)

The functor group-of-units-Commutative-Ring

group-of-units-commutative-ring-functor-Large-Precategory :
  functor-Large-Precategory (λ l → l)
    ( Commutative-Ring-Large-Precategory)
    ( Ab-Large-Precategory)
obj-functor-Large-Precategory
  group-of-units-commutative-ring-functor-Large-Precategory =
  abelian-group-of-units-Commutative-Ring
hom-functor-Large-Precategory
  group-of-units-commutative-ring-functor-Large-Precategory {X = A} {Y = B} =
  hom-group-of-units-hom-Commutative-Ring A B
preserves-comp-functor-Large-Precategory
  group-of-units-commutative-ring-functor-Large-Precategory
  {X = A}
  {Y = B}
  {Z = C} =
  preserves-comp-hom-group-of-units-hom-Commutative-Ring A B C
preserves-id-functor-Large-Precategory
  group-of-units-commutative-ring-functor-Large-Precategory {X = A} =
  preserves-id-hom-group-of-units-hom-Commutative-Ring A

Recent changes