feat(representation_theory/group_cohomology/basic): add standard defi…

…nition of group cohomology (#18341)

We define the complex of inhomogeneous cochains, define group cohomology to be its cohomology, and prove this is isomorphic to the appropriate Ext groups.



Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Amelia Livingston <al3717@ic.ac.uk>

src/algebra/big_operators/fin.lean

@@ -208,6 +208,40 @@ begin
     assoc_rw [hi, inv_mul_cancel_left] }
 end
 
+/-- Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
+Then if `k < j`, this says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ`.
+If `k = j`, it says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ₊₁ = gₖgₖ₊₁`.
+If `k > j`, it says `(g₀g₁...gₖ)⁻¹ * g₀g₁...gₖ₊₁ = gₖ₊₁.`
+Useful for defining group cohomology. -/
+@[to_additive "Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
+Then if `k < j`, this says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ) = gₖ`.
+If `k = j`, it says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ + gₖ₊₁`.
+If `k > j`, it says `-(g₀ + g₁ + ... + gₖ) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ₊₁.`
+Useful for defining group cohomology."]
+lemma inv_partial_prod_mul_eq_contract_nth {G : Type*} [group G]
+  (g : fin (n + 1) → G) (j : fin (n + 1)) (k : fin n) :
+  (partial_prod g (j.succ.succ_above k.cast_succ))⁻¹ * partial_prod g (j.succ_above k).succ
+    = j.contract_nth has_mul.mul g k :=
+begin
+  have := partial_prod_right_inv (1 : G) g,
+  simp only [one_smul, coe_eq_cast_succ] at this,
+  rcases lt_trichotomy (k : ℕ) j with (h|h|h),
+  { rwa [succ_above_below, succ_above_below, this, contract_nth_apply_of_lt],
+    { assumption },
+    { rw [cast_succ_lt_iff_succ_le, succ_le_succ_iff, le_iff_coe_le_coe],
+      exact le_of_lt h }},
+  { rwa [succ_above_below, succ_above_above, partial_prod_succ, cast_succ_fin_succ, ←mul_assoc,
+      this, contract_nth_apply_of_eq],
+    { simpa only [le_iff_coe_le_coe, ←h] },
+    { rw [cast_succ_lt_iff_succ_le, succ_le_succ_iff, le_iff_coe_le_coe],
+      exact le_of_eq h }},
+  { rwa [succ_above_above, succ_above_above, partial_prod_succ, partial_prod_succ,
+      cast_succ_fin_succ, partial_prod_succ, inv_mul_cancel_left, contract_nth_apply_of_gt],
+    { exact le_iff_coe_le_coe.2 (le_of_lt h) },
+    { rw [le_iff_coe_le_coe, coe_succ],
+      exact nat.succ_le_of_lt h }},
+end
+
 end partial_prod
 
 end fin

src/data/fin/tuple/basic.lean

@@ -847,6 +847,46 @@ lemma mem_find_of_unique {p : fin n → Prop} [decidable_pred p]
 mem_find_iff.2 ⟨hi, λ j hj, le_of_eq $ h i j hi hj⟩
 
 end find
