open import Algebra.Group.Semidirect
open import Algebra.Group.Cat.Base
open import Algebra.Group.Concrete
open import Algebra.Group.Action
open import Algebra.Group

open import Cat.Univalent
open import Cat.Prelude

open import Homotopy.Connectedness

open ConcreteGroup
open is-group-hom
open Groups

module Algebra.Group.Concrete.Semidirect {ℓ} where

Semidirect products of concrete groups🔗

The construction of the semidirect product for concrete groups is quite natural: given a concrete group $G$ and an action $\phi :\mathbf{B}G\to \mathrm{ConcreteGroups}$ of $G$ on $H=\phi ({\bullet }_G)\text{,}$ we simply define $\mathbf{B}(G⋉H)$ as the $\Sigma \text{-type}$

pointed at $({\bullet }_G,{\bullet }_H)\text{.}$

module _ (G : ConcreteGroup ℓ) (φ : ⌞ B G ⌟ → ConcreteGroup ℓ) where

  H : ConcreteGroup ℓ
  H = φ (pt G)

  Semidirect-concrete : ConcreteGroup ℓ
  Semidirect-concrete .B .fst = Σ ⌞ B G ⌟ λ g → ⌞ B (φ g) ⌟
  Semidirect-concrete .B .snd = pt G , pt H

That this is a connected groupoid follows from standard results.

  Semidirect-concrete .has-is-connected = is-connected→is-connected∙ $
    Σ-is-n-connected 
      (is-connected∙→is-connected (G .has-is-connected))
      (λ a → is-connected∙→is-connected (φ a .has-is-connected))
  Semidirect-concrete .has-is-groupoid = Σ-is-hlevel 
    (G .has-is-groupoid)
    (λ a → φ a .has-is-groupoid)

In order to relate this with the definition of semidirect products for abstract groups, we show that the fundamental group ${\pi }_1\mathbf{B}(G⋉H)$ is the semidirect product ${\pi }_1\mathbf{B}G⋉{\pi }_1\mathbf{B}H\text{.}$

To that end, we start by defining the action of ${\pi }_1\mathbf{B}G$ on ${\pi }_1\mathbf{B}H$ induced by $\phi \text{.}$ Given a loop $p:{\bullet }_G\equiv {\bullet }_G\text{,}$ we can apply the function $x\mapsto {\pi }_1\mathbf{B}\phi (x)$ to it to get a loop ${\pi }_1\mathbf{B}H\equiv {\pi }_1\mathbf{B}H\text{,}$ which we then turn into an automorphism.

  π₁-φ : Action (Groups ℓ) (π₁B G) (π₁B H)
  π₁-φ .hom p = path→iso (ap (π₁B ⊙ φ) p)
  π₁-φ .preserves .pres-⋆ p q =
    path→iso (ap (π₁B ⊙ φ) (p ∙ q))                          ≡⟨ ap path→iso (ap-∙ (π₁B ⊙ φ) p q) ⟩≡
    path→iso (ap (π₁B ⊙ φ) p ∙ ap (π₁B ⊙ φ) q)               ≡⟨ path→iso-∙ (Groups ℓ) _ _ ⟩≡
    path→iso (ap (π₁B ⊙ φ) p) ∙Iso path→iso (ap (π₁B ⊙ φ) q) ∎

  π₁BG⋉π₁BH : Group ℓ
  π₁BG⋉π₁BH = Semidirect-product (π₁B G) (π₁B H) π₁-φ

  private module ⋉ = Group-on (π₁BG⋉π₁BH .snd)

The first step is to construct an equivalence between the underlying sets of ${\pi }_1\mathbf{B}(G⋉H)$ and ${\pi }_1\mathbf{B}G⋉{\pi }_1\mathbf{B}H\text{.}$ Since $\mathbf{B}(G⋉H)$ is a $\Sigma \text{-type,}$ its loops consist of pairs $(p:{\bullet }_G\equiv {\bullet }_G,q:{\bullet }_H{\equiv }_p{\bullet }_H)\text{,}$ where the second component is a dependent path over $p$ in the total space of $\phi \text{.}$ What we actually want is a pair of non-dependent loops, so we need to “realign” the second component by transporting one of its endpoints along $p\text{;}$ we do this by generalising on the endpoints and using path induction.

