module Algebra.Group.Concrete where

Concrete groups🔗

In homotopy type theory, we can give an alternative definition of groups: they are the pointed, connected groupoids. The idea is that those groupoids contain exactly the same information as their fundamental group.

Such groups are dubbed concrete, because they represent the groups of symmetries of a given object (the base point); by opposition, “algebraic” Groups are called abstract.

record ConcreteGroup ℓ : Type (lsuc ℓ) where
  constructor concrete-group
    B                : Type∙ ℓ
    has-is-connected : is-connected∙ B
    has-is-groupoid  : is-groupoid ⌞ B ⌟

  pt : ⌞ B ⌟
  pt = B .snd

Given a concrete group GG, the underlying pointed type is denoted BG\mathbf{B} G, by analogy with the delooping of an abstract group; note that, here, the delooping is the chosen representation of GG, so B is just a record field. We write ∙G\bullet_{G} for the base point.

Concrete groups are pointed connected types, so they enjoy the following elimination principle, which will be useful later:

  B-elim-contr : {P : ⌞ B ⌟ → Type ℓ′}
               → is-contr (P pt)
               → ∀ x → P x
  B-elim-contr {P = P} c = connected∙-elim-prop {P = P} has-is-connected
    (is-contr→is-prop c) (c .centre)

A central example of a concrete group is the circle: the delooping of the integers.

S¹-is-groupoid : is-groupoid S¹
S¹-is-groupoid = connected∙-elim-prop S¹-is-connected hlevel!
               $ connected∙-elim-prop S¹-is-connected hlevel!
               $ is-hlevel≃ 2 ΩS¹≃integers (hlevel 2)

S¹-concrete : ConcreteGroup lzero
S¹-concrete .B = S¹ , base
S¹-concrete .has-is-connected = S¹-is-connected
S¹-concrete .has-is-groupoid = S¹-is-groupoid

The category of concrete groups🔗

Concrete groups naturally form a category, where the morphisms are given by pointed maps BG→BH\mathbf{B} G \to \mathbf{B} H.

ConcreteGroups : ∀ ℓ → Precategory (lsuc ℓ) ℓ
ConcreteGroups ℓ .Ob = ConcreteGroup ℓ
ConcreteGroups _ .Hom G H = B G →∙ B H

We immediately see one reason why the pointedness condition is needed: without it, the morphisms between concrete groups would not form a set.

ConcreteGroups _ .Hom-set G H (f , ptf) (g , ptg) p q =
  Σ-set-square hlevel! (funext-square (B-elim-contr G square))
    open ConcreteGroup H using (H-Level-B)
    square : is-contr ((λ j → p j .fst (pt G)) ≡ (λ j → q j .fst (pt G)))
    square .centre i j = hcomp (∂ i ∨ ∂ j) λ where
      k (k = i0) → pt H
      k (i = i0) → p j .snd (~ k)
      k (i = i1) → q j .snd (~ k)
      k (j = i0) → ptf (~ k)
      k (j = i1) → ptg (~ k)
    square .paths _ = H .has-is-groupoid _ _ _ _ _ _
The rest of the categorical structure is inherited from functions and paths in a straightforward way.
ConcreteGroups _ .id = (λ x → x) , refl
ConcreteGroups _ ._∘_ (f , ptf) (g , ptg) = f ⊙ g , ap f ptg ∙ ptf
ConcreteGroups _ .idr f = Σ-pathp refl (∙-idl _)
ConcreteGroups _ .idl f = Σ-pathp refl (∙-idr _)
ConcreteGroups _ .assoc (f , ptf) (g , ptg) (h , pth) = Σ-pathp refl $
  ⌜ ap f (ap g pth ∙ ptg) ⌝ ∙ ptf   ≡⟨ ap! (ap-∙ f _ _) ⟩≡
  (ap (f ⊙ g) pth ∙ ap f ptg) ∙ ptf ≡⟨ sym (∙-assoc _ _ _) ⟩≡
  ap (f ⊙ g) pth ∙ ap f ptg ∙ ptf   ∎

