Trivial subgroups

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

Created on 2022-08-20.
Last modified on 2023-11-24.

module group-theory.trivial-subgroups where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.subgroups

Idea

A subgroup H of G is said to be trivial if it only contains the unit element of G.

Definitions

The trivial subgroup

module _
  {l1 : Level} (G : Group l1)
  where

  trivial-Subgroup : Subgroup l1 G
  pr1 trivial-Subgroup x = is-unit-prop-Group' G x
  pr1 (pr2 trivial-Subgroup) = refl
  pr1 (pr2 (pr2 trivial-Subgroup)) refl refl =
    inv (left-unit-law-mul-Group G (unit-Group G))
  pr2 (pr2 (pr2 trivial-Subgroup)) refl =
    inv (inv-unit-Group G)

The predicate of being a trivial subgroup

module _
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G)
  where

  is-trivial-Subgroup : UU (l1 ⊔ l2)
  is-trivial-Subgroup = leq-Subgroup G H (trivial-Subgroup G)

Recent changes