Note that we have a type $A=\mathbf{B}G\text{,}$ a type family $B(a)=\mathbf{B}\phi (a)\text{,}$ and a function $f:(a:A)\to B(a)$ given by $a\mapsto {\bullet }_{\phi (a)}\text{.}$ The following constructions work in this general setting.

  module _ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} (f : (a : A) → B a) where

    align
      : ∀ {a a' : A} (p : a ≡ a')
      → PathP (λ i → B (p i)) (f a) (f a') ≃ (f a' ≡ f a')
    align {a} =
      J (λ a' p → PathP (λ i → B (p i)) (f a) (f a') ≃ (f a' ≡ f a')) id≃

    align-refl
      : ∀ {a : A} (q : f a ≡ f a)
      → align (λ _ → a) # q ≡ q
    align-refl {a} = unext $
      J-refl (λ a' p → PathP (λ i → B (p i)) (f a) (f a') ≃ (f a' ≡ f a')) id≃

    Σ-align
      : ∀ {a a' : A}
      → ((a , f a) ≡ (a' , f a')) ≃ ((a ≡ a') × (f a' ≡ f a'))
    Σ-align = Iso→Equiv Σ-pathp-iso e⁻¹ ∙e Σ-ap-snd align

It remains to show that this equivalence is a group homomorphism — or rather a groupoid homomorphism, since we’ve generalised the endpoints. First, note that we can describe the action of $\phi$ on paths using a kind of dependent conjugation operation.

    conjP : ∀ {a a' : A} → (p : a ≡ a') → f a ≡ f a → f a' ≡ f a'
    conjP {a} p = transport (λ i → f a ≡ f a → f (p i) ≡ f (p i)) λ q → q

    conjP-refl : ∀ {a : A} → (q : f a ≡ f a) → conjP refl q ≡ q
    conjP-refl {a} = unext $ transport-refl {A = f a ≡ f a → _} λ q → q

Thus we have a composition operation on pairs of paths that generalises the multiplication in ${\pi }_1\mathbf{B}G⋉{\pi }_1\mathbf{B}H\text{.}$

    _∙⋉_
      : ∀ {a₀ a₁ a₂ : A}
      → (a₀ ≡ a₁) × (f a₁ ≡ f a₁)
      → (a₁ ≡ a₂) × (f a₂ ≡ f a₂)
      → (a₀ ≡ a₂) × (f a₂ ≡ f a₂)
    (p , q) ∙⋉ (p' , q') = p ∙ p' , conjP p' q ∙ q'

    Σ-align-∙
      : ∀ {a₀ a₁ a₂ : A}
      → (p  : (a₀ , f a₀) ≡ (a₁ , f a₁))
      → (p' : (a₁ , f a₁) ≡ (a₂ , f a₂))
      → Σ-align # (p ∙ p')
      ≡ Σ-align # p ∙⋉ Σ-align # p'

    Σ-align-∙ {a₀} {a₁} {a₂} p p' = J₂
      (λ a₀ a₂ p⁻¹ p' →
        ∀ (q : PathP (λ i → B (p⁻¹ (~ i))) (f a₀) (f a₁))
        → (q' : PathP (λ i → B (p' i)) (f a₁) (f a₂))
        → Σ-align # ((sym p⁻¹ ,ₚ q) ∙ (p' ,ₚ q'))
        ≡ Σ-align # (sym p⁻¹ ,ₚ q) ∙⋉ Σ-align # (p' ,ₚ q'))
      (λ q q' →
        Σ-align # ((refl ,ₚ q) ∙ (refl ,ₚ q'))                      ≡˘⟨ ap# Σ-align (ap-∙ (a₁ ,_) q q') ⟩≡˘
        Σ-align # (refl ,ₚ q ∙ q')                                  ≡⟨⟩
        refl        , align refl # (q ∙ q')                         ≡⟨ refl ,ₚ align-refl (q ∙ q') ⟩≡
        refl        , q ∙ q'                                        ≡˘⟨ refl ,ₚ ap₂ _∙_ (align-refl q) (align-refl q') ⟩≡˘
        refl        , align refl # q ∙ align refl # q'              ≡˘⟨ ∙-idl _ ,ₚ ap (_∙ align refl # q') (conjP-refl (align refl # q)) ⟩≡˘
        refl ∙ refl , conjP refl (align refl # q) ∙ align refl # q' ∎)
      (ap fst (sym p)) (ap fst p') (ap snd p) (ap snd p')

This concludes the proof that the constructions of the semidirect product of abstract and concrete groups agree over the equivalence between abstract and concrete groups.

  Semidirect-concrete-abstract : π₁B Semidirect-concrete ≡ π₁BG⋉π₁BH
  Semidirect-concrete-abstract = ∫-Path
    (total-hom (Σ-align (pt ⊙ φ) .fst)
      (record { pres-⋆ = Σ-align-∙ (pt ⊙ φ) }))
    (Σ-align (pt ⊙ φ) .snd)