Embeddings of abelian groups

Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.

Created on 2023-03-08.
Last modified on 2023-03-13.

module group-theory.embeddings-abelian-groups where
open import foundation.embeddings
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.embeddings-groups
open import group-theory.homomorphisms-abelian-groups
open import group-theory.subgroups-abelian-groups


Embeddings of groups are group homomorphisms of which the underlying map is an embedding


Embeddings of abelian groups

module _
  {l1 l2 : Level} (A : Ab l1) (B : Ab l2)

  is-emb-hom-Ab : (type-hom-Ab A B)  UU (l1  l2)
  is-emb-hom-Ab = is-emb-hom-Group (group-Ab A) (group-Ab B)

  emb-Ab : UU (l1  l2)
  emb-Ab = emb-Group (group-Ab A) (group-Ab B)

  hom-emb-Ab : emb-Ab  type-hom-Ab A B
  hom-emb-Ab = hom-emb-Group (group-Ab A) (group-Ab B)

  map-emb-hom-Ab : emb-Ab  type-Ab A  type-Ab B
  map-emb-hom-Ab = map-emb-hom-Group (group-Ab A) (group-Ab B)

  is-emb-map-emb-hom-Ab : (f : emb-Ab)  is-emb (map-emb-hom-Ab f)
  is-emb-map-emb-hom-Ab =
    is-emb-map-emb-hom-Group (group-Ab A) (group-Ab B)

The type of all embeddings into an abelian group

emb-Ab-Slice :
  (l : Level) {l1 : Level} (A : Ab l1)  UU ((lsuc l)  l1)
emb-Ab-Slice l A = emb-Group-Slice l (group-Ab A)

emb-ab-slice-Subgroup-Ab :
  { l1 l2 : Level} (A : Ab l1) 
  Subgroup-Ab l2 A  emb-Ab-Slice (l1  l2) A
emb-ab-slice-Subgroup-Ab A = emb-group-slice-Subgroup (group-Ab A)

Recent changes