# Isomorphisms of rings

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

Created on 2022-03-20.

module ring-theory.isomorphisms-rings where

Imports
open import category-theory.isomorphisms-in-large-precategories

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.implicit-function-types
open import foundation.iterated-dependent-product-types
open import foundation.multivariable-homotopies
open import foundation.propositions
open import foundation.structure-identity-principle
open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import group-theory.homomorphisms-abelian-groups
open import group-theory.homomorphisms-monoids
open import group-theory.isomorphisms-abelian-groups
open import group-theory.isomorphisms-monoids

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


## Definition

### The predicate of being an isomorphism of rings

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

is-iso-prop-Ring : Prop (l1 ⊔ l2)
is-iso-prop-Ring =
is-iso-prop-Large-Precategory Ring-Large-Precategory {X = R} {Y = S} f

is-iso-Ring : UU (l1 ⊔ l2)
is-iso-Ring =
is-iso-Large-Precategory Ring-Large-Precategory {X = R} {Y = S} f

is-prop-is-iso-Ring : is-prop is-iso-Ring
is-prop-is-iso-Ring =
is-prop-is-iso-Large-Precategory
( Ring-Large-Precategory)
{ X = R}
{ Y = S}
( f)

hom-inv-is-iso-Ring : is-iso-Ring → hom-Ring S R
hom-inv-is-iso-Ring =
hom-inv-is-iso-Large-Precategory
( Ring-Large-Precategory)
{ X = R}
{ Y = S}
( f)

is-section-hom-inv-is-iso-Ring :
(U : is-iso-Ring) →
comp-hom-Ring S R S f (hom-inv-is-iso-Ring U) ＝ id-hom-Ring S
is-section-hom-inv-is-iso-Ring =
is-section-hom-inv-is-iso-Large-Precategory
( Ring-Large-Precategory)
{ X = R}
{ Y = S}
( f)

is-retraction-hom-inv-is-iso-Ring :
(U : is-iso-Ring) →
comp-hom-Ring R S R (hom-inv-is-iso-Ring U) f ＝ id-hom-Ring R
is-retraction-hom-inv-is-iso-Ring =
is-retraction-hom-inv-is-iso-Large-Precategory
( Ring-Large-Precategory)
{ X = R}
{ Y = S}
( f)

map-inv-is-iso-Ring : is-iso-Ring → type-Ring S → type-Ring R
map-inv-is-iso-Ring U =
map-hom-Ring S R (hom-inv-is-iso-Ring U)

is-section-map-inv-is-iso-Ring :
(U : is-iso-Ring) → map-hom-Ring R S f ∘ map-inv-is-iso-Ring U ~ id
is-section-map-inv-is-iso-Ring U =
htpy-eq-hom-Ring S S
( comp-hom-Ring S R S f (hom-inv-is-iso-Ring U))
( id-hom-Ring S)
( is-section-hom-inv-is-iso-Ring U)

is-retraction-map-inv-is-iso-Ring :
(U : is-iso-Ring) → map-inv-is-iso-Ring U ∘ map-hom-Ring R S f ~ id
is-retraction-map-inv-is-iso-Ring U =
htpy-eq-hom-Ring R R
( comp-hom-Ring R S R (hom-inv-is-iso-Ring U) f)
( id-hom-Ring R)
( is-retraction-hom-inv-is-iso-Ring U)


### Isomorphisms of rings

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

iso-Ring : UU (l1 ⊔ l2)
iso-Ring = iso-Large-Precategory Ring-Large-Precategory R S

hom-iso-Ring : iso-Ring → hom-Ring R S
hom-iso-Ring =
hom-iso-Large-Precategory Ring-Large-Precategory {X = R} {Y = S}

map-iso-Ring : iso-Ring → type-Ring R → type-Ring S
map-iso-Ring f = map-hom-Ring R S (hom-iso-Ring f)

preserves-zero-iso-Ring :
(f : iso-Ring) → map-iso-Ring f (zero-Ring R) ＝ zero-Ring S
preserves-zero-iso-Ring f = preserves-zero-hom-Ring R S (hom-iso-Ring f)

preserves-one-iso-Ring :
(f : iso-Ring) → map-iso-Ring f (one-Ring R) ＝ one-Ring S
preserves-one-iso-Ring f = preserves-one-hom-Ring R S (hom-iso-Ring f)

(f : iso-Ring) {x y : type-Ring R} →
map-iso-Ring f (add-Ring R x y) ＝
add-Ring S (map-iso-Ring f x) (map-iso-Ring f y)

