The standard and bar resolutions of k as a trivial k-linear G-representation

Given a commutative ring k and a group G, this file defines two projective resolutions of k as a trivial k-linear G-representation.

The first one, the standard resolution, has objects k[Gⁿ⁺¹] equipped with the diagonal representation, and differential defined by (g₀, ..., gₙ) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ).

We define this as 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 Rep.standardResolution, the standard projective resolution of k as a trivial k-linear G-representation.

We then construct the bar resolution. The nth object in this complex is the representation on Gⁿ →₀ k[G] defined pointwise by the left regular representation on k[G]. The differentials are defined by sending (g₀, ..., gₙ) to g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁) for j = 0, ... , n - 1.

In RepresentationTheory.Rep we define an isomorphism Rep.diagonalSuccIsoFree between k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G]) sending (g₀, ..., gₙ) ↦ g₀·(g₀⁻¹g₁, ..., gₙ₋₁⁻¹gₙ). We show that this isomorphism defines a commutative square with the bar resolution differential and the standard resolution differential, and thus conclude that the bar resolution differential squares to zero and that Rep.diagonalSuccIsoFree defines an isomorphism between the two complexes. We carry the exactness properties across this isomorphism to conclude the bar resolution is a projective resolution too, in Rep.barResolution.

In RepresentationTheory/Homological/Group(Co)homology/Basic.lean, we then use Rep.barResolution to define the inhomogeneous (co)chains of a representation, useful for computing group (co)homology.

Main definitions

• groupCohomology.resolution.ofMulActionBasis
• classifyingSpaceUniversalCover
• Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv
• Rep.standardResolution

@[deprecated Action.diagonalSuccIsoTensorTrivial (since := "2025-06-02")]

def groupCohomology.resolution.groupCohomology.resolution.actionDiagonalSucc (G : Type u) [Group G] (n : ℕ) : Action.diagonal G (n + 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) (Action.trivial G (Fin n → G))

Alias of Action.diagonalSuccIsoTensorTrivial.

---

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

@[deprecated Action.diagonalSuccIsoTensorTrivial_hom_hom_apply (since := "2025-06-02")]

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

Alias of Action.diagonalSuccIsoTensorTrivial_hom_hom_apply.

@[deprecated Action.diagonalSuccIsoTensorTrivial_inv_hom_apply (since := "2025-06-02")]

theorem groupCohomology.resolution.groupCohomology.resolution.actionDiagonalSucc_inv_apply {G : Type u} [Group G] {n : ℕ} (g : G) (f : Fin n → G) : (Action.diagonalSuccIsoTensorTrivial G n).inv.hom (g, f) = g • Fin.partialProd f

Alias of Action.diagonalSuccIsoTensorTrivial_inv_hom_apply.

@[deprecated Rep.diagonalSuccIsoTensorTrivial (since := "2025-06-02")]

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

Alias of Rep.diagonalSuccIsoTensorTrivial.

---

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

@[deprecated Rep.diagonalSuccIsoTensorTrivial_hom_hom_single (since := "2025-06-02")]

theorem groupCohomology.resolution.groupCohomology.resolution.diagonalSucc_hom_single {k G : Type u} [CommRing k] [Group G] {n : ℕ} (f : Fin (n + 1) → G) (a : k) : (ModuleCat.Hom.hom (Rep.diagonalSuccIsoTensorTrivial k G n).hom.hom) (Finsupp.single f a) = Finsupp.single (f 0) 1 ⊗ₜ[k] Finsupp.single (fun (i : Fin n) => (f i.castSucc)⁻¹ * f i.succ) a

Alias of Rep.diagonalSuccIsoTensorTrivial_hom_hom_single.

@[deprecated Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single (since := "2025-06-02")]

theorem groupCohomology.resolution.groupCohomology.resolution.diagonalSucc_inv_single_single {k G : Type u} [CommRing k] [Group G] {n : ℕ} (g : G) (f : Fin n → G) (a b : k) : (CategoryTheory.ConcreteCategory.hom (Rep.diagonalSuccIsoTensorTrivial k G n).inv.hom) (Finsupp.single g a ⊗ₜ[k] Finsupp.single f b) = Finsupp.single (g • Fin.partialProd f) (a * b)

Alias of Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single.

@[deprecated Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left (since := "2025-06-02")]

theorem groupCohomology.resolution.groupCohomology.resolution.diagonalSucc_inv_single_left {k G : Type u} [CommRing k] [Group G] {n : ℕ} (g : G) (f : (Fin n → G) →₀ k) (r : k) : (CategoryTheory.ConcreteCategory.hom (Rep.diagonalSuccIsoTensorTrivial k G n).inv.hom) (Finsupp.single g r ⊗ₜ[k] f) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun (f : Fin n → G) => Finsupp.single (g • Fin.partialProd f) r) f

Alias of Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left.

@[deprecated Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right (since := "2025-06-02")]