+section contract_nth
+
+variables {α : Type*}
+
+/-- Sends `(g₀, ..., gₙ)` to `(g₀, ..., op gⱼ gⱼ₊₁, ..., gₙ)`. -/
+def contract_nth (j : fin (n + 1)) (op : α → α → α) (g : fin (n + 1) → α) (k : fin n) : α :=
+if (k : ℕ) < j then g k.cast_succ else
+if (k : ℕ) = j then op (g k.cast_succ) (g k.succ)
+else g k.succ
+
+lemma contract_nth_apply_of_lt (j : fin (n + 1)) (op : α → α → α) (g : fin (n + 1) → α)
+  (k : fin n) (h : (k : ℕ) < j) :
+  contract_nth j op g k = g k.cast_succ := if_pos h
+
+lemma contract_nth_apply_of_eq (j : fin (n + 1)) (op : α → α → α) (g : fin (n + 1) → α)
+  (k : fin n) (h : (k : ℕ) = j) :
+  contract_nth j op g k = op (g k.cast_succ) (g k.succ) :=
+begin
+  have : ¬(k : ℕ) < j, from not_lt.2 (le_of_eq h.symm),
+  rw [contract_nth, if_neg this, if_pos h],
+end
+
+lemma contract_nth_apply_of_gt (j : fin (n + 1)) (op : α → α → α) (g : fin (n + 1) → α)
+  (k : fin n) (h : (j : ℕ) < k) :
+  contract_nth j op g k = g k.succ :=
+by rw [contract_nth, if_neg (not_lt_of_gt h), if_neg (ne.symm $ ne_of_lt h)]
+
+lemma contract_nth_apply_of_ne (j : fin (n + 1)) (op : α → α → α) (g : fin (n + 1) → α)
+  (k : fin n) (hjk : (j : ℕ) ≠ k) :
+  contract_nth j op g k = g (j.succ_above k) :=
+begin
+  rcases lt_trichotomy (k : ℕ) j with (h|h|h),
+  { rwa [j.succ_above_below, contract_nth_apply_of_lt],
+    { rwa [ fin.lt_iff_coe_lt_coe] }},
+  { exact false.elim (hjk h.symm) },
+  { rwa [j.succ_above_above, contract_nth_apply_of_gt],
+    { exact fin.le_iff_coe_le_coe.2 (le_of_lt h) }}
+end
+
+end contract_nth
 
 /-- To show two sigma pairs of tuples agree, it to show the second elements are related via
 `fin.cast`. -/

src/representation_theory/group_cohomology/basic.lean

