Homomorphisms of commutative rings

module commutative-algebra.homomorphisms-commutative-rings where
Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.homomorphisms-commutative-semirings

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

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

open import ring-theory.homomorphisms-rings

Idea

A homomorphism of commutative rings is a homomorphism between their underlying rings.

Definition

The predicate of being a ring homomorphism

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

  is-commutative-ring-homomorphism-hom-Ab-Prop :
    type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)  Prop (l1  l2)
  is-commutative-ring-homomorphism-hom-Ab-Prop =
    is-ring-homomorphism-hom-Ab-Prop
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)

  is-commutative-ring-homomorphism-hom-Ab :
    type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)  UU (l1  l2)
  is-commutative-ring-homomorphism-hom-Ab =
    is-ring-homomorphism-hom-Ab
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)

  is-prop-is-commutative-ring-homomorphism-hom-Ab :
    (f : type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)) 
    is-prop (is-commutative-ring-homomorphism-hom-Ab f)
  is-prop-is-commutative-ring-homomorphism-hom-Ab =
    is-prop-is-ring-homomorphism-hom-Ab
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
module _
  {l1 l2 : Level} (A : Commutative-Ring l1) (B : Commutative-Ring l2)
  where

  hom-Commutative-Ring : Set (l1  l2)
  hom-Commutative-Ring =
    hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B)

  type-hom-Commutative-Ring : UU (l1  l2)
  type-hom-Commutative-Ring =
    type-hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B)

  is-set-type-hom-Commutative-Ring : is-set type-hom-Commutative-Ring
  is-set-type-hom-Commutative-Ring =
    is-set-type-hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B)

  module _
    (f : type-hom-Commutative-Ring)
    where

    hom-ab-hom-Commutative-Ring :
      type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
    hom-ab-hom-Commutative-Ring =
      hom-ab-hom-Ring (ring-Commutative-Ring A) (ring-Commutative-Ring B) f

    hom-multiplicative-monoid-hom-Commutative-Ring :
      type-hom-Monoid
        ( multiplicative-monoid-Commutative-Ring A)
        ( multiplicative-monoid-Commutative-Ring B)
    hom-multiplicative-monoid-hom-Commutative-Ring =
      hom-multiplicative-monoid-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

    map-hom-Commutative-Ring : type-Commutative-Ring A  type-Commutative-Ring B
    map-hom-Commutative-Ring =
      map-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

    preserves-add-hom-Commutative-Ring :
      preserves-add-Ab
        ( ab-Commutative-Ring A)
        ( ab-Commutative-Ring B)
        ( map-hom-Commutative-Ring)
    preserves-add-hom-Commutative-Ring =
      preserves-add-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

    preserves-zero-hom-Commutative-Ring :
      preserves-zero-Ab
        ( ab-Commutative-Ring A)
        ( ab-Commutative-Ring B)
        ( map-hom-Commutative-Ring)
    preserves-zero-hom-Commutative-Ring =
      preserves-zero-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

    preserves-neg-hom-Commutative-Ring :
      preserves-negatives-Ab
        ( ab-Commutative-Ring A)
        ( ab-Commutative-Ring B)
        ( map-hom-Commutative-Ring)
    preserves-neg-hom-Commutative-Ring =
      preserves-neg-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

    preserves-mul-hom-Commutative-Ring :
      preserves-mul-hom-Ab
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( hom-ab-hom-Commutative-Ring)
    preserves-mul-hom-Commutative-Ring =
      preserves-mul-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

    preserves-unit-hom-Commutative-Ring :
      preserves-unit-hom-Ab
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( hom-ab-hom-Commutative-Ring)
    preserves-unit-hom-Commutative-Ring =
      preserves-unit-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

    is-commutative-ring-homomorphism-hom-Commutative-Ring :
      is-commutative-ring-homomorphism-hom-Ab A B hom-ab-hom-Commutative-Ring
    is-commutative-ring-homomorphism-hom-Commutative-Ring =
      is-ring-homomorphism-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

    hom-commutative-semiring-hom-Commutative-Ring :
      type-hom-Commutative-Semiring
        ( commutative-semiring-Commutative-Ring A)
        ( commutative-semiring-Commutative-Ring B)
    hom-commutative-semiring-hom-Commutative-Ring =
      hom-semiring-hom-Ring
        ( ring-Commutative-Ring A)
        ( ring-Commutative-Ring B)
        ( f)

The identity homomorphism of commutative rings

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

  preserves-mul-id-hom-Commutative-Ring :
    preserves-mul-hom-Ab
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring A)
      ( id-hom-Ab (ab-Commutative-Ring A))
  preserves-mul-id-hom-Commutative-Ring =
    preserves-mul-id-hom-Ring (ring-Commutative-Ring A)

  preserves-unit-id-hom-Commutative-Ring :
    preserves-unit-hom-Ab
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring A)
      ( id-hom-Ab (ab-Commutative-Ring A))
  preserves-unit-id-hom-Commutative-Ring =
    preserves-unit-id-hom-Ring (ring-Commutative-Ring A)

  is-ring-homomorphism-id-hom-Commutative-Ring :
    is-ring-homomorphism-hom-Ab
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring A)
      ( id-hom-Ab (ab-Commutative-Ring A))
  is-ring-homomorphism-id-hom-Commutative-Ring =
    is-ring-homomorphism-id-hom-Ring (ring-Commutative-Ring A)

  id-hom-Commutative-Ring : type-hom-Commutative-Ring A A
  id-hom-Commutative-Ring = id-hom-Ring (ring-Commutative-Ring A)

