Homomorphisms of commutative semirings

module commutative-algebra.homomorphisms-commutative-semirings where
Imports
open import commutative-algebra.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.sets
open import foundation.universe-levels

open import group-theory.homomorphisms-commutative-monoids
open import group-theory.homomorphisms-monoids

open import ring-theory.homomorphisms-semirings

Idea

A homomorphism of commutative semirings is a map which preserves 0, +, 1, and ·.

Definitions

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

  hom-Commutative-Semiring : Set (l1  l2)
  hom-Commutative-Semiring =
    hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)

  type-hom-Commutative-Semiring : UU (l1  l2)
  type-hom-Commutative-Semiring =
    type-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)

  is-set-type-hom-Commutative-Semiring : is-set type-hom-Commutative-Semiring
  is-set-type-hom-Commutative-Semiring =
    is-set-type-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)

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

    hom-additive-commutative-monoid-hom-Commutative-Semiring :
      type-hom-Commutative-Monoid
        ( additive-commutative-monoid-Commutative-Semiring A)
        ( additive-commutative-monoid-Commutative-Semiring B)
    hom-additive-commutative-monoid-hom-Commutative-Semiring =
      hom-additive-commutative-monoid-hom-Semiring
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( f)

    map-hom-Commutative-Semiring :
      type-Commutative-Semiring A  type-Commutative-Semiring B
    map-hom-Commutative-Semiring =
      map-hom-Semiring
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( f)

    preserves-addition-hom-Commutative-Semiring :
      (x y : type-Commutative-Semiring A) 
      map-hom-Commutative-Semiring (add-Commutative-Semiring A x y) 
      add-Commutative-Semiring B
        ( map-hom-Commutative-Semiring x)
        ( map-hom-Commutative-Semiring y)
    preserves-addition-hom-Commutative-Semiring =
      preserves-addition-hom-Semiring
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( f)

    preserves-zero-hom-Commutative-Semiring :
      map-hom-Commutative-Semiring (zero-Commutative-Semiring A) 
      zero-Commutative-Semiring B
    preserves-zero-hom-Commutative-Semiring =
      preserves-zero-hom-Semiring
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( f)

    preserves-mul-hom-Commutative-Semiring :
      (x y : type-Commutative-Semiring A) 
      map-hom-Commutative-Semiring (mul-Commutative-Semiring A x y) 
      mul-Commutative-Semiring B
        ( map-hom-Commutative-Semiring x)
        ( map-hom-Commutative-Semiring y)
    preserves-mul-hom-Commutative-Semiring =
      preserves-mul-hom-Semiring
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( f)

    preserves-unit-hom-Commutative-Semiring :
      map-hom-Commutative-Semiring (one-Commutative-Semiring A) 
      one-Commutative-Semiring B
    preserves-unit-hom-Commutative-Semiring =
      preserves-unit-hom-Semiring
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( f)

    is-homomorphism-semiring-hom-Commutative-Semiring :
      is-homomorphism-semiring-hom-Commutative-Monoid
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( hom-additive-commutative-monoid-hom-Commutative-Semiring)
    is-homomorphism-semiring-hom-Commutative-Semiring =
      is-homomorphism-semiring-hom-Semiring
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( f)

    hom-multiplicative-monoid-hom-Commutative-Semiring :
      type-hom-Monoid
        ( multiplicative-monoid-Commutative-Semiring A)
        ( multiplicative-monoid-Commutative-Semiring B)
    hom-multiplicative-monoid-hom-Commutative-Semiring =
      hom-multiplicative-monoid-hom-Semiring
        ( semiring-Commutative-Semiring A)
        ( semiring-Commutative-Semiring B)
        ( f)

The identity homomorphism of commutative semirings

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

  hom-additive-commutative-monoid-id-hom-Commutative-Semiring :
    type-hom-Commutative-Monoid
      ( additive-commutative-monoid-Commutative-Semiring A)
      ( additive-commutative-monoid-Commutative-Semiring A)
  hom-additive-commutative-monoid-id-hom-Commutative-Semiring =
    hom-additive-commutative-monoid-id-hom-Semiring
      ( semiring-Commutative-Semiring A)

  preserves-mul-id-hom-Commutative-Semiring :
    (x y : type-Commutative-Semiring A) 
    mul-Commutative-Semiring A x y  mul-Commutative-Semiring A x y
  preserves-mul-id-hom-Commutative-Semiring =
    preserves-mul-id-hom-Semiring (semiring-Commutative-Semiring A)

  preserves-unit-id-hom-Commutative-Semiring :
    one-Commutative-Semiring A  one-Commutative-Semiring A
  preserves-unit-id-hom-Commutative-Semiring =
    preserves-unit-id-hom-Semiring (semiring-Commutative-Semiring A)

  id-hom-Commutative-Semiring : type-hom-Commutative-Semiring A A
  id-hom-Commutative-Semiring =
    id-hom-Semiring (semiring-Commutative-Semiring A)