@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2023 Amelia Livingston. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Amelia Livingston
+-/
+
+import algebra.homology.opposite
+import representation_theory.group_cohomology.resolution
+
+/-!
+# The group cohomology of a `k`-linear `G`-representation
+
+Let `k` be a commutative ring and `G` a group. This file defines the group cohomology of
+`A : Rep k G` to be the cohomology of the complex
+$$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$
+with differential $d^n$ sending $f: G^n \to A$ to the function mapping $(g_0, \dots, g_n)$ to
+$$\rho(g_0)(f(g_1, \dots, g_n))
++ \sum_{i = 0}^{n - 1} (-1)^{i + 1}\cdot f(g_0, \dots, g_ig_{i + 1}, \dots, g_n)$$
+$$+ (-1)^{n + 1}\cdot f(g_0, \dots, g_{n - 1})$$ (where `ρ` is the representation attached to `A`).
+
+We have a `k`-linear isomorphism $\mathrm{Fun}(G^n, A) \cong \mathrm{Hom}(k[G^{n + 1}], A)$, where
+the righthand side is morphisms in `Rep k G`, and the representation on $k[G^{n + 1}]$
+is induced by the diagonal action of `G`. If we conjugate the $n$th differential in
+$\mathrm{Hom}(P, A)$ by this isomorphism, where `P` is the standard resolution of `k` as a trivial
+`k`-linear `G`-representation, then the resulting map agrees with the differential $d^n$ defined
+above, a fact we prove.
+
+This gives us for free a proof that our $d^n$ squares to zero. It also gives us an isomorphism
+$\mathrm{H}^n(G, A) \cong \mathrm{Ext}^n(k, A),$ where $\mathrm{Ext}$ is taken in the category
+`Rep k G`.
+
+## Main definitions
+
+* `group_cohomology.linear_yoneda_obj_resolution A`: a complex whose objects are the representation
+morphisms $\mathrm{Hom}(k[G^{n + 1}], A)$ and whose cohomology is the group cohomology
+$\mathrm{H}^n(G, A)$.
+* `group_cohomology.inhomogeneous_cochains A`: a complex whose objects are
+$\mathrm{Fun}(G^n, A)$ and whose cohomology is the group cohomology $\mathrm{H}^n(G, A).$
+* `group_cohomology.inhomogeneous_cochains_iso A`: an isomorphism between the above two complexes.
+* `group_cohomology A n`: this is $\mathrm{H}^n(G, A),$ defined as the $n$th cohomology of the
+second complex, `inhomogeneous_cochains A`.
+* `group_cohomology_iso_Ext A n`: an isomorphism $\mathrm{H}^n(G, A) \cong \mathrm{Ext}^n(k, A)$
+(where $\mathrm{Ext}$ is taken in the category `Rep k G`) induced by `inhomogeneous_cochains_iso A`.
+
+## Implementation notes
+
+Group cohomology is typically stated for `G`-modules, or equivalently modules over the group ring
+`ℤ[G].` However, `ℤ` can be generalized to any commutative ring `k`, which is what we use.
+Moreover, we express `k[G]`-module structures on a module `k`-module `A` using the `Rep`
+definition. We avoid using instances `module (monoid_algebra k G) A` so that we do not run into
+possible scalar action diamonds.
+
+## TODO
+
+* API for cohomology in low degree: $\mathrm{H}^0, \mathrm{H}^1$ and $\mathrm{H}^2.$ For example,
+the inflation-restriction exact sequence.
+* The long exact sequence in cohomology attached to a short exact sequence of representations.
+* Upgrading `group_cohomology_iso_Ext` to an isomorphism of derived functors.
+* Profinite cohomology.
+
+Longer term:
+* The Hochschild-Serre spectral sequence (this is perhaps a good toy example for the theory of
+spectral sequences in general).
+-/
+
+noncomputable theory
+universes u
+
+variables {k G : Type u} [comm_ring k] {n : ℕ}
+
+open category_theory
+namespace group_cohomology
+variables [monoid G]
+
+/-- The complex `Hom(P, A)`, where `P` is the standard resolution of `k` as a trivial `k`-linear
+`G`-representation. -/
+abbreviation linear_yoneda_obj_resolution (A : Rep k G) : cochain_complex (Module.{u} k) ℕ :=
+homological_complex.unop
+  ((((linear_yoneda k (Rep k G)).obj A).right_op.map_homological_complex _).obj (resolution k G))
+
+lemma linear_yoneda_obj_resolution_d_apply {A : Rep k G} (i j : ℕ) (x : (resolution k G).X i ⟶ A) :
+  (linear_yoneda_obj_resolution A).d i j x = (resolution k G).d j i ≫ x :=
+rfl
+
+end group_cohomology
+namespace inhomogeneous_cochains
+open Rep group_cohomology
+
+/-- The differential in the complex of inhomogeneous cochains used to
+calculate group cohomology. -/
+@[simps] def d [monoid G] (n : ℕ) (A : Rep k G) :
+  ((fin n → G) → A) →ₗ[k] (fin (n + 1) → G) → A :=
+{ to_fun := λ f g, A.ρ (g 0) (f (λ i, g i.succ))
+    + finset.univ.sum (λ j : fin (n + 1), (-1 : k) ^ ((j : ℕ) + 1) • f (fin.contract_nth j (*) g)),
+  map_add' := λ f g,
+  begin
+    ext x,
+    simp only [pi.add_apply, map_add, smul_add, finset.sum_add_distrib, add_add_add_comm],
+  end,
+  map_smul' := λ r f,
+  begin
+    ext x,
+    simp only [pi.smul_apply, ring_hom.id_apply, map_smul, smul_add, finset.smul_sum,
+      ←smul_assoc, smul_eq_mul, mul_comm r],
+  end }
+
+variables [group G] (n) (A : Rep k G)
+
+/-- The theorem that our isomorphism `Fun(Gⁿ, A) ≅ Hom(k[Gⁿ⁺¹], A)` (where the righthand side is
+morphisms in `Rep k G`) commutes with the differentials in the complex of inhomogeneous cochains
+and the homogeneous `linear_yoneda_obj_resolution`. -/
+lemma d_eq :
+  d n A = ((diagonal_hom_equiv n A).to_Module_iso.inv
+    ≫ (linear_yoneda_obj_resolution A).d n (n + 1)
+    ≫ (diagonal_hom_equiv (n + 1) A).to_Module_iso.hom) :=
+begin
+  ext f g,
+  simp only [Module.coe_comp, linear_equiv.coe_coe, function.comp_app,
+    linear_equiv.to_Module_iso_inv, linear_yoneda_obj_resolution_d_apply,
+    linear_equiv.to_Module_iso_hom, diagonal_hom_equiv_apply, Action.comp_hom,
+    resolution.d_eq k G n, resolution.d_of (fin.partial_prod g), linear_map.map_sum,
+    ←finsupp.smul_single_one _ ((-1 : k) ^ _), map_smul, d_apply],
+  simp only [@fin.sum_univ_succ _ _ (n + 1), fin.coe_zero, pow_zero, one_smul, fin.succ_above_zero,
+    diagonal_hom_equiv_symm_apply f (fin.partial_prod g ∘ @fin.succ (n + 1)), function.comp_app,
+    fin.partial_prod_succ, fin.cast_succ_zero, fin.partial_prod_zero, one_mul],
+  congr' 1,
+  { congr,
+    ext,
+    have := fin.partial_prod_right_inv (1 : G) g (fin.cast_succ x),
+    simp only [mul_inv_rev, fin.coe_eq_cast_succ, one_smul, fin.cast_succ_fin_succ] at *,
+    rw [mul_assoc, ←mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left] },
+  { exact finset.sum_congr rfl (λ j hj,
+      by rw [diagonal_hom_equiv_symm_partial_prod_succ, fin.coe_succ]) }
+end
+
+end inhomogeneous_cochains
+namespace group_cohomology
+variables [group G] (n) (A : Rep k G)
+
+open inhomogeneous_cochains
+
+/-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous cochains
+$$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$
+which calculates the group cohomology of `A`. -/
+noncomputable abbreviation inhomogeneous_cochains : cochain_complex (Module k) ℕ :=
+cochain_complex.of (λ n, Module.of k ((fin n → G) → A))
+(λ n, inhomogeneous_cochains.d n A) (λ n,
+begin
+  ext x y,
+  have := linear_map.ext_iff.1 ((linear_yoneda_obj_resolution A).d_comp_d n (n + 1) (n + 2)),
+  simp only [Module.coe_comp, function.comp_app] at this,
+  simp only [Module.coe_comp, function.comp_app, d_eq, linear_equiv.to_Module_iso_hom,
+    linear_equiv.to_Module_iso_inv, linear_equiv.coe_coe, linear_equiv.symm_apply_apply,
+    this, linear_map.zero_apply, map_zero, pi.zero_apply],
+end)
+
+/-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous cochains is isomorphic
+to `Hom(P, A)`, where `P` is the standard resolution of `k` as a trivial `G`-representation. -/
+def inhomogeneous_cochains_iso :
+  inhomogeneous_cochains A ≅ linear_yoneda_obj_resolution A :=
+homological_complex.hom.iso_of_components
+  (λ i, (Rep.diagonal_hom_equiv i A).to_Module_iso.symm) $
+begin
+  rintros i j (h : i + 1 = j),
+  subst h,
+  simp only [cochain_complex.of_d, d_eq, category.assoc, iso.symm_hom,
+    iso.hom_inv_id, category.comp_id],
+end
+
+end group_cohomology
+open group_cohomology
+
+/-- The group cohomology of a `k`-linear `G`-representation `A`, as the cohomology of its complex
+of inhomogeneous cochains. -/
+def group_cohomology [group G] (A : Rep k G) (n : ℕ) : Module k :=
+(inhomogeneous_cochains A).homology n
+
+/-- The `n`th group cohomology of a `k`-linear `G`-representation `A` is isomorphic to
+`Extⁿ(k, A)` (taken in `Rep k G`), where `k` is a trivial `k`-linear `G`-representation. -/
+def group_cohomology_iso_Ext [group G] (A : Rep k G) (n : ℕ) :
+  group_cohomology A n ≅ ((Ext k (Rep k G) n).obj
+    (opposite.op $ Rep.trivial k G k)).obj A :=
+(homology_obj_iso_of_homotopy_equiv (homotopy_equiv.of_iso (inhomogeneous_cochains_iso _)) _)
+  ≪≫ (homological_complex.homology_unop _ _) ≪≫ (Ext_iso k G A n).symm

