Documentation

Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Long exact sequence in group homology #

Given a commutative ring k and a group G, this file shows that a short exact sequence of k-linear G-representations 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 induces a short exact sequence of complexes 0 ⟶ inhomogeneousChains X₁ ⟶ inhomogeneousChains X₂ ⟶ inhomogeneousChains X₃ ⟶ 0.

Since the homology of inhomogeneousChains Xᵢ is the group homology of Xᵢ, this allows us to specialize API about long exact sequences to group homology.

Main definitions #

@[reducible, inline]
noncomputable abbrev groupHomology.mapShortComplex₁ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : } (hij : j + 1 = i) :

The short complex Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) ⟶ Hⱼ(G, X₂) associated to an exact sequence of representations 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0.

Equations
Instances For
    @[reducible, inline]

    The short complex Hᵢ(G, X₁) ⟶ Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃) associated to a short complex of representations X₁ ⟶ X₂ ⟶ X₃.

    Equations
    Instances For
      @[reducible, inline]
      noncomputable abbrev groupHomology.mapShortComplex₃ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : } (hij : j + 1 = i) :

      The short complex Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) associated to an exact sequence of representations 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0.

      Equations
      Instances For
        theorem groupHomology.mapShortComplex₁_exact {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : } (hij : j + 1 = i) :

        Exactness of Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) ⟶ Hⱼ(G, X₂).

        Exactness of Hᵢ(G, X₁) ⟶ Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃).

        theorem groupHomology.mapShortComplex₃_exact {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : } (hij : j + 1 = i) :

        Exactness of Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁).

        @[reducible, inline]
        noncomputable abbrev groupHomology.δ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (i j : ) (hij : j + 1 = i) :

        The connecting homomorphism Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) associated to an exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of representations.

        Equations
        Instances For
          @[reducible, inline]
          noncomputable abbrev groupHomology.cyclesMkOfCompEqD {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : } {y : (Fin iG) →₀ X.X₂.V} {x : (Fin jG) →₀ X.X₁.V} (hx : (Finsupp.mapRange.linearMap (ModuleCat.Hom.hom X.f.hom)) x = (CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains X.X₂).d i j)) y) :
          (cycles X.X₁ j)

          Given an exact sequence of G-representations 0 ⟶ X₁ ⟶f X₂ ⟶g X₃ ⟶ 0, this expresses an n-chain x : Gⁿ →₀ X₁ such that f ∘ x ∈ Bₙ(G, X₂) as a cycle. Stated for readability of δ_apply.

          Equations
          Instances For