Composition of homomorphisms of commutative semirings

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

  hom-additive-commutative-monoid-comp-hom-Commutative-Semiring :
    type-hom-Commutative-Monoid
      ( additive-commutative-monoid-Commutative-Semiring A)
      ( additive-commutative-monoid-Commutative-Semiring C)
  hom-additive-commutative-monoid-comp-hom-Commutative-Semiring =
    hom-additive-commutative-monoid-comp-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( semiring-Commutative-Semiring C)
      ( g)
      ( f)

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

  map-comp-hom-Commutative-Semiring :
    type-Commutative-Semiring A  type-Commutative-Semiring C
  map-comp-hom-Commutative-Semiring =
    map-comp-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( semiring-Commutative-Semiring C)
      ( g)
      ( f)

  preserves-mul-comp-hom-Commutative-Semiring :
    (x y : type-Commutative-Semiring A) 
    map-comp-hom-Commutative-Semiring (mul-Commutative-Semiring A x y) 
    mul-Commutative-Semiring C
      ( map-comp-hom-Commutative-Semiring x)
      ( map-comp-hom-Commutative-Semiring y)
  preserves-mul-comp-hom-Commutative-Semiring =
    preserves-mul-comp-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( semiring-Commutative-Semiring C)
      ( g)
      ( f)

  preserves-unit-comp-hom-Commutative-Semiring :
    map-comp-hom-Commutative-Semiring (one-Commutative-Semiring A) 
    one-Commutative-Semiring C
  preserves-unit-comp-hom-Commutative-Semiring =
    preserves-unit-comp-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( semiring-Commutative-Semiring C)
      ( g)
      ( f)

  comp-hom-Commutative-Semiring : type-hom-Commutative-Semiring A C
  comp-hom-Commutative-Semiring =
    comp-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( semiring-Commutative-Semiring C)
      ( g)
      ( f)

Homotopies of homomorphisms of commutative semirings

module _
  {l1 l2 : Level} (R : Commutative-Semiring l1) (S : Commutative-Semiring l2)
  where

  htpy-hom-Commutative-Semiring :
    (f g : type-hom-Commutative-Semiring R S)  UU (l1  l2)
  htpy-hom-Commutative-Semiring f g =
    htpy-hom-Commutative-Monoid
      ( additive-commutative-monoid-Commutative-Semiring R)
      ( additive-commutative-monoid-Commutative-Semiring S)
      ( hom-additive-commutative-monoid-hom-Commutative-Semiring R S f)
      ( hom-additive-commutative-monoid-hom-Commutative-Semiring R S g)

  refl-htpy-hom-Commutative-Semiring :
    (f : type-hom-Commutative-Semiring R S)  htpy-hom-Commutative-Semiring f f
  refl-htpy-hom-Commutative-Semiring f =
    refl-htpy-hom-Commutative-Monoid
      ( additive-commutative-monoid-Commutative-Semiring R)
      ( additive-commutative-monoid-Commutative-Semiring S)
      ( hom-additive-commutative-monoid-hom-Commutative-Semiring R S f)

Properties

Homotopies characterize identifications of homomorphisms of commutative semirings

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

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

  htpy-eq-hom-Commutative-Semiring :
    (g : type-hom-Commutative-Semiring A B) 
    (f  g)  htpy-hom-Commutative-Semiring A B f g
  htpy-eq-hom-Commutative-Semiring =
    htpy-eq-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( f)

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

  extensionality-hom-Commutative-Semiring :
    (g : type-hom-Commutative-Semiring A B) 
    (f  g)  htpy-hom-Commutative-Semiring A B f g
  extensionality-hom-Commutative-Semiring =
    extensionality-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( f)

  eq-htpy-hom-Commutative-Semiring :
    (g : type-hom-Commutative-Semiring A B) 
    htpy-hom-Commutative-Semiring A B f g  f  g
  eq-htpy-hom-Commutative-Semiring =
    eq-htpy-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( f)

Associativity of composition of homomorphisms of commutative semirings

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

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

Unit laws for composition of homomorphisms of commutative semirings

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

  left-unit-law-comp-hom-Commutative-Semiring :
    comp-hom-Commutative-Semiring A B B (id-hom-Commutative-Semiring B) f  f
  left-unit-law-comp-hom-Commutative-Semiring =
    left-unit-law-comp-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( f)

  right-unit-law-comp-hom-Commutative-Semiring :
    comp-hom-Commutative-Semiring A A B f (id-hom-Commutative-Semiring A)  f
  right-unit-law-comp-hom-Commutative-Semiring =
    right-unit-law-comp-hom-Semiring
      ( semiring-Commutative-Semiring A)
      ( semiring-Commutative-Semiring B)
      ( f)