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 #
group_cohomology.resolution.to_tensor
group_cohomology.resolution.of_tensor
Rep.of_mul_action
group_cohomology.resolution.equiv_tensor
group_cohomology.resolution.of_mul_action_basis
classifying_space_universal_cover
group_cohomology.resolution.forget₂_to_Module_homotopy_equiv
group_cohomology.ProjectiveResolution
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
.
The k
-linear map from k[Gⁿ⁺¹]
to k[G] ⊗ₖ k[Gⁿ]
sending (g₀, ..., gₙ)
to g₀ ⊗ (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)
.
Equations
- group_cohomology.resolution.to_tensor_aux k G n = ⇑(finsupp.lift (tensor_product k (G →₀ k) ((fin n → G) →₀ k)) k (fin (n + 1) → G)) (λ (x : fin (n + 1) → G), finsupp.single (x 0) 1 ⊗ₜ[k] finsupp.single (λ (i : fin n), (x ↑i)⁻¹ * x i.succ) 1)
The k
-linear map from k[G] ⊗ₖ k[Gⁿ]
to k[Gⁿ⁺¹]
sending g ⊗ (g₁, ..., gₙ)
to
(g, gg₁, gg₁g₂, ..., gg₁...gₙ)
.
Equations
- group_cohomology.resolution.of_tensor_aux k G n = tensor_product.lift (⇑(finsupp.lift (((fin n → G) →₀ k) →ₗ[k] (fin (n + 1) → G) →₀ k) k G) (λ (g : G), ⇑(finsupp.lift ((fin (n + 1) → G) →₀ k) k (fin n → G)) (λ (f : fin n → G), finsupp.single (g • fin.partial_prod f) 1)))
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
- group_cohomology.resolution.to_tensor k G n = {hom := group_cohomology.resolution.to_tensor_aux k G n _inst_2, comm' := _}
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
- group_cohomology.resolution.of_tensor k G n = {hom := group_cohomology.resolution.of_tensor_aux k G n _inst_2, comm' := _}
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
- group_cohomology.resolution.equiv_tensor k G n = Action.mk_iso {to_fun := (group_cohomology.resolution.to_tensor_aux k G n).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(group_cohomology.resolution.of_tensor_aux k G n), left_inv := _, right_inv := _}.to_Module_iso _
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
- group_cohomology.resolution.of_mul_action_basis_aux k G n = {to_fun := (Rep.equivalence_Module_monoid_algebra.functor.map_iso (group_cohomology.resolution.equiv_tensor k G n).symm).to_linear_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := (Rep.equivalence_Module_monoid_algebra.functor.map_iso (group_cohomology.resolution.equiv_tensor k G n).symm).to_linear_equiv.inv_fun, left_inv := _, right_inv := _}
A k[G]
-basis of k[Gⁿ⁺¹]
, coming from the k[G]
-linear isomorphism
k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹].
Equations
- group_cohomology.resolution.of_mul_action_basis k G n = (algebra.tensor_product.basis (monoid_algebra k G) {repr := linear_equiv.refl k ((fin n → G) →₀ k) (finsupp.module (fin n → G) k)}).map (group_cohomology.resolution.of_mul_action_basis_aux k G n)
The simplicial G
-set sending [n]
to Gⁿ⁺¹
equipped with the diagonal action of G
.
Equations
- classifying_space_universal_cover G = {obj := λ (n : simplex_categoryᵒᵖ), Action.of_mul_action G (fin ((opposite.unop n).len + 1) → G), map := λ (m n : simplex_categoryᵒᵖ) (f : m ⟶ n), {hom := λ (x : (Action.of_mul_action G (fin ((opposite.unop m).len + 1) → G)).V), x ∘ ⇑(simplex_category.hom.to_order_hom f.unop), comm' := _}, map_id' := _, map_comp' := _}
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
As a simplicial set, cech_nerve_terminal_from
of a monoid G
is isomorphic to the universal
cover of the classifying space of G
as a simplicial set.
Equations
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
- classifying_space_universal_cover.comp_forget_augmented G = category_theory.simplicial_object.augment (classifying_space_universal_cover G ⋙ category_theory.forget (Action (Type u) (Mon.of G))) (⊤_ Type u) (category_theory.limits.terminal.from ((classifying_space_universal_cover G ⋙ category_theory.forget (Action (Type u) (Mon.of G))).obj (opposite.op (simplex_category.mk 0)))) _
The augmented Čech nerve of the map from fin 1 → G
to the terminal object in Type u
has an
extra degeneracy.
Equations
- classifying_space_universal_cover.extra_degeneracy_augmented_cech_nerve G = category_theory.arrow.augmented_cech_nerve.extra_degeneracy (category_theory.arrow.mk (category_theory.limits.terminal.from G)) {section_ := λ (x : (𝟭 (Type u)).obj (category_theory.arrow.mk (category_theory.limits.terminal.from G)).right), 1, id' := _}
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
- classifying_space_universal_cover.extra_degeneracy_comp_forget_augmented G = simplicial_object.augmented.extra_degeneracy.of_iso (category_theory.comma.iso_mk (category_theory.cech_nerve_terminal_from.iso G ≪≫ classifying_space_universal_cover.cech_nerve_terminal_from_iso_comp_forget G) (category_theory.iso.refl (category_theory.arrow.mk (category_theory.limits.terminal.from G)).augmented_cech_nerve.right) _) (classifying_space_universal_cover.extra_degeneracy_augmented_cech_nerve G)
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
.
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.
The standard resolution of k
as a trivial representation, defined as the alternating
face map complex of a simplicial k
-linear G
-representation.
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
- group_cohomology.resolution.d k G n = ⇑(finsupp.lift ((fin n → G) →₀ k) k (fin (n + 1) → G)) (λ (g : fin (n + 1) → G), finset.univ.sum (λ (p : fin (n + 1)), finsupp.single (g ∘ ⇑(p.succ_above)) ((-1) ^ ↑p)))
The n
th 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.
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
- group_cohomology.resolution.forget₂_to_Module_homotopy_equiv k G = (homotopy_equiv.of_iso (group_cohomology.resolution.comp_forget_augmented_iso k G).symm).trans ((classifying_space_universal_cover.extra_degeneracy_comp_forget_augmented_to_Module k G).homotopy_equiv.trans (homotopy_equiv.of_iso ((chain_complex.single₀ (Module k)).map_iso (finsupp.linear_equiv.finsupp_unique k k (⊤_ Type u)).to_Module_iso)))
The hom of k
-linear G
-representations k[G¹] → k
sending ∑ nᵢgᵢ ↦ ∑ nᵢ
.
Equations
- group_cohomology.resolution.ε k G = {hom := finsupp.total (fin 1 → G) ↥((Rep.of representation.trivial).V) k (λ (f : fin 1 → G), 1), comm' := _}
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
- group_cohomology.resolution.ε_to_single₀ k G = ⇑(((group_cohomology.resolution k G).to_single₀_equiv (Rep.of representation.trivial)).symm) ⟨group_cohomology.resolution.ε k G _inst_2, _⟩
Instances for group_cohomology.resolution.ε_to_single₀
The standard projective resolution of k
as a trivial k
-linear G
-representation.
Given a k
-linear G
-representation V
, Extⁿ(k, V)
(where k
is a trivial k
-linear
G
-representation) is isomorphic to the n
th cohomology group of Hom(P, V)
, where P
is the
standard resolution of k
called group_cohomology.resolution k G
.
Equations
- group_cohomology.Ext_iso k G V n = let this : opposite.unop ((((category_theory.linear_yoneda k (Rep k G)).obj V).right_op.left_derived n).obj (Rep.of representation.trivial)) ≅ opposite.unop ((homology_functor (Module k)ᵒᵖ (complex_shape.down ℕ) n).obj ((((category_theory.linear_yoneda k (Rep k G)).obj V).right_op.map_homological_complex (complex_shape.down ℕ)).obj (group_cohomology.ProjectiveResolution k G).complex)) := (((category_theory.linear_yoneda k (Rep k G)).obj V).right_op.left_derived_obj_iso n (group_cohomology.ProjectiveResolution k G)).unop.symm in this