preserves-neg-iso-Ring :
(f : iso-Ring) {x : type-Ring R} →
map-iso-Ring f (neg-Ring R x) ＝ neg-Ring S (map-iso-Ring f x)
preserves-neg-iso-Ring f = preserves-neg-hom-Ring R S (hom-iso-Ring f)

preserves-mul-iso-Ring :
(f : iso-Ring) {x y : type-Ring R} →
map-iso-Ring f (mul-Ring R x y) ＝
mul-Ring S (map-iso-Ring f x) (map-iso-Ring f y)
preserves-mul-iso-Ring f =
preserves-mul-hom-Ring R S (hom-iso-Ring f)

is-iso-iso-Ring :
(f : iso-Ring) → is-iso-Ring R S (hom-iso-Ring f)
is-iso-iso-Ring =
is-iso-iso-Large-Precategory Ring-Large-Precategory {X = R} {Y = S}

hom-inv-iso-Ring : iso-Ring → hom-Ring S R
hom-inv-iso-Ring =
hom-inv-iso-Large-Precategory Ring-Large-Precategory {X = R} {Y = S}

map-inv-iso-Ring : iso-Ring → type-Ring S → type-Ring R
map-inv-iso-Ring f = map-hom-Ring S R (hom-inv-iso-Ring f)

preserves-zero-inv-iso-Ring :
(f : iso-Ring) → map-inv-iso-Ring f (zero-Ring S) ＝ zero-Ring R
preserves-zero-inv-iso-Ring f =
preserves-zero-hom-Ring S R (hom-inv-iso-Ring f)

preserves-one-inv-iso-Ring :
(f : iso-Ring) → map-inv-iso-Ring f (one-Ring S) ＝ one-Ring R
preserves-one-inv-iso-Ring f =
preserves-one-hom-Ring S R (hom-inv-iso-Ring f)

(f : iso-Ring) {x y : type-Ring S} →
map-inv-iso-Ring f (add-Ring S x y) ＝
add-Ring R (map-inv-iso-Ring f x) (map-inv-iso-Ring f y)

preserves-neg-inv-iso-Ring :
(f : iso-Ring) {x : type-Ring S} →
map-inv-iso-Ring f (neg-Ring S x) ＝ neg-Ring R (map-inv-iso-Ring f x)
preserves-neg-inv-iso-Ring f =
preserves-neg-hom-Ring S R (hom-inv-iso-Ring f)

preserves-mul-inv-iso-Ring :
(f : iso-Ring) {x y : type-Ring S} →
map-inv-iso-Ring f (mul-Ring S x y) ＝
mul-Ring R (map-inv-iso-Ring f x) (map-inv-iso-Ring f y)
preserves-mul-inv-iso-Ring f =
preserves-mul-hom-Ring S R (hom-inv-iso-Ring f)

is-section-hom-inv-iso-Ring :
(f : iso-Ring) →
comp-hom-Ring S R S (hom-iso-Ring f) (hom-inv-iso-Ring f) ＝ id-hom-Ring S
is-section-hom-inv-iso-Ring =
is-section-hom-inv-iso-Large-Precategory
( Ring-Large-Precategory)
{ X = R}
{ Y = S}

is-section-map-inv-iso-Ring :
(f : iso-Ring) → map-iso-Ring f ∘ map-inv-iso-Ring f ~ id
is-section-map-inv-iso-Ring f =
htpy-eq-hom-Ring S S
( comp-hom-Ring S R S (hom-iso-Ring f) (hom-inv-iso-Ring f))
( id-hom-Ring S)
( is-section-hom-inv-iso-Ring f)

is-retraction-hom-inv-iso-Ring :
(f : iso-Ring) →
comp-hom-Ring R S R (hom-inv-iso-Ring f) (hom-iso-Ring f) ＝ id-hom-Ring R
is-retraction-hom-inv-iso-Ring =
is-retraction-hom-inv-iso-Large-Precategory
( Ring-Large-Precategory)
{ X = R}
{ Y = S}

is-retraction-map-inv-iso-Ring :
(f : iso-Ring) → map-inv-iso-Ring f ∘ map-iso-Ring f ~ id
is-retraction-map-inv-iso-Ring f =
htpy-eq-hom-Ring R R
( comp-hom-Ring R S R (hom-inv-iso-Ring f) (hom-iso-Ring f))
( id-hom-Ring R)
( is-retraction-hom-inv-iso-Ring f)

