# Homomorphisms of monoids ```agda module group-theory.homomorphisms-monoids where ``` <details><summary>Imports</summary> ```agda open import foundation.action-on-identifications-functions 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.torsorial-type-families open import foundation.universe-levels open import group-theory.homomorphisms-semigroups open import group-theory.invertible-elements-monoids open import group-theory.monoids ``` </details> ## Idea **Homomorphisms** between two [monoids](group-theory.monoids.md) are [homomorphisms](group-theory.homomorphisms-semigroups.md) between their underlying [semigroups](group-theory.semigroups.md) that preserve the unit element. ## Definition ### Homomorphisms of monoids ```agda module _ {l1 l2 : Level} (M1 : Monoid l1) (M2 : Monoid l2) where preserves-unit-prop-hom-Semigroup : hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2) → Prop l2 preserves-unit-prop-hom-Semigroup f = Id-Prop ( set-Monoid M2) ( map-hom-Semigroup ( semigroup-Monoid M1) ( semigroup-Monoid M2) ( f) ( unit-Monoid M1)) ( unit-Monoid M2) preserves-unit-hom-Semigroup : hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2) → UU l2 preserves-unit-hom-Semigroup f = type-Prop (preserves-unit-prop-hom-Semigroup f) is-prop-preserves-unit-hom-Semigroup : (f : hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2)) → is-prop (preserves-unit-hom-Semigroup f) is-prop-preserves-unit-hom-Semigroup f = is-prop-type-Prop (preserves-unit-prop-hom-Semigroup f) preserves-unit-hom-prop-Semigroup : hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2) → Prop l2 preserves-unit-hom-prop-Semigroup f = ( preserves-unit-hom-Semigroup f , is-prop-preserves-unit-hom-Semigroup f) hom-set-Monoid : Set (l1 ⊔ l2) hom-set-Monoid = set-subset ( hom-set-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2)) ( preserves-unit-prop-hom-Semigroup) hom-Monoid : UU (l1 ⊔ l2) hom-Monoid = type-Set hom-set-Monoid module _ {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (f : hom-Monoid M N) where hom-semigroup-hom-Monoid : hom-Semigroup (semigroup-Monoid M) (semigroup-Monoid N) hom-semigroup-hom-Monoid = pr1 f map-hom-Monoid : type-Monoid M → type-Monoid N map-hom-Monoid = map-hom-Semigroup ( semigroup-Monoid M) ( semigroup-Monoid N) ( hom-semigroup-hom-Monoid) preserves-mul-hom-Monoid : preserves-mul-Semigroup ( semigroup-Monoid M) ( semigroup-Monoid N) ( map-hom-Monoid) preserves-mul-hom-Monoid = preserves-mul-hom-Semigroup ( semigroup-Monoid M) ( semigroup-Monoid N) ( hom-semigroup-hom-Monoid) preserves-unit-hom-Monoid : preserves-unit-hom-Semigroup M N hom-semigroup-hom-Monoid preserves-unit-hom-Monoid = pr2 f ``` ### The identity homomorphism of monoids ```agda preserves-unit-id-hom-Monoid : { l : Level} (M : Monoid l) → preserves-unit-hom-Semigroup M M (id-hom-Semigroup (semigroup-Monoid M)) preserves-unit-id-hom-Monoid M = refl id-hom-Monoid : {l : Level} (M : Monoid l) → hom-Monoid M M pr1 (id-hom-Monoid M) = id-hom-Semigroup (semigroup-Monoid M) pr2 (id-hom-Monoid M) = preserves-unit-id-hom-Monoid M ``` ### Composition of homomorphisms of monoids ```agda module _ {l1 l2 l3 : Level} (K : Monoid l1) (L : Monoid l2) (M : Monoid l3) where preserves-unit-comp-hom-Monoid : (g : hom-Monoid L M) (f : hom-Monoid K L) → preserves-unit-hom-Semigroup K M ( comp-hom-Semigroup ( semigroup-Monoid K) ( semigroup-Monoid L) ( semigroup-Monoid M) ( hom-semigroup-hom-Monoid L M g) ( hom-semigroup-hom-Monoid K L f)) preserves-unit-comp-hom-Monoid g f = ( ap (map-hom-Monoid L M g) (preserves-unit-hom-Monoid K L f)) ∙ ( preserves-unit-hom-Monoid L M g) comp-hom-Monoid : hom-Monoid L M → hom-Monoid K L → hom-Monoid K M pr1 (comp-hom-Monoid g f) = comp-hom-Semigroup ( semigroup-Monoid K) ( semigroup-Monoid L) ( semigroup-Monoid M) ( hom-semigroup-hom-Monoid L M g) ( hom-semigroup-hom-Monoid K L f) pr2 (comp-hom-Monoid g f) = preserves-unit-comp-hom-Monoid g f ``` ### Homotopies of homomorphisms of monoids ```agda module _ {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) where htpy-hom-Monoid : (f g : hom-Monoid M N) → UU (l1 ⊔ l2) htpy-hom-Monoid f g = htpy-hom-Semigroup ( semigroup-Monoid M) ( semigroup-Monoid N) ( hom-semigroup-hom-Monoid M N f) ( hom-semigroup-hom-Monoid M N g) refl-htpy-hom-Monoid : (f : hom-Monoid M N) → htpy-hom-Monoid f f refl-htpy-hom-Monoid f = refl-htpy-hom-Semigroup ( semigroup-Monoid M) ( semigroup-Monoid N) ( hom-semigroup-hom-Monoid M N f) ``` ## Properties ### Homotopies characterize identifications of homomorphisms of monoids ```agda module _ {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (f : hom-Monoid M N) where is-torsorial-htpy-hom-Monoid : is-torsorial (htpy-hom-Monoid M N f) is-torsorial-htpy-hom-Monoid = is-torsorial-Eq-subtype ( is-torsorial-htpy-hom-Semigroup ( semigroup-Monoid M) ( semigroup-Monoid N) ( hom-semigroup-hom-Monoid M N f)) ( is-prop-preserves-unit-hom-Semigroup M N) ( hom-semigroup-hom-Monoid M N f) ( refl-htpy-hom-Monoid M N f) ( preserves-unit-hom-Monoid M N f) htpy-eq-hom-Monoid : (g : hom-Monoid M N) → f = g → htpy-hom-Monoid M N f g htpy-eq-hom-Monoid .f refl = refl-htpy-hom-Monoid M N f is-equiv-htpy-eq-hom-Monoid : (g : hom-Monoid M N) → is-equiv (htpy-eq-hom-Monoid g) is-equiv-htpy-eq-hom-Monoid = fundamental-theorem-id is-torsorial-htpy-hom-Monoid htpy-eq-hom-Monoid extensionality-hom-Monoid : (g : hom-Monoid M N) → (f = g) ≃ htpy-hom-Monoid M N f g pr1 (extensionality-hom-Monoid g) = htpy-eq-hom-Monoid g pr2 (extensionality-hom-Monoid g) = is-equiv-htpy-eq-hom-Monoid g eq-htpy-hom-Monoid : (g : hom-Monoid M N) → htpy-hom-Monoid M N f g → f = g eq-htpy-hom-Monoid g = map-inv-equiv (extensionality-hom-Monoid g) ``` ### Associativity of composition of homomorphisms of monoids ```agda module _ {l1 l2 l3 l4 : Level} (K : Monoid l1) (L : Monoid l2) (M : Monoid l3) (N : Monoid l4) where associative-comp-hom-Monoid : (h : hom-Monoid M N) (g : hom-Monoid L M) (f : hom-Monoid K L) → comp-hom-Monoid K L N (comp-hom-Monoid L M N h g) f = comp-hom-Monoid K M N h (comp-hom-Monoid K L M g f) associative-comp-hom-Monoid h g f = eq-htpy-hom-Monoid K N ( comp-hom-Monoid K L N (comp-hom-Monoid L M N h g) f) ( comp-hom-Monoid K M N h (comp-hom-Monoid K L M g f)) ( refl-htpy) ``` ### Unit laws for composition of homomorphisms of monoids ```agda module _ {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) where left-unit-law-comp-hom-Monoid : (f : hom-Monoid M N) → comp-hom-Monoid M N N (id-hom-Monoid N) f = f left-unit-law-comp-hom-Monoid f = eq-htpy-hom-Monoid M N ( comp-hom-Monoid M N N (id-hom-Monoid N) f) ( f) ( refl-htpy) right-unit-law-comp-hom-Monoid : (f : hom-Monoid M N) → comp-hom-Monoid M M N f (id-hom-Monoid M) = f right-unit-law-comp-hom-Monoid f = eq-htpy-hom-Monoid M N ( comp-hom-Monoid M M N f (id-hom-Monoid M)) ( f) ( refl-htpy) ``` ### Any homomorphism of monoids sends invertible elements to invertible elements ```agda module _ {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (f : hom-Monoid M N) where preserves-invertible-elements-hom-Monoid : {x : type-Monoid M} → is-invertible-element-Monoid M x → is-invertible-element-Monoid N (map-hom-Monoid M N f x) pr1 (preserves-invertible-elements-hom-Monoid (y , p , q)) = map-hom-Monoid M N f y pr1 (pr2 (preserves-invertible-elements-hom-Monoid (y , p , q))) = ( inv (preserves-mul-hom-Monoid M N f)) ∙ ( ap (map-hom-Monoid M N f) p) ∙ ( preserves-unit-hom-Monoid M N f) pr2 (pr2 (preserves-invertible-elements-hom-Monoid (y , p , q))) = ( inv (preserves-mul-hom-Monoid M N f)) ∙ ( ap (map-hom-Monoid M N f) q) ∙ ( preserves-unit-hom-Monoid M N f) ```