mathlib3 documentation

representation_theory.group_cohomology.resolution

The structure of the `k[G]`-module `k[Gⁿ]` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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.

def group_cohomology.resolution.Action_diagonal_succ (G : Type u) [group G] (n : ℕ) :

Action.diagonal G (n + 1) ≅ Action.left_regular 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

group_cohomology.resolution.Action_diagonal_succ G (n + 1) = Action.diagonal_succ G (n + 1) ≪≫ (category_theory.iso.refl (Action.left_regular G) ⊗ group_cohomology.resolution.Action_diagonal_succ G n) ≪≫ Action.left_regular_tensor_iso G (Action.left_regular G ⊗ {V := fin n → G, ρ := 1}) ≪≫ (category_theory.iso.refl (Action.left_regular G) ⊗ Action.mk_iso (equiv.pi_fin_succ_above_equiv (λ (j : fin (n + 1)), G) 0).symm.to_iso _)
group_cohomology.resolution.Action_diagonal_succ G 0 = Action.diagonal_one_iso_left_regular G ≪≫ (ρ_ (Action.left_regular G)).symm ≪≫ (category_theory.iso.refl (Action.left_regular G) ⊗ Action.tensor_unit_iso (equiv.equiv_of_unique punit (fin 0 → G)).to_iso)

theorem group_cohomology.resolution.Action_diagonal_succ_hom_apply {G : Type u} [group G] {n : ℕ} (f : fin (n + 1) → G) :

(group_cohomology.resolution.Action_diagonal_succ G n).hom.hom f = (f 0, λ (i : fin n), (f (⇑fin.cast_succ i))⁻¹ * f i.succ)

theorem group_cohomology.resolution.Action_diagonal_succ_inv_apply {G : Type u} [group G] {n : ℕ} (g : G) (f : fin n → G) :

(group_cohomology.resolution.Action_diagonal_succ G n).inv.hom (g, f) = g • fin.partial_prod f

noncomputable def group_cohomology.resolution.diagonal_succ (k G : Type u) [comm_ring k] [group G] (n : ℕ) :

Rep.diagonal k G (n + 1) ≅ Rep.left_regular 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ₙ).

Equations

group_cohomology.resolution.diagonal_succ k G n = (Rep.linearization k G).to_lax_monoidal_functor.to_functor.map_iso (group_cohomology.resolution.Action_diagonal_succ G n) ≪≫ (category_theory.as_iso ((Rep.linearization k G).to_lax_monoidal_functor.μ (Action.left_regular G) {V := fin n → G, ρ := 1})).symm ≪≫ (category_theory.iso.refl ((Rep.linearization k G).to_lax_monoidal_functor.to_functor.obj (Action.left_regular G)) ⊗ Rep.linearization_trivial_iso k G (fin n → G))

theorem group_cohomology.resolution.diagonal_succ_hom_single {k G : Type u} [comm_ring k] {n : ℕ} [group G] (f : fin (n + 1) → G) (a : k) :

⇑((group_cohomology.resolution.diagonal_succ k G n).hom.hom) (finsupp.single f a) = finsupp.single (f 0) 1 ⊗ₜ[k] finsupp.single (λ (i : fin n), (f (⇑fin.cast_succ i))⁻¹ * f i.succ) a

theorem group_cohomology.resolution.diagonal_succ_inv_single_single {k G : Type u} [comm_ring k] {n : ℕ} [group G] (g : G) (f : fin n → G) (a b : k) :

⇑((group_cohomology.resolution.diagonal_succ k G n).inv.hom) (finsupp.single g a ⊗ₜ[k] finsupp.single f b) = finsupp.single (g • fin.partial_prod f) (a * b)

theorem group_cohomology.resolution.diagonal_succ_inv_single_left {k G : Type u} [comm_ring k] {n : ℕ} [group G] (g : G) (f : (fin n → G) →₀ k) (r : k) :

⇑((group_cohomology.resolution.diagonal_succ k G n).inv.hom) (finsupp.single g r ⊗ₜ[k] f) = ⇑(⇑(finsupp.lift ((fin (n + 1) → G) →₀ k) k (fin n → G)) (λ (f : fin n → G), finsupp.single (g • fin.partial_prod f) r)) f

theorem group_cohomology.resolution.diagonal_succ_inv_single_right {k G : Type u} [comm_ring k] {n : ℕ} [group G] (g : G →₀ k) (f : fin n → G) (r : k) :

