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 GroupCohomology.projectiveResolution, the standard projective resolution of k as a trivial k-linear G-representation.

Main definitions

• GroupCohomology.Resolution.actionDiagonalSucc
• GroupCohomology.Resolution.diagonalSucc
• GroupCohomology.Resolution.ofMulActionBasis
• classifyingSpaceUniversalCover
• GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv
• GroupCohomology.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.ofMulAction 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.

def GroupCohomology.Resolution.actionDiagonalSucc (G : Type u) [Group G] (n : ℕ) : Action.diagonal G (n + 1) ≅ CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) { V := Fin n → G, ρ := 1 }

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

• One or more equations did not get rendered due to their size.

theorem GroupCohomology.Resolution.actionDiagonalSucc_hom_apply {G : Type u} [Group G] {n : ℕ} (f : Fin (n + 1) → G) : Action.Hom.hom (GroupCohomology.Resolution.actionDiagonalSucc G n).hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))

theorem GroupCohomology.Resolution.actionDiagonalSucc_inv_apply {G : Type u} [Group G] {n : ℕ} (g : G) (f : Fin n → G) : Action.Hom.hom (Type u) CategoryTheory.types (MonCat.of G) (CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) { V := Fin n → G, ρ := 1 }) (Action.diagonal G (n + 1)) (GroupCohomology.Resolution.actionDiagonalSucc G n).inv (g, f) = g • Fin.partialProd f

def GroupCohomology.Resolution.diagonalSucc (k : Type u) (G : Type u) [CommRing k] [Group G] (n : ℕ) : Rep.diagonal k G (n + 1) ≅ CategoryTheory.MonoidalCategory.tensorObj (Rep.leftRegular k G) (Rep.trivial k G ((Fin n → G) →₀ k))

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

theorem GroupCohomology.Resolution.diagonalSucc_hom_single {k : Type u} {G : Type u} [CommRing k] {n : ℕ} [Group G] (f : Fin (n + 1) → G) (a : k) : (↑(GroupCohomology.Resolution.diagonalSucc k G n).hom.hom fun₀ | f => a) = (fun₀ | f 0 => 1) ⊗ₜ[k] fun₀ | fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i) => a

theorem GroupCohomology.Resolution.diagonalSucc_inv_single_single {k : Type u} {G : Type u} [CommRing k] {n : ℕ} [Group G] (g : G) (f : Fin n → G) (a : k) (b : k) : ↑(GroupCohomology.Resolution.diagonalSucc k G n).inv.hom ((fun₀ | g => a) ⊗ₜ[k] fun₀ | f => b) = fun₀ | g • Fin.partialProd f => a * b

theorem GroupCohomology.Resolution.diagonalSucc_inv_single_left {k : Type u} {G : Type u} [CommRing k] {n : ℕ} [Group G] (g : G) (f : (Fin n → G) →₀ k) (r : k) : ↑(GroupCohomology.Resolution.diagonalSucc k G n).inv.hom ((fun₀ | g => r) ⊗ₜ[k] f) = ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => fun₀ | g • Fin.partialProd f => r) f

theorem GroupCohomology.Resolution.diagonalSucc_inv_single_right {k : Type u} {G : Type u} [CommRing k] {n : ℕ} [Group G] (g : G →₀ k) (f : Fin n → G) (r : k) : ↑(GroupCohomology.Resolution.diagonalSucc k G n).inv.hom (g ⊗ₜ[k] fun₀ | f => r) = ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => fun₀ | a • Fin.partialProd f => r) g

def GroupCohomology.Resolution.ofMulActionBasisAux (k : Type u) (G : Type u) [CommRing k] (n : ℕ) [Group G] : TensorProduct k (MonoidAlgebra k G) ((Fin n → G) →₀ k) ≃ₗ[MonoidAlgebra k G] Representation.asModule (Representation.ofMulAction k G (Fin (n + 1) → G))

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.

def GroupCohomology.Resolution.ofMulActionBasis (k : Type u) (G : Type u) [CommRing k] (n : ℕ) [Group G] : Basis (Fin n → G) (MonoidAlgebra k G) (Representation.asModule (Representation.ofMulAction k G (Fin (n + 1) → G)))

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

theorem GroupCohomology.Resolution.ofMulAction_free (k : Type u) (G : Type u) [CommRing k] (n : ℕ) [Group G] : Module.Free (MonoidAlgebra k G) (Representation.asModule (Representation.ofMulAction k G (Fin (n + 1) → G)))

noncomputable def Rep.diagonalHomEquiv {k : Type u} {G : Type u} [CommRing k] (n : ℕ) [Group G] (A : Rep k G) : (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) ≃ₗ[k] (Fin n → G) → CoeSort.coe A

Given a k-linear G-representation A, the set of representation morphisms Hom(k[Gⁿ⁺¹], A) is k-linearly isomorphic to the set of functions Gⁿ → A.

theorem Rep.diagonalHomEquiv_apply {k : Type u} {G : Type u} [CommRing k] {n : ℕ} [Group G] {A : Rep k G} (f : Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) (x : Fin n → G) : ↑(Rep.diagonalHomEquiv n A) f x = ↑f.hom fun₀ | Fin.partialProd x => 1

