Kernels

module group-theory.kernels where

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