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 homomorphismHᵢ(G, X₃) ⟶ Hⱼ(G, X₁)
associated to an exact sequence0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0
of representations.
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₂'
Instances For
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)
Instances For
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₁'
Instances For
Exactness of Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) ⟶ Hⱼ(G, X₂)
.
Exactness of Hᵢ(G, X₁) ⟶ Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃)
.
Exactness of Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁)
.
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
Instances For
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 ⋯
Instances For
Stated for readability of δ₁_apply
.