Homomorphisms of semirings
module ring-theory.homomorphisms-semirings where
Imports
open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.subtype-identity-principle open import foundation.subtypes open import foundation.universe-levels open import group-theory.homomorphisms-commutative-monoids open import group-theory.homomorphisms-monoids open import group-theory.homomorphisms-semigroups open import ring-theory.semirings
Idea
Homomorphisms of semirings are homomorphisms of their underlying additive commutative monoids that preserve multiplication and the multiplicative unit.
Definitions
module _ {l1 l2 : Level} (R : Semiring l1) (S : Semiring l2) where is-homomorphism-semiring-hom-Commutative-Monoid-Prop : ( type-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S)) → Prop (l1 ⊔ l2) is-homomorphism-semiring-hom-Commutative-Monoid-Prop f = Σ-Prop ( preserves-mul-semigroup-Prop ( multiplicative-semigroup-Semiring R) ( multiplicative-semigroup-Semiring S) ( map-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( f))) ( λ H → preserves-unit-hom-semigroup-Prop ( multiplicative-monoid-Semiring R) ( multiplicative-monoid-Semiring S) ( ( map-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( f)) , ( H))) is-homomorphism-semiring-hom-Commutative-Monoid : ( type-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S)) → UU (l1 ⊔ l2) is-homomorphism-semiring-hom-Commutative-Monoid f = type-Prop (is-homomorphism-semiring-hom-Commutative-Monoid-Prop f) is-prop-is-homomorphism-semiring-hom-Commutative-Monoid : ( f : type-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S)) → is-prop (is-homomorphism-semiring-hom-Commutative-Monoid f) is-prop-is-homomorphism-semiring-hom-Commutative-Monoid f = is-prop-type-Prop (is-homomorphism-semiring-hom-Commutative-Monoid-Prop f) hom-Semiring : Set (l1 ⊔ l2) hom-Semiring = set-subset ( hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S)) ( is-homomorphism-semiring-hom-Commutative-Monoid-Prop) type-hom-Semiring : UU (l1 ⊔ l2) type-hom-Semiring = type-Set hom-Semiring is-set-type-hom-Semiring : is-set type-hom-Semiring is-set-type-hom-Semiring = is-set-type-Set hom-Semiring module _ (f : type-hom-Semiring) where hom-additive-commutative-monoid-hom-Semiring : type-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) hom-additive-commutative-monoid-hom-Semiring = pr1 f map-hom-Semiring : type-Semiring R → type-Semiring S map-hom-Semiring = map-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( hom-additive-commutative-monoid-hom-Semiring) preserves-addition-hom-Semiring : (x y : type-Semiring R) → map-hom-Semiring (add-Semiring R x y) ＝ add-Semiring S (map-hom-Semiring x) (map-hom-Semiring y) preserves-addition-hom-Semiring = preserves-mul-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( hom-additive-commutative-monoid-hom-Semiring) preserves-zero-hom-Semiring : map-hom-Semiring (zero-Semiring R) ＝ zero-Semiring S preserves-zero-hom-Semiring = preserves-unit-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( hom-additive-commutative-monoid-hom-Semiring) preserves-mul-hom-Semiring : (x y : type-Semiring R) → map-hom-Semiring (mul-Semiring R x y) ＝ mul-Semiring S (map-hom-Semiring x) (map-hom-Semiring y) preserves-mul-hom-Semiring = pr1 (pr2 f) preserves-unit-hom-Semiring : map-hom-Semiring (one-Semiring R) ＝ one-Semiring S preserves-unit-hom-Semiring = pr2 (pr2 f) is-homomorphism-semiring-hom-Semiring : is-homomorphism-semiring-hom-Commutative-Monoid ( hom-additive-commutative-monoid-hom-Semiring) pr1 is-homomorphism-semiring-hom-Semiring = preserves-mul-hom-Semiring pr2 is-homomorphism-semiring-hom-Semiring = preserves-unit-hom-Semiring hom-multiplicative-monoid-hom-Semiring : type-hom-Monoid ( multiplicative-monoid-Semiring R) ( multiplicative-monoid-Semiring S) pr1 (pr1 hom-multiplicative-monoid-hom-Semiring) = map-hom-Semiring pr2 (pr1 hom-multiplicative-monoid-hom-Semiring) = preserves-mul-hom-Semiring pr2 hom-multiplicative-monoid-hom-Semiring = preserves-unit-hom-Semiring
The identity homomorphism of semirings
module _ {l : Level} (R : Semiring l) where hom-additive-commutative-monoid-id-hom-Semiring : type-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring R) hom-additive-commutative-monoid-id-hom-Semiring = id-hom-Commutative-Monoid (additive-commutative-monoid-Semiring R) preserves-mul-id-hom-Semiring : (x y : type-Semiring R) → mul-Semiring R x y ＝ mul-Semiring R x y preserves-mul-id-hom-Semiring x y = refl preserves-unit-id-hom-Semiring : one-Semiring R ＝ one-Semiring R preserves-unit-id-hom-Semiring = refl id-hom-Semiring : type-hom-Semiring R R pr1 id-hom-Semiring = hom-additive-commutative-monoid-id-hom-Semiring pr1 (pr2 id-hom-Semiring) = preserves-mul-id-hom-Semiring pr2 (pr2 id-hom-Semiring) = preserves-unit-id-hom-Semiring
Composition of homomorphisms of semirings
module _ {l1 l2 l3 : Level} (R : Semiring l1) (S : Semiring l2) (T : Semiring l3) (g : type-hom-Semiring S T) (f : type-hom-Semiring R S) where hom-additive-commutative-monoid-comp-hom-Semiring : type-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring T) hom-additive-commutative-monoid-comp-hom-Semiring = comp-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( additive-commutative-monoid-Semiring T) ( hom-additive-commutative-monoid-hom-Semiring S T g) ( hom-additive-commutative-monoid-hom-Semiring R S f) hom-multiplicative-monoid-comp-hom-Semiring : type-hom-Monoid ( multiplicative-monoid-Semiring R) ( multiplicative-monoid-Semiring T) hom-multiplicative-monoid-comp-hom-Semiring = comp-hom-Monoid ( multiplicative-monoid-Semiring R) ( multiplicative-monoid-Semiring S) ( multiplicative-monoid-Semiring T) ( hom-multiplicative-monoid-hom-Semiring S T g) ( hom-multiplicative-monoid-hom-Semiring R S f) map-comp-hom-Semiring : type-Semiring R → type-Semiring T map-comp-hom-Semiring = map-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring T) ( hom-additive-commutative-monoid-comp-hom-Semiring) preserves-mul-comp-hom-Semiring : (x y : type-Semiring R) → map-comp-hom-Semiring (mul-Semiring R x y) ＝ mul-Semiring T (map-comp-hom-Semiring x) (map-comp-hom-Semiring y) preserves-mul-comp-hom-Semiring = preserves-mul-hom-Monoid ( multiplicative-monoid-Semiring R) ( multiplicative-monoid-Semiring T) ( hom-multiplicative-monoid-comp-hom-Semiring) preserves-unit-comp-hom-Semiring : map-comp-hom-Semiring (one-Semiring R) ＝ one-Semiring T preserves-unit-comp-hom-Semiring = preserves-unit-hom-Monoid ( multiplicative-monoid-Semiring R) ( multiplicative-monoid-Semiring T) ( hom-multiplicative-monoid-comp-hom-Semiring) comp-hom-Semiring : type-hom-Semiring R T pr1 comp-hom-Semiring = hom-additive-commutative-monoid-comp-hom-Semiring pr1 (pr2 comp-hom-Semiring) = preserves-mul-comp-hom-Semiring pr2 (pr2 comp-hom-Semiring) = preserves-unit-comp-hom-Semiring
Homotopies of homomorphisms of semirings
module _ {l1 l2 : Level} (R : Semiring l1) (S : Semiring l2) where htpy-hom-Semiring : (f g : type-hom-Semiring R S) → UU (l1 ⊔ l2) htpy-hom-Semiring f g = htpy-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( hom-additive-commutative-monoid-hom-Semiring R S f) ( hom-additive-commutative-monoid-hom-Semiring R S g) refl-htpy-hom-Semiring : (f : type-hom-Semiring R S) → htpy-hom-Semiring f f refl-htpy-hom-Semiring f = refl-htpy-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( hom-additive-commutative-monoid-hom-Semiring R S f)
Properties
Homotopies characterize identifications of homomorphisms of semirings
module _ {l1 l2 : Level} (R : Semiring l1) (S : Semiring l2) (f : type-hom-Semiring R S) where is-contr-total-htpy-hom-Semiring : is-contr (Σ (type-hom-Semiring R S) (htpy-hom-Semiring R S f)) is-contr-total-htpy-hom-Semiring = is-contr-total-Eq-subtype ( is-contr-total-htpy-hom-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ( additive-commutative-monoid-Semiring S) ( hom-additive-commutative-monoid-hom-Semiring R S f)) ( is-prop-is-homomorphism-semiring-hom-Commutative-Monoid R S) ( hom-additive-commutative-monoid-hom-Semiring R S f) ( refl-htpy-hom-Semiring R S f) ( is-homomorphism-semiring-hom-Semiring R S f) htpy-eq-hom-Semiring : (g : type-hom-Semiring R S) → (f ＝ g) → htpy-hom-Semiring R S f g htpy-eq-hom-Semiring .f refl = refl-htpy-hom-Semiring R S f is-equiv-htpy-eq-hom-Semiring : (g : type-hom-Semiring R S) → is-equiv (htpy-eq-hom-Semiring g) is-equiv-htpy-eq-hom-Semiring = fundamental-theorem-id is-contr-total-htpy-hom-Semiring htpy-eq-hom-Semiring extensionality-hom-Semiring : (g : type-hom-Semiring R S) → (f ＝ g) ≃ htpy-hom-Semiring R S f g pr1 (extensionality-hom-Semiring g) = htpy-eq-hom-Semiring g pr2 (extensionality-hom-Semiring g) = is-equiv-htpy-eq-hom-Semiring g eq-htpy-hom-Semiring : (g : type-hom-Semiring R S) → htpy-hom-Semiring R S f g → f ＝ g eq-htpy-hom-Semiring g = map-inv-equiv (extensionality-hom-Semiring g)
Associativity of composition of homomorphisms of semirings
module _ {l1 l2 l3 l4 : Level} (R : Semiring l1) (S : Semiring l2) (T : Semiring l3) (U : Semiring l4) (h : type-hom-Semiring T U) (g : type-hom-Semiring S T) (f : type-hom-Semiring R S) where associative-comp-hom-Semiring : comp-hom-Semiring R S U (comp-hom-Semiring S T U h g) f ＝ comp-hom-Semiring R T U h (comp-hom-Semiring R S T g f) associative-comp-hom-Semiring = eq-htpy-hom-Semiring R U ( comp-hom-Semiring R S U (comp-hom-Semiring S T U h g) f) ( comp-hom-Semiring R T U h (comp-hom-Semiring R S T g f)) ( refl-htpy)
Unit laws for composition of homomorphisms of semirings
module _ {l1 l2 : Level} (R : Semiring l1) (S : Semiring l2) (f : type-hom-Semiring R S) where left-unit-law-comp-hom-Semiring : comp-hom-Semiring R S S (id-hom-Semiring S) f ＝ f left-unit-law-comp-hom-Semiring = eq-htpy-hom-Semiring R S ( comp-hom-Semiring R S S (id-hom-Semiring S) f) ( f) ( refl-htpy) right-unit-law-comp-hom-Semiring : comp-hom-Semiring R R S f (id-hom-Semiring R) ＝ f right-unit-law-comp-hom-Semiring = eq-htpy-hom-Semiring R S ( comp-hom-Semiring R R S f (id-hom-Semiring R)) ( f) ( refl-htpy)