Given a k-linear G-representation A, diagonalHomEquiv is a k-linear isomorphism of the set of representation morphisms Hom(k[Gⁿ⁺¹], A) with Fun(Gⁿ, A). This lemma says that this sends a morphism of representations f : k[Gⁿ⁺¹] ⟶ A to the function (g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ).

theorem Rep.diagonalHomEquiv_symm_apply {k : Type u} {G : Type u} [CommRing k] {n : ℕ} [Group G] {A : Rep k G} (f : (Fin n → G) → CoeSort.coe A) (x : Fin (n + 1) → G) : (↑(↑(LinearEquiv.symm (Rep.diagonalHomEquiv n A)) f).hom fun₀ | x => 1) = ↑(↑(Rep.ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))

Given a k-linear G-representation A, diagonalHomEquiv is a k-linear isomorphism of the set of representation morphisms Hom(k[Gⁿ⁺¹], A) with Fun(Gⁿ, A). This lemma says that the inverse map sends a function f : Gⁿ → A to the representation morphism sending (g₀, ... gₙ) ↦ ρ(g₀)(f(g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)), where ρ is the representation attached to A.

theorem Rep.diagonalHomEquiv_symm_partialProd_succ {k : Type u} {G : Type u} [CommRing k] {n : ℕ} [Group G] {A : Rep k G} (f : (Fin n → G) → CoeSort.coe A) (g : Fin (n + 1) → G) (a : Fin (n + 1)) : (↑(↑(LinearEquiv.symm (Rep.diagonalHomEquiv n A)) f).hom fun₀ | Fin.partialProd g ∘ Fin.succAbove (Fin.succ a) => 1) = f (Fin.contractNth a (fun x x_1 => x * x_1) g)

Auxiliary lemma for defining group cohomology, used to show that the isomorphism diagonalHomEquiv commutes with the differentials in two complexes which compute group cohomology.

def classifyingSpaceUniversalCover (G : Type u) [Monoid G] : CategoryTheory.SimplicialObject (Action (Type u) (MonCat.of G))

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

def classifyingSpaceUniversalCover.cechNerveTerminalFromIso (G : Type u) [Monoid G] : CategoryTheory.cechNerveTerminalFrom (Action.ofMulAction G G) ≅ classifyingSpaceUniversalCover G

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.

def classifyingSpaceUniversalCover.cechNerveTerminalFromIsoCompForget (G : Type u) [Monoid G] : CategoryTheory.cechNerveTerminalFrom G ≅ CategoryTheory.Functor.comp (classifyingSpaceUniversalCover G) (CategoryTheory.forget (Action (Type u) (MonCat.of G)))

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.

def classifyingSpaceUniversalCover.compForgetAugmented (G : Type u) [Monoid G] : CategoryTheory.SimplicialObject.Augmented (Type u)

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.

def classifyingSpaceUniversalCover.extraDegeneracyAugmentedCechNerve (G : Type u) [Monoid G] : SimplicialObject.Augmented.ExtraDegeneracy (CategoryTheory.Arrow.augmentedCechNerve (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from G)))

The augmented Čech nerve of the map from Fin 1 → G to the terminal object in Type u has an extra degeneracy.

def classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmented (G : Type u) [Monoid G] : SimplicialObject.Augmented.ExtraDegeneracy (classifyingSpaceUniversalCover.compForgetAugmented G)

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.

def classifyingSpaceUniversalCover.compForgetAugmented.toModule (k : Type u) (G : Type u) [CommRing k] [Monoid G] : CategoryTheory.SimplicialObject.Augmented (ModuleCat k)

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.

def classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmentedToModule (k : Type u) (G : Type u) [CommRing k] [Monoid G] : SimplicialObject.Augmented.ExtraDegeneracy (classifyingSpaceUniversalCover.compForgetAugmented.toModule k G)

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.

def GroupCohomology.resolution (k : Type u) (G : Type u) [CommRing k] [Monoid G] : ChainComplex (Rep k G) ℕ

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

def GroupCohomology.Resolution.d (k : Type u) [CommRing 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ₙ).

@[simp]

theorem GroupCohomology.Resolution.d_of {k : Type u} [CommRing k] {G : Type u} {n : ℕ} (c : Fin (n + 1) → G) : (↑(GroupCohomology.Resolution.d k G n) fun₀ | c => 1) = Finset.sum Finset.univ fun p => fun₀ | c ∘ Fin.succAbove p => (-1) ^ ↑p

def GroupCohomology.Resolution.xIso (k : Type u) (G : Type u) [CommRing k] [Monoid G] (n : ℕ) : HomologicalComplex.X (GroupCohomology.resolution k G) n ≅ Rep.ofMulAction k G (Fin (n + 1) → G)

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.

theorem GroupCohomology.Resolution.x_projective (k : Type u) [CommRing k] (G : Type u) [Group G] (n : ℕ) : CategoryTheory.Projective (HomologicalComplex.X (GroupCohomology.resolution k G) n)

