Kernels
module group-theory.kernels where
Imports
open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.universe-levels open import group-theory.abelian-groups open import group-theory.embeddings-abelian-groups open import group-theory.embeddings-groups open import group-theory.groups open import group-theory.homomorphisms-abelian-groups open import group-theory.homomorphisms-groups open import group-theory.normal-subgroups open import group-theory.subgroups open import group-theory.subgroups-abelian-groups
Idea
The kernel of a group homomorphism f : A → B
is the subgroup of A
consisting of those elements which f
sends to the unit of B.
Definition
We define the kernel as the subgroup generated by the predicate which associates
to x
the proposition f(x) = unit
.
module _ {l k : Level} (G : Group l) (H : Group k) (f : type-hom-Group G H) where subtype-kernel-hom-Group : subset-Group k G subtype-kernel-hom-Group x = Id-Prop (set-Group H) (map-hom-Group G H f x) (unit-Group H) is-in-kernel-hom-Group : type-Group G → UU k is-in-kernel-hom-Group x = type-Prop (subtype-kernel-hom-Group x) contains-unit-subtype-kernel-hom-Group : is-in-kernel-hom-Group (unit-Group G) contains-unit-subtype-kernel-hom-Group = preserves-unit-hom-Group G H f is-closed-under-mul-subtype-kernel-hom-Group : is-closed-under-mul-subset-Group G subtype-kernel-hom-Group is-closed-under-mul-subtype-kernel-hom-Group x y p q = ( preserves-mul-hom-Group G H f x y) ∙ ( ( ap (λ (x , y) → mul-Group H x y) (eq-pair p q)) ∙ ( left-unit-law-mul-Group H _)) is-closed-under-inv-subtype-kernel-hom-Group : is-closed-under-inv-subset-Group G subtype-kernel-hom-Group is-closed-under-inv-subtype-kernel-hom-Group x p = ( preserves-inv-hom-Group G H f x) ∙ ( ap (inv-Group H) p ∙ inv-unit-Group H) subgroup-kernel-hom-Group : Subgroup k G pr1 subgroup-kernel-hom-Group = subtype-kernel-hom-Group pr1 (pr2 subgroup-kernel-hom-Group) = contains-unit-subtype-kernel-hom-Group pr1 (pr2 (pr2 subgroup-kernel-hom-Group)) = is-closed-under-mul-subtype-kernel-hom-Group pr2 (pr2 (pr2 subgroup-kernel-hom-Group)) = is-closed-under-inv-subtype-kernel-hom-Group group-kernel-hom-Group : Group (l ⊔ k) group-kernel-hom-Group = group-Subgroup G subgroup-kernel-hom-Group inclusion-kernel-hom-Group : type-hom-Group group-kernel-hom-Group G inclusion-kernel-hom-Group = hom-inclusion-Subgroup G subgroup-kernel-hom-Group is-emb-inclusion-kernel-hom-Group : is-emb-hom-Group group-kernel-hom-Group G inclusion-kernel-hom-Group is-emb-inclusion-kernel-hom-Group = is-emb-inclusion-Subgroup G subgroup-kernel-hom-Group emb-inclusion-kernel-hom-Group : emb-Group group-kernel-hom-Group G pr1 emb-inclusion-kernel-hom-Group = inclusion-kernel-hom-Group pr2 emb-inclusion-kernel-hom-Group = is-emb-inclusion-kernel-hom-Group
Properties
module _ {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : type-hom-Group G H) where is-normal-kernel-hom-Group : is-normal-Subgroup G (subgroup-kernel-hom-Group G H f) is-normal-kernel-hom-Group g h = ( preserves-mul-hom-Group G H f (mul-Group G g (pr1 h)) (inv-Group G g)) ∙ ( ( ap ( mul-Group' H (map-hom-Group G H f (inv-Group G g))) ( ( preserves-mul-hom-Group G H f g (pr1 h)) ∙ ( ( ap (mul-Group H (map-hom-Group G H f g)) (pr2 h)) ∙ ( right-unit-law-mul-Group H (map-hom-Group G H f g))))) ∙ ( ( ap ( mul-Group H (map-hom-Group G H f g)) ( preserves-inv-hom-Group G H f g)) ∙ ( right-inverse-law-mul-Group H (map-hom-Group G H f g)))) kernel-hom-Group : Normal-Subgroup l2 G pr1 kernel-hom-Group = subgroup-kernel-hom-Group G H f pr2 kernel-hom-Group = is-normal-kernel-hom-Group
module _ {l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : type-hom-Ab A B) where subtype-kernel-hom-Ab : subset-Ab l2 A subtype-kernel-hom-Ab = subtype-kernel-hom-Group (group-Ab A) (group-Ab B) f is-in-kernel-hom-Ab : type-Ab A → UU l2 is-in-kernel-hom-Ab = is-in-kernel-hom-Group (group-Ab A) (group-Ab B) f contains-zero-subtype-kernel-hom-Ab : is-in-kernel-hom-Ab (zero-Ab A) contains-zero-subtype-kernel-hom-Ab = contains-unit-subtype-kernel-hom-Group (group-Ab A) (group-Ab B) f is-closed-under-add-subtype-kernel-hom-Ab : is-closed-under-add-subset-Ab A subtype-kernel-hom-Ab is-closed-under-add-subtype-kernel-hom-Ab = is-closed-under-mul-subtype-kernel-hom-Group ( group-Ab A) ( group-Ab B) ( f) is-closed-under-neg-subtype-kernel-hom-Ab : is-closed-under-neg-subset-Ab A subtype-kernel-hom-Ab is-closed-under-neg-subtype-kernel-hom-Ab = is-closed-under-inv-subtype-kernel-hom-Group ( group-Ab A) ( group-Ab B) ( f) kernel-hom-Ab : Subgroup-Ab l2 A kernel-hom-Ab = subgroup-kernel-hom-Group (group-Ab A) (group-Ab B) f ab-kernel-hom-Ab : Ab (l1 ⊔ l2) ab-kernel-hom-Ab = ab-Subgroup-Ab A kernel-hom-Ab inclusion-kernel-hom-Ab : type-hom-Ab ab-kernel-hom-Ab A inclusion-kernel-hom-Ab = inclusion-kernel-hom-Group (group-Ab A) (group-Ab B) f is-emb-inclusion-kernel-hom-Ab : is-emb-hom-Ab ab-kernel-hom-Ab A inclusion-kernel-hom-Ab is-emb-inclusion-kernel-hom-Ab = is-emb-inclusion-kernel-hom-Group (group-Ab A) (group-Ab B) f emb-inclusion-kernel-hom-Ab : emb-Ab ab-kernel-hom-Ab A emb-inclusion-kernel-hom-Ab = emb-inclusion-kernel-hom-Group (group-Ab A) (group-Ab B) f