Trivial subgroups
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2022-08-20.
Last modified on 2023-09-15.
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
Trivial subgroups
module _ {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) where is-trivial-Subgroup : UU (l1 ⊔ l2) is-trivial-Subgroup = (x : type-Group G) → is-in-Subgroup G H x → x = unit-Group G
The trivial subgroup
module _ {l1 : Level} (G : Group l1) where trivial-Subgroup : Subgroup l1 G pr1 trivial-Subgroup x = is-unit-group-Prop G x pr1 (pr2 trivial-Subgroup) = refl pr1 (pr2 (pr2 trivial-Subgroup)) .(unit-Group G) .(unit-Group G) refl refl = left-unit-law-mul-Group G (unit-Group G) pr2 (pr2 (pr2 trivial-Subgroup)) .(unit-Group G) refl = inv-unit-Group G
Recent changes
- 2023-09-15. Fredrik Bakke. Define representations of monoids (#765).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).