⇑((group_cohomology.resolution.diagonal_succ k G n).inv.hom) (g ⊗ₜ[k] finsupp.single f r) = ⇑(⇑(finsupp.lift ((fin (n + 1) → G) →₀ k) k G) (λ (a : G), finsupp.single (a • fin.partial_prod f) r)) g

noncomputable def group_cohomology.resolution.of_mul_action_basis_aux (k G : Type u) [comm_ring k] (n : ℕ) [group G] :

tensor_product k (monoid_algebra k G) ((fin n → G) →₀ k) ≃ₗ[monoid_algebra k G] (representation.of_mul_action k G (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) (monoid_algebra k G) (representation.of_mul_action k 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

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)

theorem group_cohomology.resolution.of_mul_action_free (k G : Type u) [comm_ring k] (n : ℕ) [group G] :

module.free (monoid_algebra k G) (representation.of_mul_action k G (fin (n + 1) → G)).as_module

noncomputable def Rep.diagonal_hom_equiv {k G : Type u} [comm_ring k] (n : ℕ) [group G] (A : Rep k G) :

(Rep.of_mul_action k G (fin (n + 1) → G) ⟶ A) ≃ₗ[k] (fin n → G) → ↥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.

Equations

Rep.diagonal_hom_equiv n A = ((category_theory.linear.hom_congr k (group_cohomology.resolution.diagonal_succ k G n ≪≫ (representation.of_mul_action k G G).Rep_of_tprod_iso 1) (category_theory.iso.refl A)).trans ((Rep.monoidal_closed.linear_hom_equiv_comm (Rep.of_mul_action k G G) (Rep.of (Rep.trivial k G ((fin n → G) →₀ k)).ρ) A).trans ((category_theory.ihom (Rep.of (Rep.trivial k G ((fin n → G) →₀ k)).ρ)).obj A).left_regular_hom_equiv)).trans (finsupp.llift ↥A k k (fin n → G)).symm

theorem Rep.diagonal_hom_equiv_apply {k G : Type u} [comm_ring k] {n : ℕ} [group G] {A : Rep k G} (f : Rep.of_mul_action k G (fin (n + 1) → G) ⟶ A) (x : fin n → G) :

⇑(Rep.diagonal_hom_equiv n A) f x = ⇑(f.hom) (finsupp.single (fin.partial_prod x) 1)

Given a k-linear G-representation A, diagonal_hom_equiv 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.diagonal_hom_equiv_symm_apply {k G : Type u} [comm_ring k] {n : ℕ} [group G] {A : Rep k G} (f : (fin n → G) → ↥A) (x : fin (n + 1) → G) :

⇑((⇑((Rep.diagonal_hom_equiv n A).symm) f).hom) (finsupp.single x 1) = ⇑(⇑(A.ρ) (x 0)) (f (λ (i : fin n), (x (⇑fin.cast_succ i))⁻¹ * x i.succ))

Given a k-linear G-representation A, diagonal_hom_equiv 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.diagonal_hom_equiv_symm_partial_prod_succ {k G : Type u} [comm_ring k] {n : ℕ} [group G] {A : Rep k G} (f : (fin n → G) → ↥A) (g : fin (n + 1) → G) (a : fin (n + 1)) :

⇑((⇑((Rep.diagonal_hom_equiv n A).symm) f).hom) (finsupp.single (fin.partial_prod g ∘ ⇑(a.succ.succ_above)) 1) = f (a.contract_nth has_mul.mul g)

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

def classifying_space_universal_cover (G : Type u) [monoid G] :

category_theory.simplicial_object (Action (Type u) (Mon.of G))

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' := _}

noncomputable def classifying_space_universal_cover.cech_nerve_terminal_from_iso (G : Type u) [monoid G] :

category_theory.cech_nerve_terminal_from (Action.of_mul_action G G) ≅ classifying_space_universal_cover G

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

classifying_space_universal_cover.cech_nerve_terminal_from_iso G = category_theory.nat_iso.of_components (λ (n : simplex_category ᵒᵖ), category_theory.limits.limit.iso_limit_cone (Action.of_mul_action_limit_cone G (λ (i : fin ((opposite.unop n).len + 1)), G))) _

noncomputable def classifying_space_universal_cover.cech_nerve_terminal_from_iso_comp_forget (G : Type u) [monoid G] :

category_theory.cech_nerve_terminal_from G ≅ classifying_space_universal_cover G ⋙ category_theory.forget (Action (Type u) (Mon.of G))

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

classifying_space_universal_cover.cech_nerve_terminal_from_iso_comp_forget G = category_theory.nat_iso.of_components (λ (n : simplex_category ᵒᵖ), category_theory.limits.types.product_iso (λ (i : fin ((opposite.unop n).len + 1)), G)) _

noncomputable def classifying_space_universal_cover.comp_forget_augmented (G : Type u) [monoid G] :

category_theory.simplicial_object.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.

Equations

noncomputable def classifying_space_universal_cover.extra_degeneracy_augmented_cech_nerve (G : Type u) [monoid G] :

simplicial_object.augmented.extra_degeneracy (category_theory.arrow.mk (category_theory.limits.terminal.from G)).augmented_cech_nerve

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' := _}

noncomputable def classifying_space_universal_cover.extra_degeneracy_comp_forget_augmented (G : Type u) [monoid G] :

simplicial_object.augmented.extra_degeneracy (classifying_space_universal_cover.comp_forget_augmented 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.

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)

noncomputable def classifying_space_universal_cover.comp_forget_augmented.to_Module (k G : Type u) [comm_ring k] [monoid G] :

category_theory.simplicial_object.augmented (Module k)

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.

Equations

classifying_space_universal_cover.comp_forget_augmented.to_Module k G = ((category_theory.simplicial_object.augmented.whiskering (Type u) (Module k)).obj (Module.free k)).obj (classifying_space_universal_cover.comp_forget_augmented G)

noncomputable def classifying_space_universal_cover.extra_degeneracy_comp_forget_augmented_to_Module (k G : Type u) [comm_ring k] [monoid G] :

simplicial_object.augmented.extra_degeneracy (classifying_space_universal_cover.comp_forget_augmented.to_Module 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 ⥤ Module.{u} k, the resulting augmented simplicial k-module has an extra degeneracy.

Equations

classifying_space_universal_cover.extra_degeneracy_comp_forget_augmented_to_Module k G = (classifying_space_universal_cover.extra_degeneracy_comp_forget_augmented G).map (Module.free k)

noncomputable def group_cohomology.resolution (k G : Type u) [comm_ring k] [monoid G] :

chain_complex (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.

Equations

group_cohomology.resolution k G = (algebraic_topology.alternating_face_map_complex (Rep k G)).obj (classifying_space_universal_cover G ⋙ (Rep.linearization k G).to_lax_monoidal_functor.to_functor)

noncomputable def group_cohomology.resolution.d (k : Type u) [comm_ring 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ₙ).

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

@[simp]

theorem group_cohomology.resolution.d_of {k : Type u} [comm_ring k] {G : Type u} {n : ℕ} (c : fin (n + 1) → G) :

⇑(group_cohomology.resolution.d k G n) (finsupp.single c 1) = finset.univ.sum (λ (p : fin (n + 1)), finsupp.single (c ∘ ⇑(p.succ_above)) ((-1) ^ ↑p))

noncomputable def group_cohomology.resolution.X_iso (k G : Type u) [comm_ring k] [monoid G] (n : ℕ) :

(group_cohomology.resolution k G).X n ≅ Rep.of_mul_action 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.

Equations

group_cohomology.resolution.X_iso k G n = category_theory.iso.refl ((group_cohomology.resolution k G).X n)

theorem group_cohomology.resolution.X_projective (k : Type u) [comm_ring k] (G : Type u) [group G] (n : ℕ) :

category_theory.projective ((group_cohomology.resolution k G).X n)

theorem group_cohomology.resolution.d_eq (k G : Type u) [comm_ring k] [monoid G] (n : ℕ) :

((group_cohomology.resolution k G).d (n + 1) n).hom = group_cohomology.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ₙ₊₁).

noncomputable def group_cohomology.resolution.forget₂_to_Module (k G : Type u) [comm_ring k] [monoid G] :

homological_complex (Module k) (complex_shape.down ℕ)

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

Equations

group_cohomology.resolution.forget₂_to_Module k G = ((category_theory.forget₂ (Rep k G) (Module k)).map_homological_complex (complex_shape.down ℕ)).obj (group_cohomology.resolution k G)

noncomputable def group_cohomology.resolution.comp_forget_augmented_iso (k G : Type u) [comm_ring k] [monoid G] :

algebraic_topology.alternating_face_map_complex.obj (category_theory.simplicial_object.augmented.drop.obj (classifying_space_universal_cover.comp_forget_augmented.to_Module k G)) ≅ group_cohomology.resolution.forget₂_to_Module k G

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.

Equations

group_cohomology.resolution.comp_forget_augmented_iso k G = category_theory.eq_to_iso _

noncomputable def group_cohomology.resolution.forget₂_to_Module_homotopy_equiv (k G : Type u) [comm_ring k] [monoid G] :

homotopy_equiv (group_cohomology.resolution.forget₂_to_Module k G) ((chain_complex.single₀ (Module k)).obj ((category_theory.forget₂ (Rep k G) (Module 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.

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

noncomputable def group_cohomology.resolution.ε (k G : Type u) [comm_ring k] [monoid G] :

Rep.of_mul_action k G (fin 1 → G) ⟶ Rep.trivial k G k

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.trivial k G k).V) k (λ (f : fin 1 → G), 1), comm' := _}

theorem group_cohomology.resolution.forget₂_to_Module_homotopy_equiv_f_0_eq (k G : Type u) [comm_ring k] [monoid G] :

(group_cohomology.resolution.forget₂_to_Module_homotopy_equiv k G).hom.f 0 = (category_theory.forget₂ (Rep k G) (Module k)).map (group_cohomology.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 group_cohomology.resolution.d_comp_ε (k G : Type u) [comm_ring k] [monoid G] :

(group_cohomology.resolution k G).d 1 0 ≫ group_cohomology.resolution.ε k G = 0

noncomputable def group_cohomology.resolution.ε_to_single₀ (k G : Type u) [comm_ring k] [monoid G] :

group_cohomology.resolution k G ⟶ (chain_complex.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.

Equations

group_cohomology.resolution.ε_to_single₀ k G = ⇑(((group_cohomology.resolution k G).to_single₀_equiv (Rep.trivial k G k)).symm) ⟨group_cohomology.resolution.ε k G _inst_2, _⟩

Instances for group_cohomology.resolution.ε_to_single₀

group_cohomology.resolution.ε_to_single₀.quasi_iso

theorem group_cohomology.resolution.ε_to_single₀_comp_eq (k G : Type u) [comm_ring k] [monoid G] :

((category_theory.forget₂ (Rep k G) (Module k)).map_homological_complex (complex_shape.down ℕ)).map (group_cohomology.resolution.ε_to_single₀ k G) ≫ (chain_complex.single₀_map_homological_complex (category_theory.forget₂ (Rep k G) (Module k))).hom.app (Rep.trivial k G k) = (group_cohomology.resolution.forget₂_to_Module_homotopy_equiv k G).hom

theorem group_cohomology.resolution.quasi_iso_of_forget₂_ε_to_single₀ (k G : Type u) [comm_ring k] [monoid G] :

quasi_iso (((category_theory.forget₂ (Rep k G) (Module k)).map_homological_complex (complex_shape.down ℕ)).map (group_cohomology.resolution.ε_to_single₀ k G))

@[protected, instance]

def group_cohomology.resolution.ε_to_single₀.quasi_iso (k G : Type u) [comm_ring k] [monoid G] :

quasi_iso (group_cohomology.resolution.ε_to_single₀ k G)

noncomputable def group_cohomology.ProjectiveResolution (k G : Type u) [comm_ring k] [group G] :

category_theory.ProjectiveResolution (Rep.trivial k G k)

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

Equations

group_cohomology.ProjectiveResolution k G = homological_complex.hom.to_single₀_ProjectiveResolution (group_cohomology.resolution.ε_to_single₀ k G) _

@[protected, instance]

def Rep.category_theory.enough_projectives (k G : Type u) [comm_ring k] [group G] :

category_theory.enough_projectives (Rep k G)

noncomputable def group_cohomology.Ext_iso (k G : Type u) [comm_ring k] [group G] (V : Rep k G) (n : ℕ) :

((Ext k (Rep k G) n).obj (opposite.op (Rep.trivial k G k))).obj V ≅ opposite.unop (((((category_theory.linear_yoneda k (Rep k G)).obj V).right_op.map_homological_complex (complex_shape.down ℕ)).obj (group_cohomology.resolution k G)).homology 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 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.trivial k G k)) ≅ 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