Composition of commutative ring homomorphisms

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

  hom-ab-comp-hom-Commutative-Ring :
    type-hom-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring C)
  hom-ab-comp-hom-Commutative-Ring =
    hom-ab-comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( ring-Commutative-Ring C)
      ( g)
      ( f)

  hom-multiplicative-monoid-comp-hom-Commutative-Ring :
    type-hom-Monoid
      ( multiplicative-monoid-Commutative-Ring A)
      ( multiplicative-monoid-Commutative-Ring C)
  hom-multiplicative-monoid-comp-hom-Commutative-Ring =
    hom-multiplicative-monoid-comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( ring-Commutative-Ring C)
      ( g)
      ( f)

  preserves-mul-comp-hom-Commutative-Ring :
    preserves-mul-hom-Ab
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring C)
      ( hom-ab-comp-hom-Commutative-Ring)
  preserves-mul-comp-hom-Commutative-Ring =
    preserves-mul-comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( ring-Commutative-Ring C)
      ( g)
      ( f)

  preserves-unit-comp-hom-Commutative-Ring :
    preserves-unit-hom-Ab
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring C)
      ( hom-ab-comp-hom-Commutative-Ring)
  preserves-unit-comp-hom-Commutative-Ring =
    preserves-unit-comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( ring-Commutative-Ring C)
      ( g)
      ( f)

  is-commutative-ring-homomorphism-comp-hom-Commutative-Ring :
    is-commutative-ring-homomorphism-hom-Ab A C
      ( hom-ab-comp-hom-Commutative-Ring)
  is-commutative-ring-homomorphism-comp-hom-Commutative-Ring =
    is-ring-homomorphism-comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( ring-Commutative-Ring C)
      ( g)
      ( f)

  comp-hom-Commutative-Ring : type-hom-Commutative-Ring A C
  comp-hom-Commutative-Ring =
    comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( ring-Commutative-Ring C)
      ( g)
      ( f)

Homotopies of homomorphisms of commutative rings

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

  htpy-hom-Commutative-Ring :
    type-hom-Commutative-Ring A B  type-hom-Commutative-Ring A B  UU (l1  l2)
  htpy-hom-Commutative-Ring =
    htpy-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)

  refl-htpy-hom-Commutative-Ring :
    (f : type-hom-Commutative-Ring A B)  htpy-hom-Commutative-Ring f f
  refl-htpy-hom-Commutative-Ring =
    refl-htpy-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)

Properties

Homotopies characterize identifications of homomorphisms of commutative rings

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

  htpy-eq-hom-Commutative-Ring :
    (g : type-hom-Commutative-Ring A B) 
    (f  g)  htpy-hom-Commutative-Ring A B f g
  htpy-eq-hom-Commutative-Ring =
    htpy-eq-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  is-contr-total-htpy-hom-Commutative-Ring :
    is-contr
      ( Σ (type-hom-Commutative-Ring A B) (htpy-hom-Commutative-Ring A B f))
  is-contr-total-htpy-hom-Commutative-Ring =
    is-contr-total-htpy-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  is-equiv-htpy-eq-hom-Commutative-Ring :
    (g : type-hom-Commutative-Ring A B) 
    is-equiv (htpy-eq-hom-Commutative-Ring g)
  is-equiv-htpy-eq-hom-Commutative-Ring =
    is-equiv-htpy-eq-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  extensionality-hom-Commutative-Ring :
    (g : type-hom-Commutative-Ring A B) 
    (f  g)  htpy-hom-Commutative-Ring A B f g
  extensionality-hom-Commutative-Ring =
    extensionality-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  eq-htpy-hom-Commutative-Ring :
    (g : type-hom-Commutative-Ring A B) 
    htpy-hom-Commutative-Ring A B f g  f  g
  eq-htpy-hom-Commutative-Ring =
    eq-htpy-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

Associativity of composition of ring homomorphisms

module _
  {l1 l2 l3 l4 : Level}
  (A : Commutative-Ring l1)
  (B : Commutative-Ring l2)
  (C : Commutative-Ring l3)
  (D : Commutative-Ring l4)
  (h : type-hom-Commutative-Ring C D)
  (g : type-hom-Commutative-Ring B C)
  (f : type-hom-Commutative-Ring A B)
  where

  associative-comp-hom-Commutative-Ring :
    ( comp-hom-Commutative-Ring A B D
      ( comp-hom-Commutative-Ring B C D h g)
      ( f)) 
    ( comp-hom-Commutative-Ring A C D
      ( h)
      ( comp-hom-Commutative-Ring A B C g f))
  associative-comp-hom-Commutative-Ring =
    associative-comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( ring-Commutative-Ring C)
      ( ring-Commutative-Ring D)
      ( h)
      ( g)
      ( f)

Unit laws for composition of homomorphisms of commutative rings

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

  left-unit-law-comp-hom-Commutative-Ring :
    comp-hom-Commutative-Ring A B B (id-hom-Commutative-Ring B) f  f
  left-unit-law-comp-hom-Commutative-Ring =
    left-unit-law-comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)

  right-unit-law-comp-hom-Commutative-Ring :
    comp-hom-Commutative-Ring A A B f (id-hom-Commutative-Ring A)  f
  right-unit-law-comp-hom-Commutative-Ring =
    right-unit-law-comp-hom-Ring
      ( ring-Commutative-Ring A)
      ( ring-Commutative-Ring B)
      ( f)