iso-multiplicative-monoid-iso-Ring :
(f : iso-Ring) →
iso-Monoid (multiplicative-monoid-Ring R) (multiplicative-monoid-Ring S)
pr1 (iso-multiplicative-monoid-iso-Ring f) =
hom-multiplicative-monoid-hom-Ring R S (hom-iso-Ring f)
pr1 (pr2 (iso-multiplicative-monoid-iso-Ring f)) =
hom-multiplicative-monoid-hom-Ring S R (hom-inv-iso-Ring f)
pr1 (pr2 (pr2 (iso-multiplicative-monoid-iso-Ring f))) =
eq-htpy-hom-Monoid
( multiplicative-monoid-Ring S)
( multiplicative-monoid-Ring S)
( comp-hom-Monoid
( multiplicative-monoid-Ring S)
( multiplicative-monoid-Ring R)
( multiplicative-monoid-Ring S)
( hom-multiplicative-monoid-hom-Ring R S (hom-iso-Ring f))
( hom-multiplicative-monoid-hom-Ring S R (hom-inv-iso-Ring f)))
( id-hom-Monoid (multiplicative-monoid-Ring S))
( is-section-map-inv-iso-Ring f)
pr2 (pr2 (pr2 (iso-multiplicative-monoid-iso-Ring f))) =
eq-htpy-hom-Monoid
( multiplicative-monoid-Ring R)
( multiplicative-monoid-Ring R)
( comp-hom-Monoid
( multiplicative-monoid-Ring R)
( multiplicative-monoid-Ring S)
( multiplicative-monoid-Ring R)
( hom-multiplicative-monoid-hom-Ring S R (hom-inv-iso-Ring f))
( hom-multiplicative-monoid-hom-Ring R S (hom-iso-Ring f)))
( id-hom-Monoid (multiplicative-monoid-Ring R))
( is-retraction-map-inv-iso-Ring f)


### The identity isomorphism of rings

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

is-iso-id-hom-Ring : is-iso-Ring R R (id-hom-Ring R)
is-iso-id-hom-Ring =
is-iso-id-hom-Large-Precategory Ring-Large-Precategory {X = R}

id-iso-Ring : iso-Ring R R
pr1 id-iso-Ring = id-hom-Ring R
pr2 id-iso-Ring = is-iso-id-hom-Ring


### Converting identifications of rings to isomorphisms of rings

iso-eq-Ring :
{ l : Level} (R S : Ring l) → R ＝ S → iso-Ring R S
iso-eq-Ring R S = iso-eq-Large-Precategory Ring-Large-Precategory R S


## Properties

### A ring homomorphism is an isomorphism if and only if the underlying homomorphism of abelian groups is an isomorphism

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

iso-ab-Ring : UU (l1 ⊔ l2)
iso-ab-Ring =
Σ ( iso-Ab (ab-Ring R) (ab-Ring S))
( λ f →
is-ring-homomorphism-hom-Ab R S
( hom-iso-Ab (ab-Ring R) (ab-Ring S) f))

iso-ab-iso-ab-Ring :
iso-ab-Ring → iso-Ab (ab-Ring R) (ab-Ring S)
iso-ab-iso-ab-Ring = pr1

is-iso-ab-hom-Ring : hom-Ring R S → UU (l1 ⊔ l2)
is-iso-ab-hom-Ring f =
is-iso-Ab (ab-Ring R) (ab-Ring S) (hom-ab-hom-Ring R S f)

is-iso-ab-is-iso-Ring :
(f : hom-Ring R S) →
is-iso-Ring R S f → is-iso-ab-hom-Ring f
pr1 (is-iso-ab-is-iso-Ring f U) =
hom-ab-hom-Ring S R (hom-inv-is-iso-Ring R S f U)
pr1 (pr2 (is-iso-ab-is-iso-Ring f U)) =
ap
( hom-ab-hom-Ring S S)
( is-section-hom-inv-is-iso-Ring R S f U)
pr2 (pr2 (is-iso-ab-is-iso-Ring f U)) =
ap
( hom-ab-hom-Ring R R)
( is-retraction-hom-inv-is-iso-Ring R S f U)

