mathlib documentation

representation_theory.group_cohomology_resolution

The structure of the k[G]-module k[Gⁿ] #

This file contains facts about an important k[G]-module structure on k[Gⁿ], where k is a commutative ring and G is a group. The module structure arises from the representation G →* End(k[Gⁿ]) induced by the diagonal action of G on Gⁿ.

In particular, we define an isomorphism of k-linear G-representations between k[Gⁿ⁺¹] and k[G] ⊗ₖ k[Gⁿ] (on which G acts by ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x).

This allows us to define a k[G]-basis on k[Gⁿ⁺¹], by mapping the natural k[G]-basis of k[G] ⊗ₖ k[Gⁿ] along the isomorphism.

We then define the standard resolution of k as a trivial representation, by taking 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 group_cohomology.ProjectiveResolution, the standard projective resolution of k as a trivial k-linear G-representation.

Main definitions #

Implementation notes #

We express k[G]-module structures on a module k-module V using the representation definition. We avoid using instances module (G →₀ k) V so that we do not run into possible scalar action diamonds.

We also use the category theory library to bundle the type k[Gⁿ] - or more generally k[H] when H has G-action - and the representation together, as a term of type Rep k G, and call it Rep.of_mul_action k G H. This enables us to express the fact that certain maps are G-equivariant by constructing morphisms in the category Rep k G, i.e., representations of G over k.

noncomputable def group_cohomology.resolution.to_tensor_aux (k G : Type u) [comm_ring k] (n : ) [group G] :
((fin (n + 1) G) →₀ k) →ₗ[k] tensor_product k (G →₀ k) ((fin n G) →₀ k)

The k-linear map from k[Gⁿ⁺¹] to k[G] ⊗ₖ k[Gⁿ] sending (g₀, ..., gₙ) to g₀ ⊗ (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ).

Equations
noncomputable def group_cohomology.resolution.of_tensor_aux (k G : Type u) [comm_ring k] (n : ) [group G] :
tensor_product k (G →₀ k) ((fin n G) →₀ k) →ₗ[k] (fin (n + 1) G) →₀ k

The k-linear map from k[G] ⊗ₖ k[Gⁿ] to k[Gⁿ⁺¹] sending g ⊗ (g₁, ..., gₙ) to (g, gg₁, gg₁g₂, ..., gg₁...gₙ).

Equations
theorem group_cohomology.resolution.of_tensor_aux_single {k G : Type u} [comm_ring k] {n : } [group G] (g : G) (m : k) (x : (fin n G) →₀ k) :
noncomputable def group_cohomology.resolution.to_tensor (k G : Type u) [comm_ring k] (n : ) [group G] :

A hom 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ₙ).

Equations
noncomputable def group_cohomology.resolution.of_tensor (k G : Type u) [comm_ring k] (n : ) [group G] :

A hom of k-linear representations of G from k[G] ⊗ₖ k[Gⁿ] (on which G acts by ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x) to k[Gⁿ⁺¹] sending g ⊗ (g₁, ..., gₙ) to (g, gg₁, gg₁g₂, ..., gg₁...gₙ).

Equations
@[simp]
theorem group_cohomology.resolution.to_tensor_single {k G : Type u} [comm_ring k] {n : } [group G] (f : fin (n + 1) G) (m : k) :
@[simp]
theorem group_cohomology.resolution.of_tensor_single {k G : Type u} [comm_ring k] {n : } [group G] (g : G) (m : k) (x : (fin n G) →₀ k) :
theorem group_cohomology.resolution.of_tensor_single' {k G : Type u} [comm_ring k] {n : } [group G] (g : G →₀ k) (x : fin n G) (m : k) :
noncomputable def group_cohomology.resolution.equiv_tensor (k G : Type u) [comm_ring k] (n : ) [group G] :

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ₙ).

Equations

The k[G]-linear isomorphism k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹], where the k[G]-module structure on the lefthand side is tensor_product.left_module, whilst that of the righthand side comes from representation.as_module. Allows us to use basis.algebra_tensor_product to get a k[G]-basis of the righthand side.

Equations

A k[G]-basis of k[Gⁿ⁺¹], coming from the k[G]-linear isomorphism k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹].

Equations

The simplicial G-set sending [n] to Gⁿ⁺¹ equipped with the diagonal action of G.

Equations

When the category is G-Set, cech_nerve_terminal_from 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

The free functor Type u ⥤ Module.{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

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 ⥤ Module.{u} k, the resulting augmented simplicial k-module has an extra degeneracy.

Equations
noncomputable def group_cohomology.resolution (k G : Type u) [comm_ring k] [monoid G] :

The standard resolution of k as a trivial representation, defined as the alternating face map complex of a simplicial k-linear G-representation.

Equations
noncomputable def group_cohomology.resolution.d (k : Type u) [comm_ring k] (G : Type u) (n : ) :
((fin (n + 1) G) →₀ k) →ₗ[k] (fin n G) →₀ k

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
@[simp]
theorem group_cohomology.resolution.d_of {k : Type u} [comm_ring k] {G : Type u} {n : } (c : fin (n + 1) G) :
noncomputable def group_cohomology.resolution.X_iso (k G : Type u) [comm_ring k] [monoid G] (n : ) :

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

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

If we apply the free functor Type u ⥤ Module.{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

The hom of k-linear G-representations k[G¹] → k sending ∑ nᵢgᵢ ↦ ∑ nᵢ.

Equations

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
Instances for group_cohomology.resolution.ε_to_single₀

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 group_cohomology.resolution k G.

Equations