# Isomorphisms of commutative rings

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

Created on 2022-04-22.

module commutative-algebra.isomorphisms-commutative-rings where

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

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

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import group-theory.isomorphisms-abelian-groups

open import ring-theory.isomorphisms-rings


## Idea

An isomorphism of commutative rings is an invertible homomorphism of commutative rings.

## Definitions

### The predicate of being an isomorphism of rings

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

is-iso-prop-Commutative-Ring : Prop (l1 ⊔ l2)
is-iso-prop-Commutative-Ring =
is-iso-prop-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)
( f)

is-iso-Commutative-Ring : UU (l1 ⊔ l2)
is-iso-Commutative-Ring =
is-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)
( f)

is-prop-is-iso-Commutative-Ring : is-prop is-iso-Commutative-Ring
is-prop-is-iso-Commutative-Ring =
is-prop-is-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)
( f)

hom-inv-is-iso-Commutative-Ring :
is-iso-Commutative-Ring → hom-Commutative-Ring B A
hom-inv-is-iso-Commutative-Ring =
hom-inv-is-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)
( f)

is-section-hom-inv-is-iso-Commutative-Ring :
(U : is-iso-Commutative-Ring) →
comp-hom-Commutative-Ring B A B f (hom-inv-is-iso-Commutative-Ring U) ＝
id-hom-Commutative-Ring B
is-section-hom-inv-is-iso-Commutative-Ring =
is-section-hom-inv-is-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)
( f)

is-retraction-hom-inv-is-iso-Commutative-Ring :
(U : is-iso-Commutative-Ring) →
comp-hom-Commutative-Ring A B A (hom-inv-is-iso-Commutative-Ring U) f ＝
id-hom-Commutative-Ring A
is-retraction-hom-inv-is-iso-Commutative-Ring =
is-retraction-hom-inv-is-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)
( f)

map-inv-is-iso-Commutative-Ring :
is-iso-Commutative-Ring →
type-Commutative-Ring B → type-Commutative-Ring A
map-inv-is-iso-Commutative-Ring U =
map-hom-Commutative-Ring B A (hom-inv-is-iso-Commutative-Ring U)

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

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


### Isomorphisms of commutative rings

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

iso-Commutative-Ring : UU (l1 ⊔ l2)
iso-Commutative-Ring =
iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

hom-iso-Commutative-Ring :
iso-Commutative-Ring → hom-Commutative-Ring A B
hom-iso-Commutative-Ring =
hom-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

map-iso-Commutative-Ring :
iso-Commutative-Ring → type-Commutative-Ring A → type-Commutative-Ring B
map-iso-Commutative-Ring =
map-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

preserves-zero-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
map-iso-Commutative-Ring f (zero-Commutative-Ring A) ＝
zero-Commutative-Ring B
preserves-zero-iso-Commutative-Ring =
preserves-zero-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

preserves-one-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
map-iso-Commutative-Ring f (one-Commutative-Ring A) ＝
one-Commutative-Ring B
preserves-one-iso-Commutative-Ring =
preserves-one-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

(f : iso-Commutative-Ring) {x y : type-Commutative-Ring A} →
map-iso-Commutative-Ring f (add-Commutative-Ring A x y) ＝
( map-iso-Commutative-Ring f x)
( map-iso-Commutative-Ring f y)
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

preserves-neg-iso-Commutative-Ring :
(f : iso-Commutative-Ring) {x : type-Commutative-Ring A} →
map-iso-Commutative-Ring f (neg-Commutative-Ring A x) ＝
neg-Commutative-Ring B (map-iso-Commutative-Ring f x)
preserves-neg-iso-Commutative-Ring =
preserves-neg-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

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

is-iso-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
is-iso-Commutative-Ring A B (hom-iso-Commutative-Ring f)
is-iso-iso-Commutative-Ring =
is-iso-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

hom-inv-iso-Commutative-Ring :
iso-Commutative-Ring → hom-Commutative-Ring B A
hom-inv-iso-Commutative-Ring =
hom-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

map-inv-iso-Commutative-Ring :
iso-Commutative-Ring → type-Commutative-Ring B → type-Commutative-Ring A
map-inv-iso-Commutative-Ring =
map-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

preserves-zero-inv-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
map-inv-iso-Commutative-Ring f (zero-Commutative-Ring B) ＝
zero-Commutative-Ring A
preserves-zero-inv-iso-Commutative-Ring =
preserves-zero-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

preserves-one-inv-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
map-inv-iso-Commutative-Ring f (one-Commutative-Ring B) ＝
one-Commutative-Ring A
preserves-one-inv-iso-Commutative-Ring =
preserves-one-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

(f : iso-Commutative-Ring) {x y : type-Commutative-Ring B} →
map-inv-iso-Commutative-Ring f (add-Commutative-Ring B x y) ＝
( map-inv-iso-Commutative-Ring f x)
( map-inv-iso-Commutative-Ring f y)
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

preserves-neg-inv-iso-Commutative-Ring :
(f : iso-Commutative-Ring) {x : type-Commutative-Ring B} →
map-inv-iso-Commutative-Ring f (neg-Commutative-Ring B x) ＝
neg-Commutative-Ring A (map-inv-iso-Commutative-Ring f x)
preserves-neg-inv-iso-Commutative-Ring =
preserves-neg-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

preserves-mul-inv-iso-Commutative-Ring :
(f : iso-Commutative-Ring) {x y : type-Commutative-Ring B} →
map-inv-iso-Commutative-Ring f (mul-Commutative-Ring B x y) ＝
mul-Commutative-Ring A
( map-inv-iso-Commutative-Ring f x)
( map-inv-iso-Commutative-Ring f y)
preserves-mul-inv-iso-Commutative-Ring =
preserves-mul-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