abstract
preserves-mul-inv-is-iso-Ab :
(f : hom-Ab (ab-Ring R) (ab-Ring S)) →
(U : is-iso-Ab (ab-Ring R) (ab-Ring S) f) →
preserves-mul-hom-Ab R S f →
preserves-mul-hom-Ab S R
( hom-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U)
preserves-mul-inv-is-iso-Ab f U μ {x} {y} =
( inv
( ap
( map-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U)
( ( μ) ∙
( ap-mul-Ring S
( is-section-map-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U x)
( is-section-map-inv-is-iso-Ab
( ab-Ring R)
( ab-Ring S)
( f)
( U)
( y)))))) ∙
( is-retraction-map-inv-is-iso-Ab
( ab-Ring R)
( ab-Ring S)
( f)
( U)
( mul-Ring R
( map-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U x)
( map-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U y)))

preserves-unit-inv-is-iso-Ab :
(f : hom-Ab (ab-Ring R) (ab-Ring S)) →
(U : is-iso-Ab (ab-Ring R) (ab-Ring S) f) →
preserves-unit-hom-Ab R S f →
preserves-unit-hom-Ab S R
( hom-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U)
preserves-unit-inv-is-iso-Ab f U ν =
( inv (ap (map-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U) ν)) ∙
( is-retraction-map-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U _)

is-ring-homomorphism-inv-is-iso-Ab :
(f : hom-Ab (ab-Ring R) (ab-Ring S)) →
(U : is-iso-Ab (ab-Ring R) (ab-Ring S) f) →
is-ring-homomorphism-hom-Ab R S f →
is-ring-homomorphism-hom-Ab S R
( hom-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) f U)
pr1 (is-ring-homomorphism-inv-is-iso-Ab f U (μ , ν)) =
preserves-mul-inv-is-iso-Ab f U μ
pr2 (is-ring-homomorphism-inv-is-iso-Ab f U (μ , ν)) =
preserves-unit-inv-is-iso-Ab f U ν

inv-hom-ring-is-iso-Ab :
(f : hom-Ring R S) →
is-iso-Ab (ab-Ring R) (ab-Ring S) (hom-ab-hom-Ring R S f) →
hom-Ring S R
pr1 (inv-hom-ring-is-iso-Ab f U) =
hom-inv-is-iso-Ab (ab-Ring R) (ab-Ring S) (hom-ab-hom-Ring R S f) U
pr2 (inv-hom-ring-is-iso-Ab f U) =
is-ring-homomorphism-inv-is-iso-Ab
( hom-ab-hom-Ring R S f)
( U)
( is-ring-homomorphism-hom-Ring R S f)

abstract
is-iso-ring-is-iso-Ab :
(f : hom-Ring R S) →
is-iso-Ab (ab-Ring R) (ab-Ring S) (hom-ab-hom-Ring R S f) →
is-iso-Ring R S f
pr1 (is-iso-ring-is-iso-Ab f U) =
inv-hom-ring-is-iso-Ab f U
pr1 (pr2 (is-iso-ring-is-iso-Ab f U)) =
eq-htpy-hom-Ring S S
( comp-hom-Ring S R S f
( inv-hom-ring-is-iso-Ab f U))
( id-hom-Ring S)
( htpy-eq-hom-Ab (ab-Ring S) (ab-Ring S)
( hom-ab-hom-Ring S S
( comp-hom-Ring S R S f
( inv-hom-ring-is-iso-Ab f U)))
( id-hom-Ab (ab-Ring S))
( is-section-hom-inv-is-iso-Ab
( ab-Ring R)
( ab-Ring S)
( hom-ab-hom-Ring R S f)
( U)))
pr2 (pr2 (is-iso-ring-is-iso-Ab f U)) =
eq-htpy-hom-Ring R R
( comp-hom-Ring R S R
( inv-hom-ring-is-iso-Ab f U)
( f))
( id-hom-Ring R)
( htpy-eq-hom-Ab (ab-Ring R) (ab-Ring R)
( hom-ab-hom-Ring R R
( comp-hom-Ring R S R
( inv-hom-ring-is-iso-Ab f U)
( f)))
( id-hom-Ab (ab-Ring R))
( is-retraction-hom-inv-is-iso-Ab
( ab-Ring R)
( ab-Ring S)
( hom-ab-hom-Ring R S f)
( U)))

iso-ab-iso-Ring :
iso-Ring R S → iso-Ab (ab-Ring R) (ab-Ring S)
pr1 (iso-ab-iso-Ring f) = hom-ab-hom-Ring R S (hom-iso-Ring R S f)
pr2 (iso-ab-iso-Ring f) =
is-iso-ab-is-iso-Ring
( hom-iso-Ring R S f)
( is-iso-iso-Ring R S f)

