Alternating concrete groups

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

Created on 2022-09-22.
Last modified on 2023-03-13.

module finite-group-theory.alternating-concrete-groups where
Imports 
open import elementary-number-theory.natural-numbers

open import finite-group-theory.cartier-delooping-sign-homomorphism
open import finite-group-theory.finite-type-groups

open import foundation.universe-levels

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

Idea

The alternating concrete groups are the kernels of the concrete sign homomorphism

Definition

module _
  (n : ℕ)
  where

  alternating-Concrete-Group : Concrete-Group (lsuc (lsuc lzero))
  alternating-Concrete-Group =
    concrete-group-kernel-hom-Concrete-Group
      ( UU-Fin-Group lzero n)
      ( UU-Fin-Group (lsuc lzero) 2)
      ( cartier-delooping-sign n)

Recent changes