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.
TODO #
- Define the one and two cycles and boundaries as submodules of
G →₀ A
andG × G →₀ A
, and provide maps toH1
andH2
.
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 1st object in the complex of inhomogeneous chains of A : Rep k G
is isomorphic
to G →₀ A
as a k
-module.
Equations
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 sends 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 sends 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 sends
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.