theorem groupCohomology.resolution.groupCohomology.resolution.diagonalSucc_inv_single_right {k G : Type u} [CommRing k] [Group G] {n : ℕ} (g : G →₀ k) (f : Fin n → G) (r : k) : (CategoryTheory.ConcreteCategory.hom (Rep.diagonalSuccIsoTensorTrivial k G n).inv.hom) (g ⊗ₜ[k] Finsupp.single f r) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun (a : G) => Finsupp.single (a • Fin.partialProd f) r) g

Alias of Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right.

@[deprecated "We now favour `Representation.finsuppLEquivFreeAsModule`" (since := "2025-06-04")]

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

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.

@[deprecated Representation.freeAsModuleBasis "We now favour `Representation.freeAsModuleBasis`; the old definition can be derived from this and `Rep.diagonalSuccIsoFree" (since := "2025-06-05")]

def groupCohomology.resolution.ofMulActionBasis (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : Type u_6) : Module.Basis α (MonoidAlgebra k G) (Representation.free k G α).asModule

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

@[deprecated Representation.free_asModule_free "We now favour `Representation.free_asModule_free`; the old theorem can be derived from this and `Rep.diagonalSuccIsoFree" (since := "2025-06-05")]

theorem groupCohomology.resolution.ofMulAction_free (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : Type u_6) : Module.Free (MonoidAlgebra k G) (Representation.free k G α).asModule

Alias of Representation.free_asModule_free.

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

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

@[simp]

theorem classifyingSpaceUniversalCover_obj (G : Type u) [Monoid G] (n : SimplexCategoryᵒᵖ) : (classifyingSpaceUniversalCover G).obj n = Action.ofMulAction G (Fin ((Opposite.unop n).len + 1) → G)

@[simp]

theorem classifyingSpaceUniversalCover_map (G : Type u) [Monoid G] {X✝ Y✝ : SimplexCategoryᵒᵖ} (f : X✝ ⟶ Y✝) : (classifyingSpaceUniversalCover G).map f = { hom := fun (x : (Action.ofMulAction G (Fin ((Opposite.unop X✝).len + 1) → G)).V) => x ∘ ⇑(SimplexCategory.Hom.toOrderHom f.unop), comm := ⋯ }

noncomputable 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.

