Surjective group homomorphisms

Content created by Egbert Rijke and Fredrik Bakke

Created on 2023-08-21.
Last modified on 2023-08-21.

module group-theory.surjective-group-homomorphisms where
Imports 
open import foundation.propositions
open import foundation.surjective-maps
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.homomorphisms-groups

A group homomorphism f : G → H is said to be surjective if its underlying map is surjective

Definition

Surjective group homomorphisms

module _
  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : type-hom-Group G H)
  where

  is-surjective-prop-hom-Group : Prop (l1 ⊔ l2)
  is-surjective-prop-hom-Group = is-surjective-Prop (map-hom-Group G H f)

  is-surjective-hom-Group : UU (l1 ⊔ l2)
  is-surjective-hom-Group = type-Prop is-surjective-prop-hom-Group

  is-prop-is-surjective-hom-Group : is-prop is-surjective-hom-Group
  is-prop-is-surjective-hom-Group =
    is-prop-type-Prop is-surjective-prop-hom-Group

Recent changes