src/representation_theory/group_cohomology_resolution.lean → src/representation_theory/group_cohomology/resolution.lean

@@ -232,25 +232,25 @@ module.free.of_basis (of_mul_action_basis k G n)
 end basis
 end group_cohomology.resolution
 namespace Rep
-variables (n) [group G]
+variables (n) [group G] (A : Rep k G)
 open group_cohomology.resolution
 
 /-- 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`. -/
-noncomputable def diagonal_hom_equiv (A : Rep k G) :
+noncomputable def diagonal_hom_equiv :
   (Rep.of_mul_action k G (fin (n + 1) → G) ⟶ A) ≃ₗ[k] ((fin n → G) → A) :=
 linear.hom_congr k ((diagonal_succ k G n).trans
   ((representation.of_mul_action k G G).Rep_of_tprod_iso 1)) (iso.refl _) ≪≫ₗ
   ((Rep.monoidal_closed.linear_hom_equiv_comm _ _ _) ≪≫ₗ (Rep.left_regular_hom_equiv _))
   ≪≫ₗ (finsupp.llift A k k (fin n → G)).symm
 
-variables {n}
+variables {n A}
 
 /-- 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ₙ).` -/
-lemma diagonal_hom_equiv_apply {A : Rep k G} (f : Rep.of_mul_action k G (fin (n + 1) → G) ⟶ A)
+lemma diagonal_hom_equiv_apply (f : Rep.of_mul_action k G (fin (n + 1) → G) ⟶ A)
   (x : fin n → G) : diagonal_hom_equiv n A f x = f.hom (finsupp.single (fin.partial_prod x) 1) :=
 begin
   unfold diagonal_hom_equiv,
