Homomorphisms of groups
module group-theory.homomorphisms-groups where
Imports
open import foundation.cartesian-product-types 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.groups open import group-theory.homomorphisms-semigroups
Idea
A group homomorphism from one group to another is a semigroup homomorphism between their underlying semigroups
Definition
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) where preserves-mul-Group : (type-Group G → type-Group H) → UU (l1 ⊔ l2) preserves-mul-Group f = preserves-mul-Semigroup (semigroup-Group G) (semigroup-Group H) f preserves-mul-Group' : (type-Group G → type-Group H) → UU (l1 ⊔ l2) preserves-mul-Group' f = preserves-mul-Semigroup' (semigroup-Group G) (semigroup-Group H) f type-hom-Group : UU (l1 ⊔ l2) type-hom-Group = type-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) map-hom-Group : type-hom-Group → type-Group G → type-Group H map-hom-Group = pr1 preserves-mul-hom-Group : (f : type-hom-Group) → preserves-mul-Semigroup ( semigroup-Group G) ( semigroup-Group H) ( map-hom-Group f) preserves-mul-hom-Group = pr2
The identity group homomorphism
id-hom-Group : {l : Level} (G : Group l) → type-hom-Group G G id-hom-Group G = id-hom-Semigroup (semigroup-Group G)
Composition of group homomorphisms
comp-hom-Group : {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (K : Group l3) → type-hom-Group H K → type-hom-Group G H → type-hom-Group G K comp-hom-Group G H K = comp-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) ( semigroup-Group K)
Properties
Characterization of the identity type of group homomorphisms
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) where htpy-hom-Group : (f g : type-hom-Group G H) → UU (l1 ⊔ l2) htpy-hom-Group = htpy-hom-Semigroup (semigroup-Group G) (semigroup-Group H) refl-htpy-hom-Group : (f : type-hom-Group G H) → htpy-hom-Group f f refl-htpy-hom-Group = refl-htpy-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) htpy-eq-hom-Group : (f g : type-hom-Group G H) → Id f g → htpy-hom-Group f g htpy-eq-hom-Group = htpy-eq-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) abstract is-contr-total-htpy-hom-Group : ( f : type-hom-Group G H) → is-contr (Σ (type-hom-Group G H) (htpy-hom-Group f)) is-contr-total-htpy-hom-Group = is-contr-total-htpy-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) abstract is-equiv-htpy-eq-hom-Group : (f g : type-hom-Group G H) → is-equiv (htpy-eq-hom-Group f g) is-equiv-htpy-eq-hom-Group = is-equiv-htpy-eq-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) extensionality-hom-Group : (f g : type-hom-Group G H) → Id f g ≃ htpy-hom-Group f g pr1 (extensionality-hom-Group f g) = htpy-eq-hom-Group f g pr2 (extensionality-hom-Group f g) = is-equiv-htpy-eq-hom-Group f g eq-htpy-hom-Group : {f g : type-hom-Group G H} → htpy-hom-Group f g → Id f g eq-htpy-hom-Group = eq-htpy-hom-Semigroup (semigroup-Group G) (semigroup-Group H) is-set-type-hom-Group : is-set (type-hom-Group G H) is-set-type-hom-Group = is-set-type-hom-Semigroup (semigroup-Group G) (semigroup-Group H) hom-Group : Set (l1 ⊔ l2) pr1 hom-Group = type-hom-Group G H pr2 hom-Group = is-set-type-hom-Group
Associativity of composition of group homomorphisms
associative-comp-hom-Group : {l1 l2 l3 l4 : Level} (G : Group l1) (H : Group l2) (K : Group l3) (L : Group l4) (h : type-hom-Group K L) (g : type-hom-Group H K) (f : type-hom-Group G H) → Id ( comp-hom-Group G H L (comp-hom-Group H K L h g) f) ( comp-hom-Group G K L h (comp-hom-Group G H K g f)) associative-comp-hom-Group G H K L = associative-comp-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) ( semigroup-Group K) ( semigroup-Group L)
The left and right unit laws for composition of group homomorphisms
left-unit-law-comp-hom-Group : {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : type-hom-Group G H) → Id (comp-hom-Group G H H (id-hom-Group H) f) f left-unit-law-comp-hom-Group G H = left-unit-law-comp-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H) right-unit-law-comp-hom-Group : {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : type-hom-Group G H) → Id (comp-hom-Group G G H f (id-hom-Group G)) f right-unit-law-comp-hom-Group G H = right-unit-law-comp-hom-Semigroup ( semigroup-Group G) ( semigroup-Group H)
Group homomorphisms preserve the unit element
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) where preserves-unit-Group : (type-Group G → type-Group H) → UU l2 preserves-unit-Group f = Id (f (unit-Group G)) (unit-Group H) abstract preserves-unit-hom-Group : ( f : type-hom-Group G H) → preserves-unit-Group (map-hom-Group G H f) preserves-unit-hom-Group f = ( inv (left-unit-law-mul-Group H (map-hom-Group G H f (unit-Group G)))) ∙ ( ( ap ( λ x → mul-Group H x (map-hom-Group G H f (unit-Group G))) ( inv ( left-inverse-law-mul-Group H ( map-hom-Group G H f (unit-Group G))))) ∙ ( ( associative-mul-Group H ( inv-Group H (map-hom-Group G H f (unit-Group G))) ( map-hom-Group G H f (unit-Group G)) ( map-hom-Group G H f (unit-Group G))) ∙ ( ( ap ( mul-Group H (inv-Group H (map-hom-Group G H f (unit-Group G)))) ( inv ( preserves-mul-hom-Group G H f ( unit-Group G) ( unit-Group G)))) ∙ ( ( ap ( λ x → mul-Group H ( inv-Group H (map-hom-Group G H f (unit-Group G))) ( map-hom-Group G H f x)) ( left-unit-law-mul-Group G (unit-Group G))) ∙ ( left-inverse-law-mul-Group H ( map-hom-Group G H f (unit-Group G)))))))
Group homomorphisms preserve inverses
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) where preserves-inverses-Group : (type-Group G → type-Group H) → UU (l1 ⊔ l2) preserves-inverses-Group f = (x : type-Group G) → Id (f (inv-Group G x)) (inv-Group H (f x)) abstract preserves-inv-hom-Group : (f : type-hom-Group G H) → preserves-inverses-Group (map-hom-Group G H f) preserves-inv-hom-Group f x = ( inv ( right-unit-law-mul-Group H (map-hom-Group G H f (inv-Group G x)))) ∙ ( ( ap ( mul-Group H (map-hom-Group G H f (inv-Group G x))) ( inv (right-inverse-law-mul-Group H (map-hom-Group G H f x)))) ∙ ( ( inv ( associative-mul-Group H ( map-hom-Group G H f (inv-Group G x)) ( map-hom-Group G H f x) ( inv-Group H (map-hom-Group G H f x)))) ∙ ( ( inv ( ap ( λ y → mul-Group H y (inv-Group H (map-hom-Group G H f x))) ( preserves-mul-hom-Group G H f (inv-Group G x) x))) ∙ ( ( ap ( λ y → mul-Group H ( map-hom-Group G H f y) ( inv-Group H (map-hom-Group G H f x))) ( left-inverse-law-mul-Group G x)) ∙ ( ( ap ( λ y → mul-Group H y (inv-Group H (map-hom-Group G H f x))) ( preserves-unit-hom-Group G H f)) ∙ ( left-unit-law-mul-Group H ( inv-Group H (map-hom-Group G H f x))))))))
Group homomorphisms preserve all group structure
hom-Group' : { l1 l2 : Level} (G : Group l1) (H : Group l2) → UU (l1 ⊔ l2) hom-Group' G H = Σ ( type-hom-Group G H) ( λ f → ( preserves-unit-Group G H (map-hom-Group G H f)) × ( preserves-inverses-Group G H (map-hom-Group G H f))) preserves-group-structure-hom-Group : { l1 l2 : Level} (G : Group l1) (H : Group l2) → type-hom-Group G H → hom-Group' G H pr1 (preserves-group-structure-hom-Group G H f) = f pr1 (pr2 (preserves-group-structure-hom-Group G H f)) = preserves-unit-hom-Group G H f pr2 (pr2 (preserves-group-structure-hom-Group G H f)) = preserves-inv-hom-Group G H f