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.
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
TODO #
- Use the freeness of
k[Gⁿ⁺¹]
to build a projective resolution of the (trivial)k[G]
-modulek
, and so develop group cohomology.
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)))
Given a G
-action on H
, this is k[H]
bundled with the natural representation
G →* End(k[H])
as a term of type Rep k 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
- 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)