The standard and bar resolutions of k as a trivial k-linear G-representation #
Given a commutative ring k and a group G, this file defines two projective resolutions of k
as a trivial k-linear G-representation.
The first one, the standard resolution, has objects k[Gⁿ⁺¹] equipped with the diagonal
representation, and differential defined by (g₀, ..., gₙ) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ).
We define this as the alternating face map complex associated to an appropriate simplicial
k-linear G-representation. This simplicial object is the linearization of the simplicial
G-set given by the universal cover of the classifying space of G, EG. We prove this
simplicial G-set EG is isomorphic to the Čech nerve of the natural arrow of G-sets
G ⟶ {pt}.
We then use this isomorphism to deduce that as a complex of k-modules, the standard resolution
of k as a trivial G-representation is homotopy equivalent to the complex with k at 0 and 0
elsewhere.
Putting this material together allows us to define Rep.standardResolution, the
standard projective resolution of k as a trivial k-linear G-representation.
We then construct the bar resolution. The nth object in this complex is the representation on
Gⁿ →₀ k[G] defined pointwise by the left regular representation on k[G]. The differentials are
defined by sending (g₀, ..., gₙ) to
g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁) for
j = 0, ... , n - 1.
In RepresentationTheory.Rep we define an isomorphism Rep.diagonalSuccIsoFree between
k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G]) sending (g₀, ..., gₙ) ↦ g₀·(g₀⁻¹g₁, ..., gₙ₋₁⁻¹gₙ).
We show that this isomorphism defines a commutative square with the bar resolution differential and
the standard resolution differential, and thus conclude that the bar resolution differential
squares to zero and that Rep.diagonalSuccIsoFree defines an isomorphism between the two
complexes. We carry the exactness properties across this isomorphism to conclude the bar resolution
is a projective resolution too, in Rep.barResolution.
In RepresentationTheory/Homological/Group(Co)homology/Basic.lean, we then use
Rep.barResolution to define the inhomogeneous (co)chains of a representation, useful for
computing group (co)homology.
Main definitions #
Alias of Action.diagonalSuccIsoTensorTrivial.
An isomorphism of G-sets Gⁿ⁺¹ ≅ G × Gⁿ, where G acts by left multiplication on Gⁿ⁺¹ and
G but trivially on Gⁿ. The map sends (g₀, ..., gₙ) ↦ (g₀, (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)),
and the inverse is (g₀, (g₁, ..., gₙ)) ↦ (g₀, g₀g₁, g₀g₁g₂, ..., g₀g₁...gₙ).
Equations
Instances For
Alias of Rep.diagonalSuccIsoTensorTrivial.
An isomorphism of k-linear representations of G from k[Gⁿ⁺¹] to k[G] ⊗ₖ k[Gⁿ] (on
which G acts by ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x) sending (g₀, ..., gₙ) to
g₀ ⊗ (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ). The inverse sends g₀ ⊗ (g₁, ..., gₙ) to
(g₀, g₀g₁, ..., g₀g₁...gₙ).
Equations
Instances For
Alias of Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single.
Alias of Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left.
Alias of Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right.
The k[G]-linear isomorphism k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹], where the k[G]-module structure on
the lefthand side is TensorProduct.leftModule, whilst that of the righthand side comes from
Representation.asModule. Allows us to use Algebra.TensorProduct.basis to get a k[G]-basis
of the righthand side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A k[G]-basis of k[Gⁿ⁺¹], coming from the k[G]-linear isomorphism
k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹].
Instances For
Alias of Representation.free_asModule_free.
The simplicial G-set sending [n] to Gⁿ⁺¹ equipped with the diagonal action of G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
When the category is G-Set, cechNerveTerminalFrom of G with the left regular action is
isomorphic to EG, the universal cover of the classifying space of G as a simplicial G-set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
As a simplicial set, cechNerveTerminalFrom of a monoid G is isomorphic to the universal
cover of the classifying space of G as a simplicial set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The universal cover of the classifying space of G as a simplicial set, augmented by the map
from Fin 1 → G to the terminal object in Type u.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The augmented Čech nerve of the map from Fin 1 → G to the terminal object in Type u has an
extra degeneracy.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The universal cover of the classifying space of G as a simplicial set, augmented by the map
from Fin 1 → G to the terminal object in Type u, has an extra degeneracy.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The free functor Type u ⥤ ModuleCat.{u} k applied to the universal cover of the classifying
space of G as a simplicial set, augmented by the map from Fin 1 → G to the terminal object
in Type u.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If we augment the universal cover of the classifying space of G as a simplicial set by the
map from Fin 1 → G to the terminal object in Type u, then apply the free functor
Type u ⥤ ModuleCat.{u} k, the resulting augmented simplicial k-module has an extra
degeneracy.
Equations
Instances For
The standard resolution of k as a trivial representation, defined as the alternating
face map complex of a simplicial k-linear G-representation.
Equations
Instances For
Alias of Rep.standardComplex.
The standard resolution of k as a trivial representation, defined as the alternating
face map complex of a simplicial k-linear G-representation.
Instances For
The k-linear map underlying the differential in the standard resolution of k as a trivial
k-linear G-representation. It sends (g₀, ..., gₙ) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ).
Equations
- Rep.standardComplex.d k G n = (Finsupp.lift ((Fin n → G) →₀ k) k (Fin (n + 1) → G)) fun (g : Fin (n + 1) → G) => ∑ p : Fin (n + 1), Finsupp.single (g ∘ p.succAbove) ((-1) ^ ↑p)
Instances For
The nth object of the standard resolution of k is definitionally isomorphic to k[Gⁿ⁺¹]
equipped with the representation induced by the diagonal action of G.
Equations
- Rep.standardComplex.xIso k G n = CategoryTheory.Iso.refl ((Rep.standardComplex k G).X n)
Instances For
Simpler expression for the differential in the standard resolution of k as a
G-representation. It sends (g₀, ..., gₙ₊₁) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ₊₁).
The standard resolution of k as a trivial representation as a complex of k-modules.
Equations
- Rep.standardComplex.forget₂ToModuleCat k G = ((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).obj (Rep.standardComplex k G)
Instances For
If we apply the free functor Type u ⥤ ModuleCat.{u} k to the universal cover of the
classifying space of G as a simplicial set, then take the alternating face map complex, the result
is isomorphic to the standard resolution of the trivial G-representation k as a complex of
k-modules.
Equations
Instances For
As a complex of k-modules, the standard resolution of the trivial G-representation k is
homotopy equivalent to the complex which is k at 0 and 0 elsewhere.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The hom of k-linear G-representations k[G¹] → k sending ∑ nᵢgᵢ ↦ ∑ nᵢ.
Equations
- Rep.standardComplex.ε k G = { hom := ModuleCat.ofHom (Finsupp.linearCombination k fun (x : Fin 1 → G) => 1), comm := ⋯ }
Instances For
The homotopy equivalence of complexes of k-modules between the standard resolution of k as
a trivial G-representation, and the complex which is k at 0 and 0 everywhere else, acts as
∑ nᵢgᵢ ↦ ∑ nᵢ : k[G¹] → k at 0.
The chain map from the standard resolution of k to k[0] given by ∑ nᵢgᵢ ↦ ∑ nᵢ in
degree zero.
Equations
- Rep.standardComplex.εToSingle₀ k G = ((Rep.standardComplex k G).toSingle₀Equiv (Rep.trivial k G k)).symm ⟨Rep.standardComplex.ε k G, ⋯⟩
Instances For
The standard projective resolution of k as a trivial k-linear G-representation.
Equations
- Rep.standardResolution k G = { complex := Rep.standardComplex k G, projective := ⋯, hasHomology := ⋯, π := Rep.standardComplex.εToSingle₀ k G, quasiIso := ⋯ }
Instances For
Alias of Rep.standardResolution.
The standard projective resolution of k as a trivial k-linear G-representation.
Instances For
Given a k-linear G-representation V, Extⁿ(k, V) (where k is a trivial k-linear
G-representation) is isomorphic to the nth cohomology group of Hom(P, V), where P is the
standard resolution of k called standardComplex k G.
Equations
- Rep.standardResolution.extIso k G V n = (Rep.standardResolution k G).isoExt n V
Instances For
Alias of Rep.standardResolution.extIso.
Given a k-linear G-representation V, Extⁿ(k, V) (where k is a trivial k-linear
G-representation) is isomorphic to the nth cohomology group of Hom(P, V), where P is the
standard resolution of k called standardComplex k G.
Instances For
The differential from Gⁿ⁺¹ →₀ k[G] to Gⁿ →₀ k[G] in the bar resolution of k as a trivial
k-linear G-representation. It sends (g₀, ..., gₙ) to
g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁) for
j = 0, ... , n - 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The projective resolution of k as a trivial k-linear G-representation with nth
differential (Gⁿ⁺¹ →₀ k[G]) → (Gⁿ →₀ k[G]) sending (g₀, ..., gₙ) to
g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁) for
j = 0, ... , n - 1.
Equations
- Rep.barComplex k G = ChainComplex.of (fun (n : ℕ) => Rep.free k G (Fin n → G)) (fun (n : ℕ) => Rep.barComplex.d k G n) ⋯
Instances For
Isomorphism between the bar resolution and standard resolution, with nth map
(Gⁿ →₀ k[G]) → k[Gⁿ⁺¹] sending (g₁, ..., gₙ) ↦ (1, g₁, g₁g₂, ..., g₁...gₙ).
Equations
- Rep.barComplex.isoStandardComplex k G = HomologicalComplex.Hom.isoOfComponents (fun (i : ℕ) => (Rep.diagonalSuccIsoFree k G i).symm) ⋯
Instances For
The chain complex barComplex k G as a projective resolution of k as a trivial
k-linear G-representation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a k-linear G-representation V, Extⁿ(k, V) (where k is the trivial k-linear
G-representation) is isomorphic to the nth cohomology group of Hom(P, V), where P is the
bar resolution of k.
Equations
- Rep.barResolution.extIso k G V n = (Rep.barResolution k G).isoExt n V