is-section-hom-inv-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
comp-hom-Commutative-Ring B A B
( hom-iso-Commutative-Ring f)
( hom-inv-iso-Commutative-Ring f) ＝
id-hom-Commutative-Ring B
is-section-hom-inv-iso-Commutative-Ring =
is-section-hom-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

is-section-map-inv-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
map-iso-Commutative-Ring f ∘ map-inv-iso-Commutative-Ring f ~ id
is-section-map-inv-iso-Commutative-Ring =
is-section-map-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

is-retraction-hom-inv-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
comp-hom-Commutative-Ring A B A
( hom-inv-iso-Commutative-Ring f)
( hom-iso-Commutative-Ring f) ＝
id-hom-Commutative-Ring A
is-retraction-hom-inv-iso-Commutative-Ring =
is-retraction-hom-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

is-retraction-map-inv-iso-Commutative-Ring :
(f : iso-Commutative-Ring) →
map-inv-iso-Commutative-Ring f ∘ map-iso-Commutative-Ring f ~ id
is-retraction-map-inv-iso-Commutative-Ring =
is-retraction-map-inv-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)


### The identity isomorphism of commutative rings

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

is-iso-id-hom-Commutative-Ring :
is-iso-Commutative-Ring A A (id-hom-Commutative-Ring A)
is-iso-id-hom-Commutative-Ring =
is-iso-id-hom-Ring (ring-Commutative-Ring A)

id-iso-Commutative-Ring : iso-Commutative-Ring A A
id-iso-Commutative-Ring = id-iso-Ring (ring-Commutative-Ring A)


### Converting identifications of commutative rings to isomorphisms of commutative rings

iso-eq-Commutative-Ring :
{ l : Level} (A B : Commutative-Ring l) → A ＝ B → iso-Commutative-Ring A B
iso-eq-Commutative-Ring =
iso-eq-Large-Precategory Commutative-Ring-Large-Precategory


## Properties

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

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

iso-ab-Commutative-Ring : UU (l1 ⊔ l2)
iso-ab-Commutative-Ring =
iso-ab-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

iso-ab-iso-ab-Commutative-Ring :
iso-ab-Commutative-Ring →
iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
iso-ab-iso-ab-Commutative-Ring =
iso-ab-iso-ab-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

is-iso-ab-hom-Commutative-Ring :
hom-Commutative-Ring A B → UU (l1 ⊔ l2)
is-iso-ab-hom-Commutative-Ring =
is-iso-ab-hom-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

is-iso-ab-is-iso-Commutative-Ring :
(f : hom-Commutative-Ring A B) →
is-iso-Commutative-Ring A B f → is-iso-ab-hom-Commutative-Ring f
is-iso-ab-is-iso-Commutative-Ring =
is-iso-ab-is-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

iso-ab-iso-Commutative-Ring :
iso-Commutative-Ring A B →
iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
iso-ab-iso-Commutative-Ring =
iso-ab-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)

equiv-iso-ab-iso-Commutative-Ring :
iso-Commutative-Ring A B ≃ iso-ab-Commutative-Ring
equiv-iso-ab-iso-Commutative-Ring =
equiv-iso-ab-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring B)


### Characterizing identifications of commutative rings

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

abstract
is-torsorial-iso-Commutative-Ring :
is-torsorial (λ (B : Commutative-Ring l) → iso-Commutative-Ring A B)
is-torsorial-iso-Commutative-Ring =
is-torsorial-Eq-subtype
( is-torsorial-iso-Ring (ring-Commutative-Ring A))
( is-prop-is-commutative-Ring)
( ring-Commutative-Ring A)
( id-iso-Ring (ring-Commutative-Ring A))
( commutative-mul-Commutative-Ring A)

is-equiv-iso-eq-Commutative-Ring :
(B : Commutative-Ring l) → is-equiv (iso-eq-Commutative-Ring A B)
is-equiv-iso-eq-Commutative-Ring =
fundamental-theorem-id
( is-torsorial-iso-Commutative-Ring)
( iso-eq-Commutative-Ring A)

extensionality-Commutative-Ring :
(B : Commutative-Ring l) → (A ＝ B) ≃ iso-Commutative-Ring A B
pr1 (extensionality-Commutative-Ring B) = iso-eq-Commutative-Ring A B
pr2 (extensionality-Commutative-Ring B) = is-equiv-iso-eq-Commutative-Ring B

eq-iso-Commutative-Ring :
(B : Commutative-Ring l) → iso-Commutative-Ring A B → A ＝ B
eq-iso-Commutative-Ring B =
map-inv-is-equiv (is-equiv-iso-eq-Commutative-Ring B)


### Any isomorphism of commutative rings preserves and reflects invertible elements

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

preserves-invertible-elements-iso-Commutative-Ring :
{x : type-Commutative-Ring A} →
is-invertible-element-Commutative-Ring A x →
is-invertible-element-Commutative-Ring S (map-iso-Commutative-Ring A S f x)
preserves-invertible-elements-iso-Commutative-Ring =
preserves-invertible-elements-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring S)
( f)

reflects-invertible-elements-iso-Commutative-Ring :
{x : type-Commutative-Ring A} →
is-invertible-element-Commutative-Ring S
( map-iso-Commutative-Ring A S f x) →
is-invertible-element-Commutative-Ring A x
reflects-invertible-elements-iso-Commutative-Ring =
reflects-invertible-elements-iso-Ring
( ring-Commutative-Ring A)
( ring-Commutative-Ring S)
( f)