Long exact sequence in group cohomology

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 ⟶ inhomogeneousCochains X₁ ⟶ inhomogeneousCochains X₂ ⟶ inhomogeneousCochains X₃ ⟶ 0.

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

Main definitions

• groupCohomology.δ hX i j hij: the connecting homomorphism Hⁱ(G, X₃) ⟶ Hʲ(G, X₁) associated to an exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of representations.

theorem groupCohomology.map_cochainsFunctor_shortExact {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) : (X.map (cochainsFunctor k G)).ShortExact

@[reducible, inline]

noncomputable abbrev groupCohomology.mapShortComplex₁ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : ℕ} (hij : i + 1 = j) : CategoryTheory.ShortComplex (ModuleCat k)

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

• groupCohomology.mapShortComplex₁ hX hij = (HomologicalComplex.HomologySequence.snakeInput ⋯ i j hij).L₂'

@[reducible, inline]

noncomputable abbrev groupCohomology.mapShortComplex₂ {k G : Type u} [CommRing k] [Group G] (X : CategoryTheory.ShortComplex (Rep k G)) (i : ℕ) : CategoryTheory.ShortComplex (ModuleCat k)

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

Equations

• groupCohomology.mapShortComplex₂ X i = X.map (groupCohomology.functor k G i)

@[reducible, inline]

noncomputable abbrev groupCohomology.mapShortComplex₃ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : ℕ} (hij : i + 1 = j) : CategoryTheory.ShortComplex (ModuleCat k)

The short complex Hⁱ(G, X₂) ⟶ Hⁱ(G, X₃) ⟶ Hʲ(G, X₁).

Equations

• groupCohomology.mapShortComplex₃ hX hij = (HomologicalComplex.HomologySequence.snakeInput ⋯ i j hij).L₁'

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

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

