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

• groupHomology.δ 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 groupHomology.map_chainsFunctor_shortExact {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) : (X.map (chainsFunctor k G)).ShortExact

@[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) : 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

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

@[reducible, inline]

noncomputable abbrev groupHomology.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

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

@[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) : 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

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

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) : (mapShortComplex₁ hX hij).Exact

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 : ℕ) : (mapShortComplex₂ X i).Exact

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) : (mapShortComplex₃ hX hij).Exact

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) : groupHomology X.X₃ i ⟶ groupHomology 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

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

theorem groupHomology.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 (groupHomology X.X₂ n)) : CategoryTheory.Epi (δ hX (n + 1) n ⋯)

theorem groupHomology.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 (groupHomology X.X₂ (n + 1))) : CategoryTheory.Mono (δ hX (n + 1) n ⋯)

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

@[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 i → G) →₀ ↑X.X₂.V} {x : (Fin j → G) →₀ ↑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

• groupHomology.cyclesMkOfCompEqD hX hx = groupHomology.cyclesMk j ((ComplexShape.down ℕ).next j) ⋯ x ⋯

theorem groupHomology.δ_apply {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {i j : ℕ} (hij : j + 1 = i) (z : (Fin i → G) →₀ ↑X.X₃.V) (hz : (CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains X.X₃).d i j)) z = 0) (y : (Fin i → G) →₀ ↑X.X₂.V) (hy : (CategoryTheory.ConcreteCategory.hom ((chainsMap (MonoidHom.id G) X.g).f i)) y = z) (x : (Fin j → G) →₀ ↑X.X₁.V) (hx : (Finsupp.mapRange.linearMap (ModuleCat.Hom.hom X.f.hom)) x = (CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains X.X₂).d i j)) y) : (CategoryTheory.ConcreteCategory.hom (δ hX i j hij)) ((CategoryTheory.ConcreteCategory.hom (π X.X₃ i)) (cyclesMk i j ⋯ z ⋯)) = (CategoryTheory.ConcreteCategory.hom (π X.X₁ j)) (cyclesMkOfCompEqD hX hx)

theorem groupHomology.δ₀_apply {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (z : ↥(cycles₁ X.X₃)) (y : G →₀ ↑X.X₂.V) (hy : (Finsupp.mapRange.linearMap (ModuleCat.Hom.hom X.g.hom)) y = ↑z) (x : ↑X.X₁.V) (hx : (CategoryTheory.ConcreteCategory.hom X.f.hom) x = (CategoryTheory.ConcreteCategory.hom (d₁₀ X.X₂)) y) : (CategoryTheory.ConcreteCategory.hom (δ hX 1 0 ⋯)) ((CategoryTheory.ConcreteCategory.hom (H1π X.X₃)) z) = (CategoryTheory.ConcreteCategory.hom (H0π X.X₁)) x

theorem groupHomology.mem_cycles₁_of_comp_eq_d₂₁ {k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) {y : G × G →₀ ↑X.X₂.V} {x : G →₀ ↑X.X₁.V} (hx : (Finsupp.mapRange.linearMap (ModuleCat.Hom.hom X.f.hom)) x = (CategoryTheory.ConcreteCategory.hom (d₂₁ X.X₂)) y) : x ∈ cycles₁ X.X₁

Stated for readability of δ₁_apply.

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