@@ -266,7 +266,7 @@ the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`.
 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`. -/
-lemma diagonal_hom_equiv_symm_apply {A : Rep k G} (f : (fin n → G) → A) (x : fin (n + 1) → G) :
+lemma diagonal_hom_equiv_symm_apply (f : (fin n → G) → A) (x : fin (n + 1) → G) :
   ((diagonal_hom_equiv n A).symm f).hom (finsupp.single x 1)
     = A.ρ (x 0) (f (λ (i : fin n), (x ↑i)⁻¹ * x i.succ)) :=
 begin
@@ -281,6 +281,22 @@ begin
     finsupp.llift_apply A k k],
 end
 
+/-- 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. -/
+lemma diagonal_hom_equiv_symm_partial_prod_succ
+  (f : (fin n → G) → A) (g : fin (n + 1) → G) (a : fin (n + 1)) :
+  ((diagonal_hom_equiv n A).symm f).hom (finsupp.single (fin.partial_prod g ∘ a.succ.succ_above) 1)
+    = f (fin.contract_nth a (*) g) :=
+begin
+  simp only [diagonal_hom_equiv_symm_apply, function.comp_app, fin.succ_succ_above_zero,
+    fin.partial_prod_zero, map_one, fin.coe_eq_cast_succ, fin.succ_succ_above_succ,
+    linear_map.one_apply, fin.partial_prod_succ],
+  congr,
+  ext,
+  rw [←fin.partial_prod_succ, fin.inv_partial_prod_mul_eq_contract_nth],
+end
+
 end Rep
 variables (G)