# mathlibdocumentation

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.

## 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]-module k, 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.

noncomputable def group_cohomology.resolution.to_tensor_aux (k G : Type u) [comm_ring k] (n : ) [group G] :
((fin (n + 1) → G) →₀ k) →ₗ[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] :
(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.to_tensor_aux_single {k G : Type u} [comm_ring k] {n : } [group G] (f : fin (n + 1) → G) (m : k) :
m) = finsupp.single (f 0) m ⊗ₜ[k] finsupp.single (λ (i : fin n), (f i)⁻¹ * f i.succ) 1
theorem group_cohomology.resolution.to_tensor_aux_of_mul_action {k G : Type u} [comm_ring k] {n : } [group G] (g : G) (x : fin (n + 1) → G) :
(( (fin (n + 1) → G)) g) 1)) = (tensor_product.map ( G) g) 1) 1))
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) :
m ⊗ₜ[k] x) = ((finsupp.lift ((fin (n + 1) → G) →₀ k) k (fin n → G)) (λ (f : fin n → G), m)) x
theorem group_cohomology.resolution.of_tensor_aux_comm_of_mul_action {k G : Type u} [comm_ring k] {n : } [group G] (g h : G) (x : fin n → G) :
((tensor_product.map ( G) g) 1) 1 ⊗ₜ[k] 1)) = ( (fin (n + 1) → G)) g) 1 ⊗ₜ[k] 1))
theorem group_cohomology.resolution.to_tensor_aux_left_inv {k G : Type u} [comm_ring k] {n : } [group G] (x : (fin (n + 1) → G) →₀ k) :
= x
theorem group_cohomology.resolution.to_tensor_aux_right_inv {k G : Type u} [comm_ring k] {n : } [group G] (x : (G →₀ k) ((fin n → G) →₀ k)) :
= x
@[reducible]
noncomputable def Rep.of_mul_action (k : Type u) [comm_ring k] (G : Type u) [monoid G] (H : Type u) [ H] :
Rep k G

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.

noncomputable def group_cohomology.resolution.to_tensor (k G : Type u) [comm_ring k] (n : ) [group G] :
(fin (n + 1) → G) Rep.of G).tprod 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
noncomputable def group_cohomology.resolution.of_tensor (k G : Type u) [comm_ring k] (n : ) [group G] :
Rep.of G).tprod 1) (fin (n + 1) → 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) :
.hom) m) = finsupp.single (f 0) m ⊗ₜ[k] finsupp.single (λ (i : fin n), (f i)⁻¹ * f i.succ) 1
@[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) :
.hom) m ⊗ₜ[k] x) = ((finsupp.lift (fin (n + 1) → G)) k (fin n → G)) (λ (f : fin n → G), m)) x
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) :
.hom) (g ⊗ₜ[k] m) = ((finsupp.lift ((fin (n + 1) → G) →₀ k) k G) (λ (a : G), m)) g
noncomputable def group_cohomology.resolution.equiv_tensor (k G : Type u) [comm_ring k] (n : ) [group G] :
(fin (n + 1) → G) Rep.of G).tprod 1)

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
@[simp]
theorem group_cohomology.resolution.equiv_tensor_def (k G : Type u) [comm_ring k] (n : ) [group G] :
@[simp]
theorem group_cohomology.resolution.equiv_tensor_inv_def (k G : Type u) [comm_ring k] (n : ) [group G] :
noncomputable def group_cohomology.resolution.of_mul_action_basis_aux (k G : Type u) [comm_ring k] (n : ) [group G] :
G) ((fin n → G) →₀ k) ≃ₗ[] (fin (n + 1) → G)).as_module

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
noncomputable def group_cohomology.resolution.of_mul_action_basis (k G : Type u) [comm_ring k] (n : ) [group G] :
basis (fin n → G) G) (fin (n + 1) → G)).as_module

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

Equations
theorem group_cohomology.resolution.of_mul_action_free (k G : Type u) [comm_ring k] (n : ) [group G] :
(fin (n + 1) → G)).as_module