From 67761c325022cf81c5dbcd3749d7b6637c2bcc15 Mon Sep 17 00:00:00 2001 From: Amelia Livingston <101damnations@github.com> Date: Mon, 11 Jul 2022 19:17:26 +0000 Subject: [PATCH] feat(representation_theory/monoid_algebra_basis): add some API for `k[G^n]` (#14308) Co-authored-by: Oliver Nash --- src/algebra/big_operators/fin.lean | 34 +++- src/representation_theory/basic.lean | 24 +++ .../group_cohomology_resolution.lean | 147 ++++++++++++++++++ 3 files changed, 203 insertions(+), 2 deletions(-) create mode 100644 src/representation_theory/group_cohomology_resolution.lean diff --git a/src/algebra/big_operators/fin.lean b/src/algebra/big_operators/fin.lean index b006f3ce286c7..01763403f7769 100644 --- a/src/algebra/big_operators/fin.lean +++ b/src/algebra/big_operators/fin.lean @@ -135,12 +135,40 @@ lemma prod_trunc {M : Type*} [comm_monoid M] {a b : ℕ} (f : fin (a+b) → M) ∏ (i : fin a), f (cast_le (nat.le.intro rfl) i) := by simpa only [prod_univ_add, fintype.prod_eq_one _ hf, mul_one] +section partial_prod + +variables [monoid α] {n : ℕ} + +/-- For `f = (a₁, ..., aₙ)` in `αⁿ`, `partial_prod f` is `(1, a₁, a₁a₂, ..., a₁...aₙ)` in `αⁿ⁺¹`. -/ +@[to_additive "For `f = (a₁, ..., aₙ)` in `αⁿ`, `partial_sum f` is +`(0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ)` in `αⁿ⁺¹`."] +def partial_prod (f : fin n → α) (i : fin (n + 1)) : α := +((list.of_fn f).take i).prod + +@[simp, to_additive] lemma partial_prod_zero (f : fin n → α) : + partial_prod f 0 = 1 := +by simp [partial_prod] + +@[to_additive] lemma partial_prod_succ (f : fin n → α) (j : fin n) : + partial_prod f j.succ = partial_prod f j.cast_succ * (f j) := +by simp [partial_prod, list.take_succ, list.of_fn_nth_val, dif_pos j.is_lt, ←option.coe_def] + +@[to_additive] lemma partial_prod_succ' (f : fin (n + 1) → α) (j : fin (n + 1)) : + partial_prod f j.succ = f 0 * partial_prod (fin.tail f) j := +by simpa [partial_prod] + +end partial_prod + end fin namespace list +section comm_monoid + +variables [comm_monoid α] + @[to_additive] -lemma prod_take_of_fn [comm_monoid α] {n : ℕ} (f : fin n → α) (i : ℕ) : +lemma prod_take_of_fn {n : ℕ} (f : fin n → α) (i : ℕ) : ((of_fn f).take i).prod = ∏ j in finset.univ.filter (λ (j : fin n), j.val < i), f j := begin have A : ∀ (j : fin n), ¬ ((j : ℕ) < 0) := λ j, not_lt_bot, @@ -167,7 +195,7 @@ begin end @[to_additive] -lemma prod_of_fn [comm_monoid α] {n : ℕ} {f : fin n → α} : +lemma prod_of_fn {n : ℕ} {f : fin n → α} : (of_fn f).prod = ∏ i, f i := begin convert prod_take_of_fn f n, @@ -176,6 +204,8 @@ begin simp [this] } end +end comm_monoid + lemma alternating_sum_eq_finset_sum {G : Type*} [add_comm_group G] : ∀ (L : list G), alternating_sum L = ∑ i : fin L.length, (-1 : ℤ) ^ (i : ℕ) • L.nth_le i i.is_lt | [] := by { rw [alternating_sum, finset.sum_eq_zero], rintro ⟨i, ⟨⟩⟩ } diff --git a/src/representation_theory/basic.lean b/src/representation_theory/basic.lean index d865818794286..456791264b02f 100644 --- a/src/representation_theory/basic.lean +++ b/src/representation_theory/basic.lean @@ -92,11 +92,35 @@ noncomputable def as_module : module (monoid_algebra k G) V := end monoid_algebra +section mul_action +variables (k : Type*) [comm_semiring k] (G : Type*) [monoid G] (H : Type*) [mul_action G H] + +/-- A `G`-action on `H` induces a representation `G →* End(k[H])` in the natural way. -/ +noncomputable def of_mul_action : representation k G (H →₀ k) := +{ to_fun := λ g, finsupp.lmap_domain k k ((•) g), + map_one' := by { ext x y, dsimp, simp }, + map_mul' := λ x y, by { ext z w, simp [mul_smul] }} + +variables {k G H} + +lemma of_mul_action_def (g : G) : of_mul_action k G H g = finsupp.lmap_domain k k ((•) g) := rfl + +end mul_action section group variables {k G V : Type*} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] variables (ρ : representation k G V) +@[simp] lemma of_mul_action_apply {H : Type*} [mul_action G H] + (g : G) (f : H →₀ k) (h : H) : of_mul_action k G H g f h = f (g⁻¹ • h) := +begin + conv_lhs { rw ← smul_inv_smul g h, }, + let h' := g⁻¹ • h, + change of_mul_action k G H g f (g • h') = f h', + have hg : function.injective ((•) g : H → H), { intros h₁ h₂, simp, }, + simp only [of_mul_action_def, finsupp.lmap_domain_apply, finsupp.map_domain_apply, hg], +end + /-- When `G` is a group, a `k`-linear representation of `G` on `V` can be thought of as a group homomorphism from `G` into the invertible `k`-linear endomorphisms of `V`. diff --git a/src/representation_theory/group_cohomology_resolution.lean b/src/representation_theory/group_cohomology_resolution.lean new file mode 100644 index 0000000000000..3536193182c0a --- /dev/null +++ b/src/representation_theory/group_cohomology_resolution.lean @@ -0,0 +1,147 @@ +/- +Copyright (c) 2022 Amelia Livingston. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Amelia Livingston +-/ +import representation_theory.Rep +import representation_theory.basic + +/-! +# 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 morphisms of `k`-linear `G`-representations between `k[Gⁿ⁺¹]` and +`k[G] ⊗ₖ k[Gⁿ]` (on which `G` acts by `ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x`). + +## Main definitions + + * `group_cohomology.resolution.to_tensor` + * `group_cohomology.resolution.of_tensor` + * `Rep.of_mul_action` + +## TODO + + * Show that `group_cohomology.resolution.to_tensor` and `group_cohomology.resolution.of_tensor` are + mutually inverse. + * Use the above to deduce that `k[Gⁿ⁺¹]` is free over `k[G]`. + * 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 theory + +universes u + +variables {k G : Type u} [comm_ring k] {n : ℕ} + +open_locale tensor_product + +local notation `Gⁿ` := fin n → G +local notation `Gⁿ⁺¹` := fin (n + 1) → G + +namespace group_cohomology.resolution + +open finsupp (hiding lift) fin (partial_prod) representation + +variables (k G n) [group G] + +/-- The `k`-linear map from `k[Gⁿ⁺¹]` to `k[G] ⊗ₖ k[Gⁿ]` sending `(g₀, ..., gₙ)` +to `g₀ ⊗ (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)`. -/ +def to_tensor_aux : + ((fin (n + 1) → G) →₀ k) →ₗ[k] (G →₀ k) ⊗[k] ((fin n → G) →₀ k) := +finsupp.lift ((G →₀ k) ⊗[k] ((fin n → G) →₀ k)) k (fin (n + 1) → G) + (λ x, single (x 0) 1 ⊗ₜ[k] single (λ i, (x i)⁻¹ * x i.succ) 1) + +/-- The `k`-linear map from `k[G] ⊗ₖ k[Gⁿ]` to `k[Gⁿ⁺¹]` sending `g ⊗ (g₁, ..., gₙ)` to +`(g, gg₁, gg₁g₂, ..., gg₁...gₙ)`. -/ +def of_tensor_aux : + (G →₀ k) ⊗[k] ((fin n → G) →₀ k) →ₗ[k] ((fin (n + 1) → G) →₀ k) := +tensor_product.lift (finsupp.lift _ _ _ $ λ g, finsupp.lift _ _ _ + (λ f, single (g • partial_prod f) (1 : k))) + +variables {k G n} + +lemma to_tensor_aux_single (f : Gⁿ⁺¹) (m : k) : + to_tensor_aux k G n (single f m) = single (f 0) m ⊗ₜ single (λ i, (f i)⁻¹ * f i.succ) 1 := +begin + erw [lift_apply, sum_single_index, tensor_product.smul_tmul'], + { simp }, + { simp }, +end + +lemma to_tensor_aux_of_mul_action (g : G) (x : Gⁿ⁺¹) : + to_tensor_aux k G n (of_mul_action k G Gⁿ⁺¹ g (single x 1)) = + tensor_product.map (of_mul_action k G G g) 1 (to_tensor_aux k G n (single x 1)) := +by simp [of_mul_action_def, to_tensor_aux_single, mul_assoc, inv_mul_cancel_left] + +lemma of_tensor_aux_single (g : G) (m : k) (x : Gⁿ →₀ k) : + of_tensor_aux k G n ((single g m) ⊗ₜ x) = + finsupp.lift (Gⁿ⁺¹ →₀ k) k Gⁿ (λ f, single (g • partial_prod f) m) x := +by simp [of_tensor_aux, sum_single_index, smul_sum, mul_comm m] + +lemma of_tensor_aux_comm_of_mul_action (g h : G) (x : Gⁿ) : + of_tensor_aux k G n (tensor_product.map (of_mul_action k G G g) + (1 : module.End k (Gⁿ →₀ k)) (single h (1 : k) ⊗ₜ single x (1 : k))) = + of_mul_action k G Gⁿ⁺¹ g (of_tensor_aux k G n (single h 1 ⊗ₜ single x 1)) := +begin + dsimp, + simp [of_mul_action_def, of_tensor_aux_single, mul_smul], +end + +variables (k G n) + +/-- 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`. -/ +abbreviation _root_.Rep.of_mul_action (G : Type u) [monoid G] (H : Type u) [mul_action G H] : + Rep k G := +Rep.of $ representation.of_mul_action k G H + +/-- 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ₙ)`. -/ +def to_tensor : Rep.of_mul_action k G (fin (n + 1) → G) ⟶ Rep.of + ((representation.of_mul_action k G G).tprod (1 : G →* module.End k ((fin n → G) →₀ k))) := +{ hom := to_tensor_aux k G n, + comm' := λ g, by ext; exact to_tensor_aux_of_mul_action _ _ } + +/-- 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ₙ)`. -/ +def of_tensor : + Rep.of ((representation.of_mul_action k G G).tprod (1 : G →* module.End k ((fin n → G) →₀ k))) + ⟶ Rep.of_mul_action k G (fin (n + 1) → G) := +{ hom := of_tensor_aux k G n, + comm' := λ g, by { ext, congr' 1, exact (of_tensor_aux_comm_of_mul_action _ _ _) }} + +variables {k G n} + +@[simp] lemma to_tensor_single (f : Gⁿ⁺¹) (m : k) : + (to_tensor k G n).hom (single f m) = single (f 0) m ⊗ₜ single (λ i, (f i)⁻¹ * f i.succ) 1 := +to_tensor_aux_single _ _ + +@[simp] lemma of_tensor_single (g : G) (m : k) (x : Gⁿ →₀ k) : + (of_tensor k G n).hom ((single g m) ⊗ₜ x) = + finsupp.lift (Rep.of_mul_action k G Gⁿ⁺¹) k Gⁿ (λ f, single (g • partial_prod f) m) x := +of_tensor_aux_single _ _ _ + +lemma of_tensor_single' (g : G →₀ k) (x : Gⁿ) (m : k) : + (of_tensor k G n).hom (g ⊗ₜ single x m) = + finsupp.lift _ k G (λ a, single (a • partial_prod x) m) g := +by simp [of_tensor, of_tensor_aux] + +end group_cohomology.resolution