module Algebra.Group.Concrete.Abelian where

Concrete abelian groupsπŸ”—

A concrete abelian group is, unsurprisingly, a concrete group in which concatenation of loops at the base point is commutative.

module _ {β„“} (G : ConcreteGroup β„“) where
  is-concrete-abelian : Type β„“
  is-concrete-abelian = βˆ€ (p q : pt G ≑ pt G) β†’ p βˆ™ q ≑ q βˆ™ p

This is a property:

  open ConcreteGroup G using (H-Level-B)

  is-concrete-abelian-is-prop : is-prop is-concrete-abelian
  is-concrete-abelian-is-prop = hlevel 1

As an easy consequence, in an abelian group we can fill any square that has equal opposite sides.

    : is-concrete-abelian
    β†’ {x : ⌞ B G ⌟} β†’ (p q : x ≑ x) β†’ Square p q q p
  concrete-abelianβ†’square ab {x} = connectedβˆ™-elim-prop
    {P = Ξ» x β†’ (p q : x ≑ x) β†’ Square p q q p}
    (G .has-is-connected)
    (hlevel 1)
    (λ p q → commutes→square (ab p q))

Still unsurprisingly, the delooping of an abelian group is abelian.

  : βˆ€ {β„“} {G : Group β„“}
  β†’ is-commutative-group G β†’ is-concrete-abelian (Concrete G)
Deloop-abelian G-ab = βˆ™-comm _ G-ab

The circle is another example, being the delooping of

  : βˆ€ {β„“} {G : ConcreteGroup β„“}
  β†’ is-commutative-group (π₁B G) β†’ is-concrete-abelian G
π₁-abelianβ†’abelian {G = G} π₁G-ab = subst is-concrete-abelian
  (Concrete≃Abstract.Ξ· G)
  (Deloop-abelian π₁G-ab)

SΒΉ-concrete-abelian : is-concrete-abelian SΒΉ-concrete
SΒΉ-concrete-abelian = π₁-abelianβ†’abelian {G = SΒΉ-concrete}
  (subst is-commutative-group
    (sym π₁S¹≑℀)
    (Abelian→Group-on-abelian (℀-ab .snd)))

First abelian group cohomologyπŸ”—

When is a concrete abelian group, something interesting happens: for any other concrete group the set of pointed maps (i.e. group homomorphisms from to turns out to be equivalent to the set truncation of the type of unpointed maps,

This is a special case of a theorem that relates this set truncation with the set of orbits of the action of the inner automorphism group of on the set of group homomorphisms We do not prove this here, but see (Bezem et al. 2023, theorem 5.12.2). In the special case that is abelian, its inner automorphism group is trivial, and we can avoid quotienting.

In even fancier language, it is also a computation of the first cohomology group of with coefficients in hence we adopt the notation

HΒΉ[_,_] : βˆ€ {β„“ β„“'} β†’ ConcreteGroup β„“ β†’ ConcreteGroup β„“' β†’ Type (β„“ βŠ” β„“')
HΒΉ[ G , H ] = βˆ₯ (⌞ B G ⌟ β†’ ⌞ B H ⌟) βˆ₯β‚€

First, note that there is always a natural map that just forgets the pointing path.

  : βˆ€ {β„“ β„“'} (G : ConcreteGroup β„“) (H : ConcreteGroup β„“')
  β†’ (B G β†’βˆ™ B H) β†’ HΒΉ[ G , H ]
class G H (f , _) = inc f

Now assume is abelian; we will show that this map is injective and surjective, so that it is an equivalence of sets.

Surjectivity is the easy part: since is connected, every map is merely homotopic to a pointed map.

  class-surjective : is-surjective (class G H)
  class-surjective = βˆ₯-βˆ₯β‚€-elim (Ξ» _ β†’ hlevel 2) Ξ» f β†’ do
    ptf ← H .has-is-connected (f (pt G))
    inc ((f , ptf) , refl)

For injectivity, we restrict our attention to the case of two pointed maps whose underlying maps are definitionally equal. In other words, we prove that any two pointings of (say yield equal pointed maps.

In order to define our underlying homotopy, we proceed by induction: since is a pointed connected type, it suffices to give a path and to show that every loop respects this identification, in the sense of the following square:

Since our homotopy additionally has to be pointed, we know that we must have This is where the fact that is abelian comes in: the above square has equal opposite sides, so it automatically commutes.

    : βˆ€ f β†’ (p q : f (pt G) ≑ pt H)
    β†’ Path (B G β†’βˆ™ B H) (f , p) (f , q)
  class-injective f p q = Ξ£-pathp
    (funext E.elim)
    (transpose (symP (βˆ™β†’square'' E.elim-Ξ²-point)))
      Ξ± : f (pt G) ≑ f (pt G)
      Ξ± = p βˆ™ sym q

      coh : βˆ€ (l : pt G ≑ pt G) β†’ Square (ap f l) Ξ± Ξ± (ap f l)
      coh l = concrete-abelian→square H H-ab (ap f l) α

      module E = connectedβˆ™-elim-set {P = Ξ» g β†’ f g ≑ f g}
        (G .has-is-connected) (hlevel 2) Ξ± coh

By a quick path induction, we can conclude that class is an equivalence between sets.

  class-is-equiv : is-equiv (class G H)
  class-is-equiv = injective-surjective→is-equiv! (inj _ _) class-surjective
      inj : βˆ€ f g β†’ class G H f ≑ class G H g β†’ f ≑ g
      inj (f , ptf) (g , ptg) f≑g = βˆ₯-βˆ₯-rec
        (ConcreteGroups-Hom-set G H _ _)
        (Ξ» f≑g β†’ J (Ξ» g _ β†’ βˆ€ ptg β†’ (f , ptf) ≑ (g , ptg))
                   (class-injective f ptf)
                   f≑g ptg)
        (βˆ₯-βˆ₯β‚€ f≑g)

    : (B G β†’βˆ™ B H) ≃ HΒΉ[ G , H ]
    = class G H , class-is-equiv

Translating this across our equivalence of categories gives a similar statement for abstract groups.

  Deloop-hom-equiv : (Deloopβˆ™ G β†’βˆ™ Deloopβˆ™ H) ≃ Hom (Groups β„“) G H
  Deloop-hom-equiv = ff+split-esoβ†’hom-equiv π₁F
    (Ξ» {G} {H} β†’ π₁F-is-ff {_} {G} {H})
    G H .snd .snd

    : HΒΉ[ Concrete G , Concrete H ] ≃ Hom (Groups β„“) G H
  first-abelian-group-cohomology =
      (Concrete G) (Concrete H) (Deloop-abelian H-ab) e⁻¹
    βˆ™e Deloop-hom-equiv