We can check that ConcreteGroups is a univalent category: this essentially follows from the univalence of the universe of groupoids.

Concrete vs. abstract🔗

Our goal is now to prove that concrete groups and abstract groups are equivalent, in the sense that there is an equivalence of categories between ConcreteGroups and Groups.

To make the following developments easier, we define a version of πₙ₊₁ 0 that does not use the set truncation. Indeed, there’s no need since we’re dealing with groupoids: each loop space is already a set.

π₁B : ConcreteGroup ℓ → Group ℓ
π₁B G = to-group mk where
  open make-group
  mk : make-group (pt G ≡ pt G)
  mk .group-is-set = G .has-is-groupoid _ _
  mk .unit = refl
  mk .mul = _∙_
  mk .inv = sym
  mk .assoc = ∙-assoc
  mk .invl = ∙-invl
  mk .idl = ∙-idl

π₁≡π₀₊₁ : {G : ConcreteGroup ℓ} → π₁B G ≡ πₙ₊₁ 0 (B G)
π₁≡π₀₊₁ {G = G} = ∫-Path Groups-equational
  (total-hom inc (record { pres-⋆ = λ _ _ → refl }))
  (∥-∥₀-idempotent (G .has-is-groupoid _ _))

We define a functor from concrete groups to abstract groups. The object mapping is given by taking the fundamental group. Given a pointed map f:BG→BHf : \mathbf{B} G \to \mathbf{B} H, we can apply it to a loop on ∙G\bullet_{G} to get a loop on f(∙G)f(\bullet_{G}); then, we use the fact that ff is pointed to get a loop on ∙H\bullet_{H}.

Π₁ : Functor (ConcreteGroups ℓ) (Groups ℓ)
Π₁ .F₀ = π₁B
Π₁ .F₁ (f , ptf) .hom x = sym ptf ·· ap f x ·· ptf

By some simple path yoga, this preserves multiplication, and the construction is functorial:

Π₁ .F₁ (f , ptf) .preserves .pres-⋆ x y =
  (sym ptf ·· ⌜ ap f (x ∙ y) ⌝ ·· ptf)                    ≡⟨ ap! (ap-∙ f _ _) ⟩≡
  (sym ptf ·· ap f x ∙ ap f y ·· ptf)                     ≡˘⟨ ··-chain ⟩≡˘
  (sym ptf ·· ap f x ·· ptf) ∙ (sym ptf ·· ap f y ·· ptf) ∎

Π₁ .F-id = Homomorphism-path λ _ → sym (··-filler _ _ _)
Π₁ .F-∘ (f , ptf) (g , ptg) = Homomorphism-path λ x →
  (sym (ap f ptg ∙ ptf) ·· ap (f ⊙ g) x ·· (ap f ptg ∙ ptf))         ≡˘⟨ ··-stack ⟩≡˘
  (sym ptf ·· ⌜ ap f (sym ptg) ·· ap (f ⊙ g) x ·· ap f ptg ⌝ ·· ptf) ≡˘⟨ ap¡ (ap-·· f _ _ _) ⟩≡˘
  (sym ptf ·· ap f (sym ptg ·· ap g x ·· ptg) ·· ptf)                ∎

We start by showing that Π₁ is split essentially surjective. This is the easy part: to build a concrete group out of an abstract group, we simply take its Delooping, and use the fact that the fundamental group of the delooping recovers the original group.

Π₁-is-split-eso : is-split-eso (Π₁ {ℓ})
Π₁-is-split-eso G .fst = concrete-group (Deloop G , base) Deloop-is-connected squash
Π₁-is-split-eso G .snd = path→iso (π₁≡π₀₊₁ ∙ sym (G≡π₁B G))