theorem groupCohomology.mapShortComplex₂_exact {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (i : ℕ) : (mapShortComplex₂ X i).Exact

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

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

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

@[reducible, inline]

noncomputable abbrev groupCohomology.δ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (i j : ℕ) (hij : i + 1 = j) : groupCohomology X.X₃ i ⟶ groupCohomology X.X₁ j

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

Equations

• groupCohomology.δ hX i j hij = ⋯.δ i j hij

theorem groupCohomology.epi_δ_of_isZero {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (n : ℕ) (h : CategoryTheory.Limits.IsZero (groupCohomology X.X₂ (n + 1))) : CategoryTheory.Epi (δ hX n (n + 1) ⋯)

theorem groupCohomology.mono_δ_of_isZero {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (n : ℕ) (h : CategoryTheory.Limits.IsZero (groupCohomology X.X₂ n)) : CategoryTheory.Mono (δ hX n (n + 1) ⋯)

theorem groupCohomology.isIso_δ_of_isZero {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (n : ℕ) (h : CategoryTheory.Limits.IsZero (groupCohomology X.X₂ n)) (hs : CategoryTheory.Limits.IsZero (groupCohomology X.X₂ (n + 1))) : CategoryTheory.IsIso (δ hX n (n + 1) ⋯)

@[reducible, inline]

noncomputable abbrev groupCohomology.cocyclesMkOfCompEqD {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : ℕ} {y : (Fin i → G) → ↑X.X₂.V} {x : (Fin j → G) → ↑X.X₁.V} (hx : ⇑(CategoryTheory.ConcreteCategory.hom X.f.hom) ∘ x = (CategoryTheory.ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y) : ↑(cocycles X.X₁ j)

Given an exact sequence of G-representations 0 ⟶ X₁ ⟶f X₂ ⟶g X₃ ⟶ 0, this expresses an n + 1-cochain x : Gⁿ⁺¹ → X₁ such that f ∘ x ∈ Bⁿ⁺¹(G, X₂) as a cocycle. Stated for readability of δ_apply.

Equations

• groupCohomology.cocyclesMkOfCompEqD hX hx = groupCohomology.cocyclesMk x ⋯

theorem groupCohomology.δ_apply {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : ℕ} (hij : i + 1 = j) (z : (Fin i → G) → ↑X.X₃.V) (hz : (CategoryTheory.ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i j)) z = 0) (y : (Fin i → G) → ↑X.X₂.V) (hy : (CategoryTheory.ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z) (x : (Fin j → G) → ↑X.X₁.V) (hx : ⇑(CategoryTheory.ConcreteCategory.hom X.f.hom) ∘ x = (CategoryTheory.ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y) : (CategoryTheory.ConcreteCategory.hom (δ hX i j hij)) ((CategoryTheory.ConcreteCategory.hom (π X.X₃ i)) (cocyclesMk z ⋯)) = (CategoryTheory.ConcreteCategory.hom (π X.X₁ j)) (cocyclesMkOfCompEqD hX hx)

theorem groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {y : ↑X.X₂.V} {x : G → ↑X.X₁.V} (hx : ⇑(CategoryTheory.ConcreteCategory.hom X.f.hom) ∘ x = (CategoryTheory.ConcreteCategory.hom (d₀₁ X.X₂)) y) : x ∈ cocycles₁ X.X₁

Stated for readability of δ₀_apply.

@[deprecated groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁ (since := "2025-07-02")]

theorem groupCohomology.mem_oneCocycles_of_comp_eq_dZero {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {y : ↑X.X₂.V} {x : G → ↑X.X₁.V} (hx : ⇑(CategoryTheory.ConcreteCategory.hom X.f.hom) ∘ x = (CategoryTheory.ConcreteCategory.hom (d₀₁ X.X₂)) y) : x ∈ cocycles₁ X.X₁

Alias of groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁.

---

Stated for readability of δ₀_apply.

theorem groupCohomology.δ₀_apply {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (z : ↥X.X₃.ρ.invariants) (y : ↑X.X₂.V) (hy : (CategoryTheory.ConcreteCategory.hom X.g.hom) y = ↑z) (x : G → ↑X.X₁.V) (hx : ⇑(CategoryTheory.ConcreteCategory.hom X.f.hom) ∘ x = (CategoryTheory.ConcreteCategory.hom (d₀₁ X.X₂)) y) : (CategoryTheory.ConcreteCategory.hom (δ hX 0 1 ⋯)) ((CategoryTheory.ConcreteCategory.hom (H0Iso X.X₃).inv) z) = (CategoryTheory.ConcreteCategory.hom (H1π X.X₁)) ⟨x, ⋯⟩

theorem groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {y : G → ↑X.X₂.V} {x : G × G → ↑X.X₁.V} (hx : ⇑(CategoryTheory.ConcreteCategory.hom X.f.hom) ∘ x = (CategoryTheory.ConcreteCategory.hom (d₁₂ X.X₂)) y) : x ∈ cocycles₂ X.X₁

Stated for readability of δ₁_apply.

@[deprecated groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂ (since := "2025-07-02")]

theorem groupCohomology.mem_twoCocycles_of_comp_eq_dOne {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {y : G → ↑X.X₂.V} {x : G × G → ↑X.X₁.V} (hx : ⇑(CategoryTheory.ConcreteCategory.hom X.f.hom) ∘ x = (CategoryTheory.ConcreteCategory.hom (d₁₂ X.X₂)) y) : x ∈ cocycles₂ X.X₁

Alias of groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂.

---

Stated for readability of δ₁_apply.

theorem groupCohomology.δ₁_apply {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (z : ↥(cocycles₁ X.X₃)) (y : G → ↑X.X₂.V) (hy : ⇑(CategoryTheory.ConcreteCategory.hom X.g.hom) ∘ y = ⇑z) (x : G × G → ↑X.X₁.V) (hx : ⇑(CategoryTheory.ConcreteCategory.hom X.f.hom) ∘ x = (CategoryTheory.ConcreteCategory.hom (d₁₂ X.X₂)) y) : (CategoryTheory.ConcreteCategory.hom (δ hX 1 2 ⋯)) ((CategoryTheory.ConcreteCategory.hom (H1π X.X₃)) z) = (CategoryTheory.ConcreteCategory.hom (H2π X.X₁)) ⟨x, ⋯⟩