noncomputable def classifyingSpaceUniversalCover.cechNerveTerminalFromIsoCompForget (G : Type u) [Monoid G] : CategoryTheory.cechNerveTerminalFrom G ≅ CategoryTheory.Functor.comp (classifyingSpaceUniversalCover G) (CategoryTheory.forget (Action (Type u) 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.

noncomputable 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.

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

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

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

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.

noncomputable def classifyingSpaceUniversalCover.compForgetAugmented.toModule (k 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.

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

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.

noncomputable def Rep.standardComplex (k 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.

@[deprecated Rep.standardComplex (since := "2025-06-06")]

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

Alias of Rep.standardComplex.

---

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

noncomputable def Rep.standardComplex.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 Rep.standardComplex.d_of {k : Type u} [CommRing k] {G : Type u} {n : ℕ} (c : Fin (n + 1) → G) : (d k G n) (Finsupp.single c 1) = ∑ p : Fin (n + 1), Finsupp.single (c ∘ p.succAbove) ((-1) ^ ↑p)

noncomputable def Rep.standardComplex.xIso (k G : Type u) [CommRing k] [Monoid G] (n : ℕ) : (standardComplex k G).X n ≅ 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.

instance Rep.standardComplex.x_projective (k : Type u) [CommRing k] (G : Type u) [Group G] [DecidableEq G] (n : ℕ) : CategoryTheory.Projective ((standardComplex k G).X n)

theorem Rep.standardComplex.d_eq (k G : Type u) [CommRing k] [Monoid G] (n : ℕ) : ((standardComplex k G).d (n + 1) n).hom = ModuleCat.ofHom (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ₙ₊₁).

noncomputable def Rep.standardComplex.forget₂ToModuleCat (k 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.

noncomputable def Rep.standardComplex.compForgetAugmentedIso (k G : Type u) [CommRing k] [Monoid G] : AlgebraicTopology.AlternatingFaceMapComplex.obj (CategoryTheory.SimplicialObject.Augmented.drop.obj (classifyingSpaceUniversalCover.compForgetAugmented.toModule k G)) ≅ 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.

noncomputable def Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv (k G : Type u) [CommRing k] [Monoid G] : HomotopyEquiv (forget₂ToModuleCat k G) ((ChainComplex.single₀ (ModuleCat k)).obj ((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).obj (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.

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

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

theorem Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq (k G : Type u) [CommRing k] [Monoid G] : (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 = (CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).map (ε 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 Rep.standardComplex.d_comp_ε (k G : Type u) [CommRing k] [Monoid G] : CategoryTheory.CategoryStruct.comp ((standardComplex k G).d 1 0) (ε k G) = 0

noncomputable def Rep.standardComplex.εToSingle₀ (k G : Type u) [CommRing k] [Monoid G] : standardComplex k G ⟶ (ChainComplex.single₀ (Rep k G)).obj (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 Rep.standardComplex.εToSingle₀_comp_eq (k G : Type u) [CommRing k] [Monoid G] : CategoryTheory.CategoryStruct.comp (((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G)) ((HomologicalComplex.singleMapHomologicalComplex (CategoryTheory.forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app (trivial k G k)) = (forget₂ToModuleCatHomotopyEquiv k G).hom

theorem Rep.standardComplex.quasiIso_forget₂_εToSingle₀ (k G : Type u) [CommRing k] [Monoid G] : QuasiIso (((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))

instance Rep.standardComplex.instQuasiIsoNatεToSingle₀ (k G : Type u) [CommRing k] [Monoid G] : QuasiIso (εToSingle₀ k G)

noncomputable def Rep.standardResolution (k G : Type u) [CommRing k] [Group G] [DecidableEq G] : CategoryTheory.ProjectiveResolution (trivial k G k)

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

@[deprecated Rep.standardResolution (since := "2025-06-06")]

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

Alias of Rep.standardResolution.

---

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

noncomputable def Rep.standardResolution.extIso (k G : Type u) [CommRing k] [Group G] [DecidableEq G] (V : Rep k G) (n : ℕ) : ((Ext k (Rep k G) n).obj (Opposite.op (trivial k G k))).obj V ≅ HomologicalComplex.homology ((standardComplex k G).linearYonedaObj k V) n

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 standardComplex k G.

@[deprecated Rep.standardResolution.extIso (since := "2025-06-06")]

def Rep.groupCohomology.extIso (k G : Type u) [CommRing k] [Group G] [DecidableEq G] (V : Rep k G) (n : ℕ) : ((Ext k (Rep k G) n).obj (Opposite.op (trivial k G k))).obj V ≅ HomologicalComplex.homology ((standardComplex k G).linearYonedaObj k V) n

Alias of Rep.standardResolution.extIso.

---

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 standardComplex k G.

noncomputable def Rep.barComplex.d (k G : Type u) [CommRing k] (n : ℕ) [Group G] [DecidableEq G] : free k G (Fin (n + 1) → G) ⟶ free k G (Fin n → G)

The differential from Gⁿ⁺¹ →₀ k[G] to Gⁿ →₀ k[G] in the bar resolution of k as a trivial k-linear G-representation. It sends (g₀, ..., gₙ) to g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁) for j = 0, ... , n - 1.

theorem Rep.barComplex.d_single {k G : Type u} [CommRing k] (n : ℕ) [Group G] [DecidableEq G] (x : Fin (n + 1) → G) : (CategoryTheory.ConcreteCategory.hom (d k G n).hom) (Finsupp.single x (Finsupp.single 1 1)) = Finsupp.single (fun (i : Fin n) => x i.succ) (Finsupp.single (x 0) 1) + ∑ j : Fin (n + 1), Finsupp.single (j.contractNth (fun (x1 x2 : G) => x1 * x2) x) (Finsupp.single 1 ((-1) ^ (↑j + 1)))

theorem Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq (k G : Type u) [CommRing k] (n : ℕ) [Group G] [DecidableEq G] : CategoryTheory.CategoryStruct.comp (d k G n) (diagonalSuccIsoFree k G n).inv = CategoryTheory.CategoryStruct.comp (diagonalSuccIsoFree k G (n + 1)).inv ((standardComplex k G).d (n + 1) n)

@[reducible, inline]

noncomputable abbrev Rep.barComplex (k G : Type u) [CommRing k] [Group G] [DecidableEq G] : ChainComplex (Rep k G) ℕ

The projective resolution of k as a trivial k-linear G-representation with nth differential (Gⁿ⁺¹ →₀ k[G]) → (Gⁿ →₀ k[G]) sending (g₀, ..., gₙ) to g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁) for j = 0, ... , n - 1.

@[simp]

theorem Rep.barComplex.d_def (k G : Type u) [CommRing k] {n : ℕ} [Group G] [DecidableEq G] : (barComplex k G).d (n + 1) n = d k G n

noncomputable def Rep.barComplex.isoStandardComplex (k G : Type u) [CommRing k] [Group G] [DecidableEq G] : barComplex k G ≅ standardComplex k G

Isomorphism between the bar resolution and standard resolution, with nth map (Gⁿ →₀ k[G]) → k[Gⁿ⁺¹] sending (g₁, ..., gₙ) ↦ (1, g₁, g₁g₂, ..., g₁...gₙ).

noncomputable def Rep.barResolution (k G : Type u) [CommRing k] [Group G] [DecidableEq G] : CategoryTheory.ProjectiveResolution (trivial k G k)

The chain complex barComplex k G as a projective resolution of k as a trivial k-linear G-representation.

@[simp]

theorem Rep.barResolution_complex (k G : Type u) [CommRing k] [Group G] [DecidableEq G] : (barResolution k G).complex = barComplex k G

noncomputable def Rep.barResolution.extIso (k G : Type u) [CommRing k] [Group G] [DecidableEq G] (V : Rep k G) (n : ℕ) : ((Ext k (Rep k G) n).obj (Opposite.op (trivial k G k))).obj V ≅ HomologicalComplex.homology ((barComplex k G).linearYonedaObj k V) n

Given a k-linear G-representation V, Extⁿ(k, V) (where k is the trivial k-linear G-representation) is isomorphic to the nth cohomology group of Hom(P, V), where P is the bar resolution of k.