We now tackle the hard part: to prove that Π₁ is fully faithful. In order to show that the action on morphisms is an equivalence, we need a way of “delooping” a group homomorphism f:π1(BG)→π1(BH)f : \pi_1(\mathbf{B} G) \to \pi_1(\mathbf{B} H) into a pointed map BG→BH\mathbf{B} G \to \mathbf{B} H.

module Deloop-Hom {G H : ConcreteGroup ℓ} (f : Groups ℓ .Hom (π₁B G) (π₁B H)) where
  open ConcreteGroup H using (H-Level-B)

How can we build such a map? All we know about BG\mathbf{B} G is that it is a pointed connected groupoid, and thus that it comes with the elimination principle B-elim-contr. This suggests that we need to define a type family C:BG→TypeC : \mathbf{B} G \to \mathrm{Type} such that C(∙G)C(\bullet_{G}) is contractible, conclude that ∀x.C(x)\forall x. C(x) holds and extract a map BG→BH\mathbf{B} G \to \mathbf{B} H from that. The following construction is adapted from (Bezem et al. 2023, sec. 4.10):

  record C (x : ⌞ G ⌟) : Type ℓ where
    constructor mk
      y : ⌞ H ⌟
      p : pt G ≡ x → pt H ≡ y
      f-p : (ω : pt G ≡ pt G) (α : pt G ≡ x) → p (ω ∙ α) ≡ f # ω ∙ p α

Our family sends a point x:BGx : \mathbf{B} G to a point y:BHy : \mathbf{B} H with a function pp that sends based paths ending at xx to based paths ending at yy, with the additional constraint that pp must “extend” ff, in the sense that a loop on the left can be factored out using ff.

For the centre of contraction, we simply pick pp to be ff, sending loops on ∙G\bullet_{G} to loops on ∙H\bullet_{H}.

  C-contr : is-contr (C (pt G))
  C-contr .centre .C.y = pt H
  C-contr .centre .C.p = f .hom
  C-contr .centre .C.f-p = f .preserves .pres-⋆