theorem GroupCohomology.Resolution.d_eq (k : Type u) (G : Type u) [CommRing k] [Monoid G] (n : ℕ) : (HomologicalComplex.d (GroupCohomology.resolution k G) (n + 1) n).hom = GroupCohomology.Resolution.d k G (n + 1)

Simpler expression for the differential in the standard resolution of k as a G-representation. It sends (g₀, ..., gₙ₊₁) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ₊₁).

def GroupCohomology.Resolution.forget₂ToModuleCat (k : Type u) (G : Type u) [CommRing k] [Monoid G] : HomologicalComplex (ModuleCat k) (ComplexShape.down ℕ)

The standard resolution of k as a trivial representation as a complex of k-modules.

def GroupCohomology.Resolution.compForgetAugmentedIso (k : Type u) (G : Type u) [CommRing k] [Monoid G] : AlgebraicTopology.AlternatingFaceMapComplex.obj (CategoryTheory.SimplicialObject.Augmented.drop.obj (classifyingSpaceUniversalCover.compForgetAugmented.toModule k G)) ≅ GroupCohomology.Resolution.forget₂ToModuleCat k G

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.

def GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv (k : Type u) (G : Type u) [CommRing k] [Monoid G] : HomotopyEquiv (GroupCohomology.Resolution.forget₂ToModuleCat k G) ((ChainComplex.single₀ (ModuleCat k)).obj ((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).obj (Rep.trivial k G k)))

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.

def GroupCohomology.Resolution.ε (k : Type u) (G : Type u) [CommRing k] [Monoid G] : Rep.ofMulAction k G (Fin 1 → G) ⟶ Rep.trivial k G k

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

theorem GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv_f_0_eq (k : Type u) (G : Type u) [CommRing k] [Monoid G] : HomologicalComplex.Hom.f (GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv k G).hom 0 = (CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).map (GroupCohomology.Resolution.ε k G)

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.

theorem GroupCohomology.Resolution.d_comp_ε (k : Type u) (G : Type u) [CommRing k] [Monoid G] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d (GroupCohomology.resolution k G) 1 0) (GroupCohomology.Resolution.ε k G) = 0

def GroupCohomology.Resolution.εToSingle₀ (k : Type u) (G : Type u) [CommRing k] [Monoid G] : GroupCohomology.resolution k G ⟶ (ChainComplex.single₀ (Rep k G)).obj (Rep.trivial k G k)

The chain map from the standard resolution of k to k[0] given by ∑ nᵢgᵢ ↦ ∑ nᵢ in degree zero.

theorem GroupCohomology.Resolution.εToSingle₀_comp_eq (k : Type u) (G : Type u) [CommRing k] [Monoid G] : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.mapHomologicalComplex (CategoryTheory.forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (GroupCohomology.Resolution.εToSingle₀ k G)) ((ChainComplex.single₀MapHomologicalComplex (CategoryTheory.forget₂ (Rep k G) (ModuleCat k))).hom.app (Rep.trivial k G k)) = (GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv k G).hom

theorem GroupCohomology.Resolution.quasiIsoOfForget₂εToSingle₀ (k : Type u) (G : Type u) [CommRing k] [Monoid G] : QuasiIso ((CategoryTheory.Functor.mapHomologicalComplex (CategoryTheory.forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (GroupCohomology.Resolution.εToSingle₀ k G))

instance GroupCohomology.Resolution.instQuasiIsoNatRepToRingInstCategoryActionModuleCatModuleCategoryOfPreadditiveHasZeroMorphismsInstPreadditiveActionInstCategoryActionInstPreadditiveModuleCatModuleCategoryHasEqualizersInstAbelianActionInstCategoryActionAbelianHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisationsHasImageMapsOfHasStrongEpiImagesHasStrongEpiImages_of_hasPullbacks_of_hasEqualizersHasPullbacksHasCokernels_of_hasCoequalizersHasCoequalizersDownToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringResolutionObjToQuiverToCategoryStructChainComplexInstCategoryHomologicalComplexToPrefunctorSingle₀HasZeroObjectTrivialToAddCommGroupToModuleToSemiringToCommSemiringεToSingle₀ (k : Type u) (G : Type u) [CommRing k] [Monoid G] : QuasiIso (GroupCohomology.Resolution.εToSingle₀ k G)

def GroupCohomology.projectiveResolution (k : Type u) (G : Type u) [CommRing k] [Group G] : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)

The standard projective resolution of k as a trivial k-linear G-representation.

instance instEnoughProjectivesRepToRingToMonoidToDivInvMonoidInstCategoryActionModuleCatModuleCategoryOf (k : Type u) (G : Type u) [CommRing k] [Group G] : CategoryTheory.EnoughProjectives (Rep k G)

def GroupCohomology.extIso (k : Type u) (G : Type u) [CommRing k] [Group G] (V : Rep k G) (n : ℕ) : ((Ext k (Rep k G) n).obj (Opposite.op (Rep.trivial k G k))).obj V ≅ (HomologicalComplex.homology ((CategoryTheory.Functor.mapHomologicalComplex ((CategoryTheory.linearYoneda k (Rep k G)).obj V).rightOp (ComplexShape.down ℕ)).obj (GroupCohomology.resolution k G)) n).unop

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