Type

Martin Escardo, 13th February. Group basics.

There is another equivalent definition of group in the file
UF.SIP-Examples.


{-# OPTIONS --safe --without-K --lossy-unification #-}

module Groups.Type where

open import MLTT.Spartan
open import UF.Base
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.FunExt
open import UF.Subsingletons-FunExt
open import UF.Equiv hiding (_≅_ ; ≅-refl)


Underlying type of a mathematical structure:


⟨_⟩ : {S : 𝓤 ̇ → 𝓥 ̇ } → Σ S → 𝓤 ̇
⟨ X , s ⟩ = X

monoid-structure : 𝓤 ̇ → 𝓤 ̇
monoid-structure X = (X → X → X) × X

monoid-axioms : (X : 𝓤 ̇ ) → monoid-structure X → 𝓤 ̇
monoid-axioms X (_·_ , e) = is-set X
                          × left-neutral  e _·_
                          × right-neutral e _·_
                          × associative     _·_

We choose the unit and inverses to be part of the axioms rather than
part of the structure in the case of groups:


group-structure : 𝓤 ̇ → 𝓤 ̇
group-structure X = X → X → X

group-axioms : (X : 𝓤 ̇ ) → group-structure X → 𝓤 ̇
group-axioms X _·_ = is-set X
                   × associative _·_
                   × (Σ e ꞉ X
                    , left-neutral  e _·_
                    × right-neutral e _·_
                    × ((x : X) → Σ x' ꞉ X , (x' · x ＝ e) × (x · x' ＝ e)))


Added by Ettore Aldrovandi (ealdrovandi@fsu.edu), July 25, 2022

Direct proof that the "group-axioms" is a proposition.


group-axioms-is-prop : funext 𝓤 𝓤
                     → (X : 𝓤 ̇ )
                     → (_·_ : group-structure X)
                     → is-prop (group-axioms X _·_)
group-axioms-is-prop fe X _·_ s = γ s
  where
    i : is-set X
    i = pr₁ s

    α : is-prop (associative _·_)
    α = Π-is-prop fe
                  (λ x → Π-is-prop fe
                                   (λ y →  Π-is-prop fe
                                                     (λ z → i)))

    β : is-prop ( Σ e ꞉ X , left-neutral e _·_ ×
                            right-neutral e _·_ ×
                            ((x : X) → Σ x' ꞉ X , (x' · x ＝ e) × (x · x' ＝ e)) )
    β (e , l , _ , _) (e' , _ , r , _) = to-subtype-＝ η p
      where
        p : e ＝ e'
        p = e      ＝⟨ (r e) ⁻¹ ⟩
            e · e' ＝⟨ l e' ⟩
            e' ∎

        η : (x : X) → is-prop (left-neutral x _·_ ×
                               right-neutral x _·_ ×
                               ((x₁ : X) → Σ x' ꞉ X , (x' · x₁ ＝ x) × (x₁ · x' ＝ x)))
        η x t = ε t
          where
            ε : is-prop (left-neutral x _·_ ×
                               right-neutral x _·_ ×
                               ((x₁ : X) → Σ x' ꞉ X , (x' · x₁ ＝ x) × (x₁ · x' ＝ x)))
            ε = ×-is-prop (Π-is-prop fe (λ _ → i))
                (×-is-prop (Π-is-prop fe (λ _ → i))
                 (Π-is-prop fe ε'))
                    where
                      ε' : (x₁ : X) → is-prop (Σ x' ꞉ X , (x' · x₁ ＝ x) × (x₁ · x' ＝ x))
                      ε' x₁ (u , v) (u' , v') = to-subtype-＝ (λ x₂ → ×-is-prop i i) q
                        where
                          q : u ＝ u'
                          q = u             ＝⟨ (pr₁ (pr₂ t) u) ⁻¹ ⟩
                              u · x         ＝⟨ ap (λ a → u · a) (pr₂ v') ⁻¹ ⟩
                              u · (x₁ · u') ＝⟨ (pr₁ (pr₂ s) _ _ _) ⁻¹ ⟩
                              (u · x₁) · u' ＝⟨ ap (λ a → a · u') (pr₁ v) ⟩
                              x · u'        ＝⟨ pr₁ t u' ⟩
                              u' ∎

    γ : is-prop (group-axioms X _·_)
    γ = ×-is-prop (being-set-is-prop fe)
        (×-is-prop α β)


End of addition.


Group-structure : 𝓤 ̇ → 𝓤 ̇
Group-structure X = Σ _·_ ꞉ group-structure X , (group-axioms X _·_)

Group : (𝓤 : Universe) → 𝓤 ⁺ ̇
Group 𝓤 = Σ X ꞉ 𝓤 ̇ , Group-structure X

monoid-structure-of : (G : Group 𝓤) → monoid-structure ⟨ G ⟩
monoid-structure-of (X , _·_ , i , a , e , l , r , ι) = (_·_ , e)

monoid-axioms-of : (G : Group 𝓤) → monoid-axioms ⟨ G ⟩ (monoid-structure-of G)
monoid-axioms-of (X , _·_ , i , a , e , l , r , ι) = i , l , r , a

inv-lemma : (X : 𝓤 ̇ ) (_·_ : X → X → X) (e : X)
          → monoid-axioms X (_·_ , e)
          → (x y z : X)
          → (y · x) ＝ e
          → (x · z) ＝ e
          → y ＝ z

inv-lemma X _·_  e (s , l , r , a) x y z q p =

   y             ＝⟨ (r y)⁻¹ ⟩
   (y · e)       ＝⟨ ap (y ·_) (p ⁻¹) ⟩
   (y · (x · z)) ＝⟨ (a y x z)⁻¹ ⟩
   ((y · x) · z) ＝⟨ ap (_· z) q ⟩
   (e · z)       ＝⟨ l z ⟩
   z             ∎

multiplication : (G : Group 𝓤) → ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
multiplication (X , _·_ , _) = _·_

syntax multiplication G x y = x ·⟨ G ⟩ y

groups-are-sets : (G : Group 𝓤) → is-set ⟨ G ⟩
groups-are-sets (X , _·_ , i , a , e , l , r , u) = i

unit : (G : Group 𝓤) → ⟨ G ⟩
unit (X , _·_ , i , a , e , l , r , u) = e

syntax unit G = e⟨ G ⟩

unit-left : (G : Group 𝓤) (x : ⟨ G ⟩)
          → unit G ·⟨ G ⟩ x ＝ x
unit-left (X , _·_ , i , a , e , l , r , u) = l


unit-right : (G : Group 𝓤) (x : ⟨ G ⟩)
           → x ·⟨ G ⟩ unit G ＝ x
unit-right (X , _·_ , i , a , e , l , r , u) = r


assoc : (G : Group 𝓤) (x y z : ⟨ G ⟩)
      → (x ·⟨ G ⟩ y) ·⟨ G ⟩ z ＝ x ·⟨ G ⟩ (y ·⟨ G ⟩ z)
assoc (X , _·_ , i , a , e , l , r , ι) = a

inv : (G : Group 𝓤) → ⟨ G ⟩ → ⟨ G ⟩
inv (X , _·_ , i , a , e , l , r , ι) x = pr₁ (ι x)

inv-left : (G : Group 𝓤) (x : ⟨ G ⟩)
         → inv G x ·⟨ G ⟩ x ＝ unit G
inv-left (X , _·_ , i , a , e , l , r , ι) x = pr₁ (pr₂ (ι x))

inv-right : (G : Group 𝓤) (x : ⟨ G ⟩)
          → x ·⟨ G ⟩ inv G x ＝ unit G
inv-right (X , _·_ , i , a , e , l , r , ι) x = pr₂ (pr₂ (ι x))

is-hom : (G : Group 𝓤) (H : Group 𝓥) → (⟨ G ⟩ → ⟨ H ⟩) → 𝓤 ⊔ 𝓥 ̇
is-hom G H f = ∀ {x y} → f (x ·⟨ G ⟩ y) ＝ f x ·⟨ H ⟩ f y

id-is-hom : (G : Group 𝓤) → is-hom G G id
id-is-hom G = refl

∘-is-hom : (F : Group 𝓤) (G : Group 𝓥) (H : Group 𝓦)
           (f : ⟨ F ⟩ → ⟨ G ⟩) (g : ⟨ G ⟩ → ⟨ H ⟩)
         → is-hom F G f → is-hom G H g → is-hom F H (g ∘ f)
∘-is-hom F G H f g h k {x} {y} = g (f (x ·⟨ F ⟩ y))     ＝⟨ ap g h ⟩
                                 g (f x ·⟨ G ⟩ f y)     ＝⟨ k ⟩
                                 g (f x) ·⟨ H ⟩ g (f y) ∎

being-hom-is-prop : Fun-Ext
                  → (G : Group 𝓤) (H : Group 𝓥) (f : ⟨ G ⟩ → ⟨ H ⟩)
                  → is-prop (is-hom G H f)
being-hom-is-prop fe G H f = implicit-Π-is-prop fe
                              (λ x → implicit-Π-is-prop fe
                                      (λ y → groups-are-sets H))

preserves-unit : (G : Group 𝓤) (H : Group 𝓥) → (⟨ G ⟩ → ⟨ H ⟩) → 𝓥 ̇
preserves-unit G H f = f (unit G) ＝ unit H

idempotent-is-unit : (G : Group 𝓤) (x : ⟨ G ⟩)
                   → x ·⟨ G ⟩ x ＝ x
                   → x ＝ unit G

idempotent-is-unit G x p = γ
 where
  x' = inv G x
  γ = x                        ＝⟨ (unit-left G x)⁻¹ ⟩
      unit G ·⟨ G ⟩ x          ＝⟨ (ap (λ - → - ·⟨ G ⟩ x) (inv-left G x))⁻¹ ⟩
      (x' ·⟨ G ⟩ x) ·⟨ G ⟩ x   ＝⟨ assoc G x' x x ⟩
      x' ·⟨ G ⟩ (x ·⟨ G ⟩ x)   ＝⟨ ap (λ - → x' ·⟨ G ⟩ -) p ⟩
      x' ·⟨ G ⟩ x              ＝⟨ inv-left G x ⟩
      unit G                   ∎

homs-preserve-unit : (G : Group 𝓤) (H : Group 𝓥) (f : ⟨ G ⟩ → ⟨ H ⟩)
                   → is-hom G H f
                   → preserves-unit G H f

homs-preserve-unit G H f m = idempotent-is-unit H e p
 where
  e = f (unit G)

  p = e ·⟨ H ⟩ e               ＝⟨ m ⁻¹ ⟩
      f (unit G ·⟨ G ⟩ unit G) ＝⟨ ap f (unit-left G (unit G)) ⟩
      e                        ∎

inv-Lemma : (G : Group 𝓤) (x y z : ⟨ G ⟩)
          → (y ·⟨ G ⟩ x) ＝ unit G
          → (x ·⟨ G ⟩ z) ＝ unit G
          → y ＝ z
inv-Lemma G = inv-lemma ⟨ G ⟩ (multiplication G) (unit G) (monoid-axioms-of G)


one-left-inv : (G : Group 𝓤) (x x' : ⟨ G ⟩)
             → (x' ·⟨ G ⟩ x) ＝ unit G
             → x' ＝ inv G x

one-left-inv G x x' p = inv-Lemma G x x' (inv G x) p (inv-right G x)

one-right-inv : (G : Group 𝓤) (x x' : ⟨ G ⟩)
              → (x ·⟨ G ⟩ x') ＝ unit G
              → x' ＝ inv G x

one-right-inv G x x' p = (inv-Lemma G x (inv G x) x' (inv-left G x) p)⁻¹

preserves-inv : (G : Group 𝓤) (H : Group 𝓥) → (⟨ G ⟩ → ⟨ H ⟩) → 𝓤 ⊔ 𝓥 ̇
preserves-inv G H f = (x : ⟨ G ⟩) → f (inv G x) ＝ inv H (f x)

homs-preserve-invs : (G : Group 𝓤) (H : Group 𝓥) (f : ⟨ G ⟩ → ⟨ H ⟩)
                   → is-hom G H f
                   → preserves-inv G H f
homs-preserve-invs G H f m x = γ
 where
  p = f (inv G x) ·⟨ H ⟩ f x ＝⟨ m ⁻¹ ⟩
      f (inv G x ·⟨ G ⟩ x)   ＝⟨ ap f (inv-left G x) ⟩
      f (unit G)             ＝⟨ homs-preserve-unit G H f m ⟩
      unit H                 ∎

  γ : f (inv G x) ＝ inv H (f x)
  γ = one-left-inv H (f x) (f (inv G x)) p


is-iso : (G : Group 𝓤) (H : Group 𝓥) → (⟨ G ⟩ → ⟨ H ⟩) → 𝓤 ⊔ 𝓥 ̇
is-iso G H f = is-equiv f × is-hom G H f

group-isos-are-equivs : (G : Group 𝓤) (H : Group 𝓥)
                        {f : ⟨ G ⟩ → ⟨ H ⟩}
                      → is-iso G H f
                      → is-equiv f
group-isos-are-equivs G H = pr₁

group-isos-are-homs : (G : Group 𝓤) (H : Group 𝓥)
                      {f : ⟨ G ⟩ → ⟨ H ⟩}
                     → is-iso G H f
                     → is-hom G H f
group-isos-are-homs G H = pr₂


inverses-are-homs : (G : Group 𝓤) (H : Group 𝓥) (f : ⟨ G ⟩ → ⟨ H ⟩)
                  → (i : is-equiv f)
                  → is-hom G H f
                  → is-hom H G (inverse f i)
inverses-are-homs G H f i h {x} {y} = γ
 where
  g : ⟨ H ⟩ → ⟨ G ⟩
  g = inverse f i

  η : f ∘ g ∼ id
  η = inverses-are-sections f i

  ε : g ∘ f ∼ id
  ε = inverses-are-retractions f i

  γ = g (x ·⟨ H ⟩ y)             ＝⟨ ap₂ (λ x y → g (x ·⟨ H ⟩ y)) ((η x)⁻¹) ((η y)⁻¹) ⟩
      g (f (g x) ·⟨ H ⟩ f (g y)) ＝⟨ ap g (h ⁻¹) ⟩
      g (f (g x ·⟨ G ⟩ g y))     ＝⟨ ε _ ⟩
      g x ·⟨ G ⟩ g y             ∎

inverses-are-homs' : (G : Group 𝓤) (H : Group 𝓥) (𝕗 : ⟨ G ⟩ ≃ ⟨ H ⟩)
                   → is-hom G H ⌜ 𝕗 ⌝
                   → is-hom H G (⌜ 𝕗 ⌝⁻¹)
inverses-are-homs' G H (f , i) = inverses-are-homs G H f i


Users of this module may wish to rename the following symbol _≅_ for
group ismorphism when importing it.


_≅_ : Group 𝓤 → Group 𝓥 → 𝓤 ⊔ 𝓥 ̇
G ≅ H = Σ f ꞉ (⟨ G ⟩ → ⟨ H ⟩) , is-iso G H f

≅-to-≃ : (G : Group 𝓤) (H : Group 𝓥) → G ≅ H → ⟨ G ⟩ ≃ ⟨ H ⟩
≅-to-≃ G H (f , f-is-iso) = (f , group-isos-are-equivs G H f-is-iso)

iso-to-equiv = ≅-to-≃

≅-to-≃-is-hom : (G : Group 𝓤) (H : Group 𝓥) (𝕗 : G ≅ H)
              → is-hom G H ⌜ ≅-to-≃ G H 𝕗 ⌝
≅-to-≃-is-hom G H (f , f-is-iso) = group-isos-are-homs G H f-is-iso

≅-refl : (G : Group 𝓤) → G ≅ G
≅-refl G = id , id-is-equiv ⟨ G ⟩ , id-is-hom G

≅-sym : (G : Group 𝓤) (H : Group 𝓥) → G ≅ H → H ≅ G
≅-sym G H (f , e , h) = inverse f e ,
                        inverses-are-equivs f e ,
                        inverses-are-homs G H f e h

≅-trans : (F : Group 𝓤) (G : Group 𝓥) (H : Group 𝓦)
        → F ≅ G → G ≅ H → F ≅ H
≅-trans F G H (f , i , h) (g , j , k) = g ∘ f ,
                                        ∘-is-equiv i j ,
                                        ∘-is-hom F G H f g h k

isomorphic-groups-have-equivalent-carriers : (G : Group 𝓤)
                                             (H : Group 𝓥)
                                           → G ≅ H → ⟨ G ⟩ ≃ ⟨ H ⟩
isomorphic-groups-have-equivalent-carriers G H (f , e , h) = (f , e)


If G is a group in a universe 𝓤 whose underlying set has a copy in a
universe 𝓥, then G itself has a copy in the universe 𝓥.


transport-Group-structure : (G : Group 𝓤) (Y : 𝓥 ̇ ) (f : Y → ⟨ G ⟩)
                          → is-equiv f
                          → Σ s ꞉ Group-structure Y , is-hom (Y , s) G f
transport-Group-structure {𝓤} {𝓥} (X , _·_ , i , a , e , l , r , ι)
                          Y  f f-is-equiv = γ
 where
  G : Group 𝓤
  G = X , _·_ , i , a , e , l , r , ι

  -- abstract (speeds things up but breaks some things - try opaque blocks)
  g : X → Y
  g = inverse f f-is-equiv

  η : f ∘ g ∼ id
  η = inverses-are-sections f f-is-equiv

  ε : g ∘ f ∼ id
  ε = inverses-are-retractions f f-is-equiv

  f-is-hom : {y y' : Y} → f (g (f y · f y')) ＝ f y · f y'
  f-is-hom {y} {y'} = η (f y · f y')
  -- end of abstract

  _•_ : Y → Y → Y
  y • y' = g (f y · f y')

  i' : is-set Y
  i' = equiv-to-set (f , f-is-equiv) i

  e' : Y
  e' = g e

  a' : associative _•_
  a' y₀ y₁ y₂ = g (f (g (f y₀ · f y₁)) · f y₂)         ＝⟨ ap g (f-is-hom ⁻¹) ⟩
                g (f (g (f (g (f y₀ · f y₁)) · f y₂))) ＝⟨ ε _ ⟩
                g (f (g (f y₀ · f y₁)) · f y₂)         ＝⟨ ap (λ - → g (- · f y₂)) (η _) ⟩
                g ((f y₀ · f y₁) · f y₂)               ＝⟨ ap g (a _ _ _) ⟩
                g (f y₀ · (f y₁ · f y₂))               ＝⟨ ap (λ - → g (f y₀ · -)) ((η _)⁻¹) ⟩
                g (f y₀ · f (g (f y₁ · f y₂)))         ∎

  l' : left-neutral e' _•_
  l' y = g (f (g e) · f y) ＝⟨ ap (λ - → g (- · f y)) (η e) ⟩
         g (e · f y)       ＝⟨ ap g (l (f y)) ⟩
         g (f y)           ＝⟨ ε y ⟩
         y                 ∎

  r' : right-neutral e' _•_
  r' y = g (f y · f (g e)) ＝⟨ ap (λ - → g (f y · -)) (η e) ⟩
         g (f y · e)       ＝⟨ ap g (r (f y)) ⟩
         g (f y)           ＝⟨ ε y ⟩
         y                 ∎


  ι' : (y : Y) → Σ y' ꞉ Y , (y' • y ＝ e') × (y • y' ＝ e')
  ι' y = g (pr₁ (ι (f y))) ,

        (g (f (g (pr₁ (ι (f y)))) · f y) ＝⟨ ap (λ - → g (- · f y)) (η _) ⟩
         g (pr₁ (ι (f y)) · f y)         ＝⟨ ap g (pr₁ (pr₂ (ι (f y)))) ⟩
         g e                             ∎) ,

        (g (f y · f (g (pr₁ (ι (f y))))) ＝⟨ ap (λ - → g (f y · -)) (η _) ⟩
         g (f y · id (pr₁ (ι (f y))))    ＝⟨ ap g (pr₂ (pr₂ (ι (f y)))) ⟩
         g e                             ∎)


  s : Group-structure Y
  s = _•_ , i' , a' , e' , l' , r' , ι'

  γ : Σ s ꞉ Group-structure Y , is-hom (Y , s) G f
  γ = s , f-is-hom

transport-Group-structure' : (G : Group 𝓤) (Y : 𝓥 ̇ ) (𝕗 : Y ≃ ⟨ G ⟩)
                           → Σ s ꞉ Group-structure Y , is-hom (Y , s) G ⌜ 𝕗 ⌝
transport-Group-structure' G Y 𝕗 =
 transport-Group-structure G Y ⌜ 𝕗 ⌝ ⌜ 𝕗 ⌝-is-equiv

group-copy : (G : Group 𝓤)
           → (Σ Y ꞉ 𝓥 ̇ , Y ≃ ⟨ G ⟩)
           → Σ H ꞉ Group 𝓥 , H ≅ G
group-copy {𝓤} {𝓥} G (Y , f , f-is-equiv) = γ
 where
  δ : (Σ s ꞉ Group-structure Y , is-hom (Y , s) G f)
    → Σ H ꞉ Group 𝓥 , H ≅ G
  δ (s , f-is-hom) = (Y , s) , f , f-is-equiv , f-is-hom

  γ : codomain δ
  γ = δ (transport-Group-structure G Y f f-is-equiv)

transport-Group-structure₁ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                          → X ≃ Y
                          → Group-structure X
                          → Group-structure Y
transport-Group-structure₁ {𝓤} {𝓥} {X} {Y} (f , f-is-equiv) s =
 pr₁ (transport-Group-structure (X , s) Y
       (inverse f f-is-equiv)
       (inverses-are-equivs f f-is-equiv))

open import UF.UniverseEmbedding

Lift-Group : ∀ {𝓤} 𝓥 → Group 𝓤 → Group (𝓤 ⊔ 𝓥)
Lift-Group {𝓤} 𝓥 (X , s) = Lift 𝓥 X , transport-Group-structure₁ (≃-Lift 𝓥 X) s

Lifted-Group-is-isomorphic : ∀ {𝓤} {𝓥} (G : Group 𝓤) → Lift-Group 𝓥 G ≅ G
Lifted-Group-is-isomorphic {𝓤} {𝓥} G =
 pr₂ (group-copy G (Lift 𝓥 ⟨ G ⟩ , Lift-is-universe-embedding 𝓥 ⟨ G ⟩))


Boolean groups.


boolean-groups-are-abelian' : {X : 𝓤 ̇ } (_·_ : X → X → X) (e : X)
                            → associative _·_
                            → left-neutral e _·_
                            → right-neutral e _·_
                            → ((x : X) → x · x ＝ e)
                            → commutative _·_
boolean-groups-are-abelian' _·_  e a ln rn b x y =
  xy                  ＝⟨ ap (x ·_) ((ln y)⁻¹) ⟩
  x · (e · y)         ＝⟨ ap (λ - → x · (- · y)) ((b xy)⁻¹) ⟩
  x · ((xy · xy) · y) ＝⟨ (a x (xy · xy) y)⁻¹ ⟩
  (x · (xy · xy)) · y ＝⟨ ap (_· y) ((a x xy xy)⁻¹) ⟩
  ((x · xy) · xy) · y ＝⟨ ap (λ - → (- · xy) · y) ((a x x y)⁻¹) ⟩
  ((xx · y) · xy) · y ＝⟨ ap (λ - → (( - · y) · xy) · y) (b x) ⟩
  ((e · y) · xy) · y  ＝⟨ ap (λ - → (- · xy) · y) (ln y) ⟩
  (y · xy) · y        ＝⟨ a y xy y ⟩
  y · (xy · y)        ＝⟨ ap (y ·_) (a x y y) ⟩
  y · (x · yy)        ＝⟨ ap (λ - → y · (x · -)) (b y) ⟩
  y · (x · e)         ＝⟨ ap (y ·_) (rn x) ⟩
  yx                  ∎

 where
  xx = x · x
  xy = x · y
  yx = y · x
  yy = y · y

is-boolean : Group 𝓤 → 𝓤 ̇
is-boolean G = (x : ⟨ G ⟩) → x ·⟨ G ⟩ x ＝ e⟨ G ⟩

is-abelian : Group 𝓤 → 𝓤 ̇
is-abelian G = (x y : ⟨ G ⟩) → x ·⟨ G ⟩ y ＝ y ·⟨ G ⟩ x

boolean-groups-are-abelian : (G : Group 𝓤)
                           → is-boolean G
                           → is-abelian G
boolean-groups-are-abelian (G , _·_ , _ , a , e , ln , rn , _) =
 boolean-groups-are-abelian' _·_ e a ln rn