As it turns out, such a structure is entirely determined by the pair (y,p(refl):∙H≡y)(y, p(\mathrm{refl}) : \bullet_{H} \equiv y), which means it is contractible.

  C-contr .paths (mk y p f-p) i = mk (pt≡y i) (funextP f≡p i) (□≡□ i) where
    pt≡y : pt H ≡ y
    pt≡y = p refl

    f≡p : ∀ ω → Square refl (f # ω) (p ω) (p refl)
    f≡p ω = ∙-filler (f # ω) (p refl) ▷ (sym (f-p ω refl) ∙ ap p (∙-idr ω))

    □≡□ : PathP (λ i → ∀ ω α → f≡p (ω ∙ α) i ≡ f # ω ∙ f≡p α i) (f .preserves .pres-⋆) f-p
    □≡□ = prop!

We can now apply the elimination principle and unpack our data:

  c : ∀ x → C x
  c = B-elim-contr G C-contr

  g : B G →∙ B H
  p : {x : ⌞ G ⌟} → pt G ≡ x → pt H ≡ g .fst x

  g .fst x = c x .C.y
  g .snd = sym (p refl)

  p {x} = c x .C.p

  f-p : (ω : pt G ≡ pt G) (α : pt G ≡ pt G) → p (ω ∙ α) ≡ f # ω ∙ p α
  f-p = c (pt G) .C.f-p

In order to show that this is a delooping of ff (i.e. that Π1(g)≡f\Pi_1(g) \equiv f), we need one more thing: that pp extends gg on the right. We get this essentially for free, by path induction, because p(α)p(α) ends at g(x)g(x) by definition.

  p-g : (α : pt G ≡ pt G) {x' : ⌞ G ⌟} (l : pt G ≡ x')
      → p (α ∙ l) ≡ p α ∙ ap (g .fst) l
  p-g α = J (λ _ l → p (α ∙ l) ≡ p α ∙ ap (g .fst) l)
    (ap p (∙-idr _) ∙ sym (∙-idr _))

Since gg is pointed by p(refl)p(\mathrm{refl}), this lets us conclude that we have found a right inverse to Π1\Pi_1:

  f≡apg : (ω : pt G ≡ pt G) → Square (p refl) (f # ω) (ap (g .fst) ω) (p refl)
  f≡apg ω = commutes→square $
    p refl ∙ ap (g .fst) ω ≡˘⟨ p-g refl ω ⟩≡˘
    p (refl ∙ ω)           ≡˘⟨ ap p ∙-id-comm ⟩≡˘
    p (ω ∙ refl)           ≡⟨ f-p ω refl ⟩≡
    f # ω ∙ p refl         ∎

  rinv : Π₁ .F₁ g ≡ f
  rinv = Homomorphism-path λ ω → sym (··-unique' (symP (f≡apg ω)))

We are most of the way there. In order to get a proper equivalence, we must check that delooping Π1(f)\Pi_1(f) gives us back the same pointed map ff.

We use the same trick, building upon what we’ve done before: start by defining a family that asserts that pxp_x agrees with ff all the way, not just on loops:

module Deloop-Hom-Π₁ {G H : ConcreteGroup ℓ} (f : B G →∙ B H) where
  open Deloop-Hom {G = G} {H} (Π₁ .F₁ f) public
  open ConcreteGroup H using (H-Level-B)

  C′ : ∀ x → Type _
  C′ x = Σ (f .fst x ≡ g .fst x) λ eq
       → (α : pt G ≡ x) → Square (f .snd) (ap (f .fst) α) (p α) eq

This is a property, and ∙G\bullet_{G} has it:

  C′-contr : is-contr (C′ (pt G))
  C′-contr .centre .fst = f .snd ∙ sym (g .snd)
  C′-contr .centre .snd α = transport (sym Square≡double-composite-path) $
    ··-∙-assoc ∙ sym (f-p α refl) ∙ ap p (∙-idr _)
  C′-contr .paths (eq , eq-paths) = Σ-prop-path! $
    sym (∙-unique _ (transpose (eq-paths refl)))

Using the elimination principle again, we get enough information about g to conclude that it is equal to f, so that we have a left inverse.

  c′ : ∀ x → C′ x
  c′ = B-elim-contr G C′-contr

  g≡f : ∀ x → g .fst x ≡ f .fst x
  g≡f x = sym (c′ x .fst)

The homotopy g≡f is pointed by definition, but we need to bend the path into a Square:

  β : g≡f (pt G) ≡ sym (f .snd ∙ sym (g .snd))
  β = ap (sym ⊙ fst) (sym (C′-contr .paths (c′ (pt G))))

  ptg≡ptf : Square (g≡f (pt G)) (g .snd) (f .snd) refl
  ptg≡ptf i j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → ∙-filler (f .snd) (sym (g .snd)) (~ j) (~ i)
    k (i = i0) → g .snd j
    k (i = i1) → f .snd (j ∧ k)
    k (j = i0) → β (~ k) i
    k (j = i1) → f .snd (~ i ∨ k)

  linv : g ≡ f
  linv = funext∙ g≡f ptg≡ptf

Phew. At last, Π₁ is fully faithful.

Π₁-is-ff : is-fully-faithful (Π₁ {ℓ})
Π₁-is-ff {ℓ} {G} {H} = is-iso→is-equiv $
  iso Deloop-Hom.g Deloop-Hom.rinv (Deloop-Hom-Π₁.linv {G = G} {H})

We’ve shown that Π₁ is fully faithful and essentially surjective; this lets us conclude with the desired equivalence.

Concrete≃Abstract : is-equivalence (Π₁ {ℓ})
Concrete≃Abstract = ff+split-eso→is-equivalence Π₁-is-ff Π₁-is-split-eso