The low-degree homology of a k
-linear G
-representation #
Let k
be a commutative ring and G
a group. This file contains specialised API for
the cycles and group homology of a k
-linear G
-representation A
in degrees 0, 1 and 2.
In RepresentationTheory/Homological/GroupHomology/Basic.lean
, we define the n
th group homology
of A
to be the homology of a complex inhomogeneousChains A
, whose objects are
(Fin n →₀ G) → A
; this is unnecessarily unwieldy in low degree.
Given an additive abelian group A
with an appropriate scalar action of G
, we provide support
for turning a finsupp f : G →₀ A
satisfying the 1-cycle identity into an element of the
cycles₁
of the representation on A
corresponding to the scalar action. We also do this for
0-boundaries, 1-boundaries, 2-cycles and 2-boundaries.
The file also contains an identification between the definitions in
RepresentationTheory/Homological/GroupHomology/Basic.lean
, groupHomology.cycles A n
, and the
cyclesₙ
in this file for n = 1, 2
, as well as an isomorphism groupHomology.cycles A 0 ≅ A.V
.
Moreover, we provide API for the natural maps cyclesₙ A → Hn A
for n = 1, 2
.
We show that when the representation on A
is trivial, H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A
.
Main definitions #
groupHomology.H0Iso A
: isomorphism betweenH₀(G, A)
and the coinvariantsA_G
of theG
-representation onA
.groupHomology.H1π A
: epimorphism from the 1-cycles (i.e.Z₁(G, A) := Ker(d₀ : (G →₀ A) → A
) toH₁(G, A)
.groupHomology.H2π A
: epimorphism from the 2-cycles (i.e.Z₂(G, A) := Ker(d₁ : (G² →₀ A) → (G →₀ A)
) toH₂(G, A)
.groupHomology.H1AddEquivOfIsTrivial
: an isomorphismH₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A
when the representation onA
is trivial.
The 0th object in the complex of inhomogeneous chains of A : Rep k G
is isomorphic
to A
as a k
-module.
Equations
- groupHomology.chainsIso₀ A = (Finsupp.LinearEquiv.finsuppUnique k (↑A.V) (Fin 0 → G)).toModuleIso
Instances For
The 2nd object in the complex of inhomogeneous chains of A : Rep k G
is isomorphic
to G² →₀ A
as a k
-module.
Equations
- groupHomology.chainsIso₂ A = (Finsupp.domLCongr (piFinTwoEquiv fun (x : Fin 2) => G)).toModuleIso
Instances For
The 3rd object in the complex of inhomogeneous chains of A : Rep k G
is isomorphic
to G³ → A
as a k
-module.
Equations
- groupHomology.chainsIso₃ A = (Finsupp.domLCongr ((Fin.consEquiv fun (i : Fin (2 + 1)) => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) => G)))).toModuleIso
Instances For
The 0th differential in the complex of inhomogeneous chains of A : Rep k G
, as a
k
-linear map (G →₀ A) → A
. It is defined by single g a ↦ ρ_A(g⁻¹)(a) - a.
Equations
- groupHomology.d₁₀ A = ModuleCat.ofHom ((Finsupp.lsum k) fun (g : G) => A.ρ g⁻¹ - LinearMap.id)
Instances For
The 0th differential in the complex of inhomogeneous chains of a G
-representation A
as a
linear map into the k
-submodule of A
spanned by elements of the form
ρ(g)(x) - x, g ∈ G, x ∈ A
.
Equations
Instances For
The 1st differential in the complex of inhomogeneous chains of A : Rep k G
, as a
k
-linear map (G² →₀ A) → (G →₀ A)
. It is defined by
a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁
.
Equations
- groupHomology.d₂₁ A = ModuleCat.ofHom ((Finsupp.lsum k) fun (g : G × G) => Finsupp.lsingle g.2 ∘ₗ A.ρ g.1⁻¹ - Finsupp.lsingle (g.1 * g.2) + Finsupp.lsingle g.1)
Instances For
The 2nd differential in the complex of inhomogeneous chains of A : Rep k G
, as a
k
-linear map (G³ →₀ A) → (G² →₀ A)
. It is defined by
a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Let C(G, A)
denote the complex of inhomogeneous chains of A : Rep k G
. This lemma
says d₁₀
gives a simpler expression for the 0th differential: that is, the following
square commutes:
C₁(G, A) --d 1 0--> C₀(G, A)
| |
| |
| |
v v
(G →₀ A) ----d₁₀----> A
where the vertical arrows are chainsIso₁
and chainsIso₀
respectively.
Let C(G, A)
denote the complex of inhomogeneous chains of A : Rep k G
. This lemma
says d₂₁
gives a simpler expression for the 1st differential: that is, the following
square commutes:
C₂(G, A) --d 2 1--> C₁(G, A)
| |
| |
| |
v v
(G² →₀ A) --d₂₁--> (G →₀ A)
where the vertical arrows are chainsIso₂
and chainsIso₁
respectively.
Let C(G, A)
denote the complex of inhomogeneous chains of A : Rep k G
. This lemma
says d₃₂
gives a simpler expression for the 2nd differential: that is, the following
square commutes:
C₃(G, A) --d 3 2--> C₂(G, A)
| |
| |
| |
v v
(G³ →₀ A) --d₃₂--> (G² →₀ A)
where the vertical arrows are chainsIso₃
and chainsIso₂
respectively.
The (exact) short complex (G →₀ A) ⟶ A ⟶ A.ρ.coinvariants
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A
.
Equations
- groupHomology.shortComplexH1 A = { X₁ := ModuleCat.of k (G × G →₀ ↑A.V), X₂ := ModuleCat.of k (G →₀ ↑A.V), X₃ := A.V, f := groupHomology.d₂₁ A, g := groupHomology.d₁₀ A, zero := ⋯ }
Instances For
The short complex (G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural inclusion B₁(G, A) →ₗ[k] Z₁(G, A)
.
Equations
Instances For
The natural inclusion B₂(G, A) →ₗ[k] Z₂(G, A)
.
Equations
Instances For
A finsupp ∑ aᵢ·gᵢ : G →₀ A
satisfies the 1-cycle condition if ∑ gᵢ⁻¹ • aᵢ = ∑ aᵢ
.
Equations
Instances For
A finsupp ∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A
satisfies the 2-cycle condition if
∑ (gᵢ⁻¹ • aᵢ)·hᵢ + aᵢ·gᵢ = ∑ aᵢ·gᵢhᵢ
.
Equations
- groupHomology.IsCycle₂ x = ((x.sum fun (g : G × G) (a : A) => Finsupp.single g.2 (g.1⁻¹ • a) + Finsupp.single g.1 a) = x.sum fun (g : G × G) (a : A) => Finsupp.single (g.1 * g.2) a)
Instances For
A term x : A
satisfies the 0-boundary condition if there exists a finsupp
∑ aᵢ·gᵢ : G →₀ A
such that ∑ gᵢ⁻¹ • aᵢ - aᵢ = x
.
Equations
Instances For
A finsupp x : G →₀ A
satisfies the 1-boundary condition if there's a finsupp
∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A
such that ∑ (gᵢ⁻¹ • aᵢ)·hᵢ - aᵢ·gᵢhᵢ + aᵢ·gᵢ = x
.
Equations
- groupHomology.IsBoundary₁ x = ∃ (y : G × G →₀ A), (y.sum fun (g : G × G) (a : A) => Finsupp.single g.2 (g.1⁻¹ • a) - Finsupp.single (g.1 * g.2) a + Finsupp.single g.1 a) = x
Instances For
A finsupp x : G × G →₀ A
satsfies the 2-boundary condition if there's a finsupp
∑ aᵢ·(gᵢ, hᵢ, jᵢ) : G × G × G →₀ A
such that
∑ (gᵢ⁻¹ • aᵢ)·(hᵢ, jᵢ) - aᵢ·(gᵢhᵢ, jᵢ) + aᵢ·(gᵢ, hᵢjᵢ) - aᵢ·(gᵢ, hᵢ) = x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a k
-module A
with a compatible DistribMulAction
of G
, and a term
x : A
satisfying the 0-boundary condition, this produces an element of the kernel of the quotient
map A → A_G
for the representation on A
induced by the DistribMulAction
.
Equations
Instances For
Given a k
-module A
with a compatible DistribMulAction
of G
, and a finsupp
x : G →₀ A
satisfying the 1-cycle condition, produces a 1-cycle for the representation on
A
induced by the DistribMulAction
.
Equations
- groupHomology.cyclesOfIsCycle₁ x hx = ⟨x, ⋯⟩
Instances For
Given a k
-module A
with a compatible DistribMulAction
of G
, and a finsupp
x : G →₀ A
satisfying the 1-boundary condition, produces a 1-boundary for the representation
on A
induced by the DistribMulAction
.
Equations
- groupHomology.boundariesOfIsBoundary₁ x hx = ⟨x, hx⟩
Instances For
Given a k
-module A
with a compatible DistribMulAction
of G
, and a finsupp
x : G × G →₀ A
satisfying the 2-cycle condition, produces a 2-cycle for the representation on
A
induced by the DistribMulAction
.
Equations
- groupHomology.cyclesOfIsCycle₂ x hx = ⟨x, ⋯⟩
Instances For
Given a k
-module A
with a compatible DistribMulAction
of G
, and a finsupp
x : G × G →₀ A
satisfying the 2-boundary condition, produces a 2-boundary for the
representation on A
induced by the DistribMulAction
.
Equations
- groupHomology.boundariesOfIsBoundary₂ x hx = ⟨x, hx⟩
Instances For
The 0-cycles of the complex of inhomogeneous chains of A
are isomorphic to A
.
Equations
Instances For
The arrow (G →₀ A) --d₁₀--> A
is isomorphic to the differential
(inhomogeneousChains A).d 1 0
of the complex of inhomogeneous chains of A
.
Equations
Instances For
The 0-cycles of the complex of inhomogeneous chains of A
are isomorphic to
A.ρ.coinvariants
, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A
is isomorphic to the 1st
short complex associated to the complex of inhomogeneous chains of A
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The short complex (G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A)
is isomorphic to the 2nd
short complex associated to the complex of inhomogeneous chains of A
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Shorthand for the 0th group homology of a k
-linear G
-representation A
, H₀(G, A)
,
defined as the 0th homology of the complex of inhomogeneous chains of A
.
Equations
- groupHomology.H0 A = groupHomology A 0
Instances For
The 0th group homology of A
, defined as the 0th homology of the complex of inhomogeneous
chains, is isomorphic to the invariants of the representation on A
.
Equations
Instances For
The quotient map from A
to H₀(G, A)
.
Equations
Instances For
Shorthand for the 1st group homology of a k
-linear G
-representation A
, H₁(G, A)
,
defined as the 1st homology of the complex of inhomogeneous chains of A
.
Equations
- groupHomology.H1 A = groupHomology A 1
Instances For
The quotient map from the 1-cycles of A
, as a submodule of G →₀ A
, to H₁(G, A)
.
Equations
Instances For
The 1st group homology of A
, defined as the 1st homology of the complex of inhomogeneous
chains, is isomorphic to cycles₁ A ⧸ boundaries₁ A
, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If a G
-representation on A
is trivial, this is the natural map H₁(G, A) → Gᵃᵇ ⊗[ℤ] A
sending ⟦single g a⟧
to ⟦g⟧ ⊗ₜ a
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Shorthand for the 2nd group homology of a k
-linear G
-representation A
, H₂(G, A)
,
defined as the 2nd homology of the complex of inhomogeneous chains of A
.
Equations
- groupHomology.H2 A = groupHomology A 2
Instances For
The quotient map from the 2-cycles of A
, as a submodule of G × G →₀ A
, to H₂(G, A)
.
Equations
Instances For
The 2nd group homology of A
, defined as the 2nd homology of the complex of inhomogeneous
chains, is isomorphic to cycles₂ A ⧸ boundaries₂ A
, which is a simpler type.
Equations
- One or more equations did not get rendered due to their size.