equiv-iso-ab-iso-Ring : iso-Ring R S ≃ iso-ab-Ring
equiv-iso-ab-iso-Ring =
( inv-equiv
( associative-Σ
( hom-Ab (ab-Ring R) (ab-Ring S))
( is-iso-Ab (ab-Ring R) (ab-Ring S))
( λ f → is-ring-homomorphism-hom-Ab R S (pr1 f)))) ∘e
( equiv-tot (λ f → commutative-product)) ∘e
( associative-Σ
( hom-Ab (ab-Ring R) (ab-Ring S))
( is-ring-homomorphism-hom-Ab R S)
( λ f → is-iso-Ab (ab-Ring R) (ab-Ring S) (pr1 f))) ∘e
( equiv-type-subtype
( is-prop-is-iso-Ring R S)
( λ f → is-prop-is-iso-Ab (ab-Ring R) (ab-Ring S) (hom-ab-hom-Ring R S f))
( is-iso-ab-is-iso-Ring)
( is-iso-ring-is-iso-Ab))


### Characterizing identifications of rings

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

abstract
is-torsorial-iso-Ring : is-torsorial (λ (S : Ring l) → iso-Ring R S)
is-torsorial-iso-Ring =
is-contr-equiv
( Σ (Ring l) (iso-ab-Ring R))
( equiv-tot (equiv-iso-ab-iso-Ring R))
( is-torsorial-Eq-structure
( is-torsorial-iso-Ab (ab-Ring R))
( ab-Ring R , id-iso-Ab (ab-Ring R))
( is-torsorial-Eq-structure
( is-torsorial-Eq-subtype
( is-torsorial-multivariable-implicit-htpy 2 (mul-Ring R))
( λ μ →
is-prop-iterated-Π 3
( λ x y z → is-set-type-Ring R (μ (μ x y) z) (μ x (μ y z))))
( mul-Ring R)
( λ {x} {y} → refl)
( associative-mul-Ring R))
( (mul-Ring R , associative-mul-Ring R) , λ {x} {y} → refl)
( is-torsorial-Eq-subtype
( is-torsorial-Eq-subtype
( is-torsorial-Id (one-Ring R))
( λ x →
is-prop-product
( is-prop-Π (λ y → is-set-type-Ring R (mul-Ring R x y) y))
( is-prop-Π (λ y → is-set-type-Ring R (mul-Ring R y x) y)))
( one-Ring R)
( refl)
( left-unit-law-mul-Ring R , right-unit-law-mul-Ring R))
( λ u →
is-prop-product
( is-prop-iterated-Π 3
( λ x y z →
is-set-type-Ring R
( mul-Ring R x (add-Ring R y z))
( add-Ring R (mul-Ring R x y) (mul-Ring R x z))))
( is-prop-iterated-Π 3
( λ x y z →
is-set-type-Ring R
( mul-Ring R (add-Ring R x y) z)
( add-Ring R (mul-Ring R x z) (mul-Ring R y z)))))
( is-unital-Ring R)
( refl)

is-equiv-iso-eq-Ring :
(S : Ring l) → is-equiv (iso-eq-Ring R S)
is-equiv-iso-eq-Ring =
fundamental-theorem-id
( is-torsorial-iso-Ring)
( iso-eq-Ring R)

extensionality-Ring : (S : Ring l) → (R ＝ S) ≃ iso-Ring R S
pr1 (extensionality-Ring S) = iso-eq-Ring R S
pr2 (extensionality-Ring S) = is-equiv-iso-eq-Ring S

eq-iso-Ring : (S : Ring l) → iso-Ring R S → R ＝ S
eq-iso-Ring S = map-inv-is-equiv (is-equiv-iso-eq-Ring S)


### Any ring isomorphism preserves and reflects invertible elements

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

preserves-invertible-elements-iso-Ring :
{x : type-Ring R} →
is-invertible-element-Ring R x →
is-invertible-element-Ring S (map-iso-Ring R S f x)
preserves-invertible-elements-iso-Ring =
preserves-invertible-elements-iso-Monoid
( multiplicative-monoid-Ring R)
( multiplicative-monoid-Ring S)
( iso-multiplicative-monoid-iso-Ring R S f)

reflects-invertible-elements-iso-Ring :
{x : type-Ring R} →
is-invertible-element-Ring S (map-iso-Ring R S f x) →
is-invertible-element-Ring R x
reflects-invertible-elements-iso-Ring =
reflects-invertible-elements-iso-Monoid
( multiplicative-monoid-Ring R)
( multiplicative-monoid-Ring S)
( iso-multiplicative-monoid-iso-Ring R S f)