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 nth 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 →₀ AandG × G →₀ A, and provide maps toH1andH2.
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.