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β Group
s are called
abstract.
record ConcreteGroup β : Type (lsuc β) where no-eta-equality constructor concrete-group field 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)
instance H-Level-B : β {n} β H-Level β B β (3 + n) H-Level-B = basic-instance 3 has-is-groupoid open ConcreteGroup instance Underlying-ConcreteGroup : Underlying (ConcreteGroup β) Underlying-ConcreteGroup {β} .Underlying.β-underlying = β Underlying-ConcreteGroup .β_β G = β B G β ConcreteGroup-path : {G H : ConcreteGroup β} β B G β‘ B H β G β‘ H ConcreteGroup-path {G = G} {H} p = go prop! prop! where go : PathP (Ξ» i β is-connectedβ (p i)) (G .has-is-connected) (H .has-is-connected) β PathP (Ξ» i β is-groupoid β p i β) (G .has-is-groupoid) (H .has-is-groupoid) β G β‘ H go c g i .B = p i go c g i .has-is-connected = c i go c g i .has-is-groupoid = g i
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.
opaque 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.
ConcreteGroups-Hom-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)) where 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 β private 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β‘Οβββ) public
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 ap
ply 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 Deloop
ing, 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 field 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}) ΟβF-is-split-eso ΟβB-is-equiv : is-equiv (ΟβB {β}) ΟβB-is-equiv = is-cat-equivalenceβequiv-on-objects ConcreteGroups-is-category Groups-is-category ΟβF-is-equivalence module ConcreteβAbstract {β} = Equiv (_ , ΟβB-is-equiv {β})
References
- Bezem, Marc, Ulrik Buchholtz, Pierre Cagne, BjΓΈrn Ian Dundas, and Daniel R. Grayson. 2023. βSymmetry.β https://github.com/UniMath/SymmetryBook.