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 the underlying pointed type is denoted by analogy with the delooping of an abstract group; note that, here, the delooping is the chosen representation of so B is just a record field. We write 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)

The delooping of a group is a concrete group. In fact, we will prove later that all concrete groups arise as deloopings.

Concrete : ∀ {ℓ} → Group ℓ → ConcreteGroup ℓ
Concrete G .B = Deloop∙ G
Concrete G .has-is-connected = Deloop-is-connected
Concrete G .has-is-groupoid = squash

Another important example of a concrete group is the circle: the delooping of the integers.

  S¹-is-connected : is-connected∙ S¹∙
  S¹-is-connected = S¹-elim (inc refl) prop!

S¹-concrete : ConcreteGroup lzero
S¹-concrete .B = S¹∙
S¹-concrete .has-is-connected = S¹-is-connected
S¹-concrete .has-is-groupoid = hlevel 3

The category of concrete groups🔗

The notion of group homomorphism between two groups and gets translated to, on the “concrete” side, pointed maps

The pointedness condition ensures that these maps behave like abstract group homomorphisms; in particular, that they form a set.

  : (G : ConcreteGroup ℓ) (H : ConcreteGroup ℓ')
  → is-set (B G →∙ B H)
ConcreteGroups-Hom-set G H (f , ptf) (g , ptg) p q =
  Σ-set-square (λ _ → hlevel 2) (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 _ _ _ _ _ _

These naturally assemble into a category.

ConcreteGroups : ∀ ℓ → Precategory (lsuc ℓ) ℓ
ConcreteGroups ℓ .Ob = ConcreteGroup ℓ
ConcreteGroups _ .Hom G H = B G →∙ B H
ConcreteGroups _ .Hom-set = ConcreteGroups-Hom-set
The rest of the categorical structure is inherited from pointed functions, and univalence follows from the univalence of the universe of groupoids.
ConcreteGroups _ .id = id∙
ConcreteGroups _ ._∘_ = _∘∙_
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   ∎

  iso→equiv : ∀ {a b} → Isomorphism (ConcreteGroups ℓ) a b → ⌞ a ⌟ ≃ ⌞ b ⌟
  iso→equiv im = Iso→Equiv (im .to .fst ,
    iso (im .from .fst) (happly (ap fst (im .invl))) (happly (ap fst (im .invr))))

ConcreteGroups-is-category : is-category (ConcreteGroups ℓ)
ConcreteGroups-is-category .to-path im = ConcreteGroup-path $
  Σ-pathp (ua (iso→equiv im)) (path→ua-pathp _ (im .to .snd))
ConcreteGroups-is-category {ℓ} .to-path-over im = ≅-pathp (ConcreteGroups ℓ) _ _ $
  Σ-pathp (funextP λ _ → path→ua-pathp _ refl)
    (λ i j → path→ua-pathp (iso→equiv im) (λ i → im .to .snd (i ∧ j)) i)

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.

Since we’re dealing with groupoids, we can use the alternative definition of the fundamental group that avoids set truncations.

module _ (G : ConcreteGroup ℓ) where
  open π₁Groupoid (B G) (G .has-is-groupoid)
    renaming (π₁ to π₁B; π₁≡π₀₊₁ to π₁B≡π₀₊₁)

We define a functor from concrete groups to abstract groups. The object mapping is given by taking the fundamental group. Given a pointed map we can apply it to a loop on to get a loop on then, we use the fact that is pointed to get a loop on by conjugation.

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

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

π₁F .F₁ (f , ptf) .preserves .pres-⋆ x y =
  conj ptf ⌜ ap f (x ∙ y) ⌝             ≡⟨ ap! (ap-∙ f _ _) ⟩≡
  conj ptf (ap f x ∙ ap f y)            ≡⟨ conj-of-∙ _ _ _ ⟩≡
  conj ptf (ap f x) ∙ conj ptf (ap f y) ∎

π₁F .F-id = ext conj-refl
π₁F .F-∘ (f , ptf) (g , ptg) = ext λ x →
  conj (ap f ptg ∙ ptf) (ap (f ⊙ g) x)        ≡˘⟨ conj-∙ _ _ _ ⟩≡˘
  conj ptf ⌜ conj (ap f ptg) (ap (f ⊙ g) x) ⌝ ≡˘⟨ ap¡ (ap-conj f _ _) ⟩≡˘
  conj ptf (ap f (conj ptg (ap g x)))         ∎

We start by showing that π₁F 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.

π₁F-is-split-eso : is-split-eso (π₁F {ℓ})
π₁F-is-split-eso G .fst = Concrete G
π₁F-is-split-eso G .snd = path→iso (π₁B≡π₀₊₁ (Concrete G) ∙ sym (G≡π₁B G))

We now tackle the hard part: to prove that π₁F is fully faithful. In order to show that the action on morphisms is an equivalence, we need a way of “delooping” a group homomorphism into a pointed map

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 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 such that is contractible, conclude that holds and extract a map 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 to a point with a function that sends based paths ending at to based paths ending at with the additional constraint that must “extend” in the sense that a loop on the left can be factored out using

For the centre of contraction, we simply pick to be sending loops on to loops on

  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 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
    □≡□ = is-prop→pathp (λ i → hlevel 1) _ _

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 (i.e. that we need one more thing: that extends on the right. We get this essentially for free, by path induction, because ends at 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 is pointed by this lets us conclude that we have found a right inverse to

  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 .F₁ {G} {H} g ≡ f
  rinv = ext λ ω → pathp→conj (symP (f≡apg ω))

We are most of the way there. In order to get a proper equivalence, we must check that delooping gives us back the same pointed map

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

module Deloop-Hom-π₁F {G H : ConcreteGroup ℓ} (f : B G →∙ B H) where
  open Deloop-Hom {G = G} {H} (π₁F .F₁ {G} {H} 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 has it:

  C'-contr : is-contr (C' (pt G))
  C'-contr .centre .fst = f .snd ∙ sym (g .snd)
  C'-contr .centre .snd α = commutes→square $
    f .snd ∙ p ⌜ α ⌝                                ≡˘⟨ ap¡ (∙-idr _) ⟩≡˘
    f .snd ∙ ⌜ p (α ∙ refl) ⌝                       ≡⟨ ap! (f-p α refl) ⟩≡
    f .snd ∙ conj (f .snd) (ap (f .fst) α) ∙ p refl ≡˘⟨ ∙-extendl (∙-swapl (sym (conj-defn _ _))) ⟩≡˘
    ap (f .fst) α ∙ f .snd ∙ p refl                 ∎
  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, π₁F is fully faithful.

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

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

π₁F-is-equivalence : is-equivalence (π₁F {ℓ})
π₁F-is-equivalence = ff+split-eso→is-equivalence
  (λ {G} {H} → π₁F-is-ff {_} {G} {H})

π₁B-is-equiv : is-equiv (π₁B {ℓ})
π₁B-is-equiv = is-cat-equivalence→equiv-on-objects

module Concrete≃Abstract {ℓ} = Equiv (_ , π₁B-is-equiv {ℓ})