feat(representation_theory/group_cohomology_resolution): show k[G^(n …

…+ 1)] is free over k[G] (#15501)

Defines an isomorphism $k[G^{n + 1}] \cong k[G] \otimes_k k[G^n].$ Also shows that given a $k$-algebra $R$ and a $k$-basis for a module $M,$ we get an $R$-basis of $R \otimes_k M.$ Then, using that, we show $k[G^{n + 1}]$ is free.

src/algebra/big_operators/fin.lean

@@ -181,6 +181,29 @@ by simp [partial_prod, list.take_succ, list.of_fn_nth_val, dif_pos j.is_lt, ←o
   partial_prod f j.succ = f 0 * partial_prod (fin.tail f) j :=
 by simpa [partial_prod]
 
+@[to_additive] lemma partial_prod_left_inv {G : Type*} [group G] (f : fin (n + 1) → G) :
+  f 0 • partial_prod (λ i : fin n, (f i)⁻¹ * f i.succ) = f :=
+funext $ λ x, fin.induction_on x (by simp) (λ x hx,
+begin
+  simp only [coe_eq_cast_succ, pi.smul_apply, smul_eq_mul] at hx ⊢,
+  rw [partial_prod_succ, ←mul_assoc, hx, mul_inv_cancel_left],
+end)
+
+@[to_additive] lemma partial_prod_right_inv {G : Type*} [group G]
+  (g : G) (f : fin n → G) (i : fin n) :
+  ((g • partial_prod f) i)⁻¹ * (g • partial_prod f) i.succ = f i :=
+begin
+  cases i with i hn,
+  induction i with i hi generalizing hn,
+  { simp [←fin.succ_mk, partial_prod_succ] },
+  { specialize hi (lt_trans (nat.lt_succ_self i) hn),
+    simp only [mul_inv_rev, fin.coe_eq_cast_succ, fin.succ_mk, fin.cast_succ_mk,
+      smul_eq_mul, pi.smul_apply] at hi ⊢,
+    rw [←fin.succ_mk _ _ (lt_trans (nat.lt_succ_self _) hn), ←fin.succ_mk],
+    simp only [partial_prod_succ, mul_inv_rev, fin.cast_succ_mk],
+    assoc_rw [hi, inv_mul_cancel_left] }
+end
+
 end partial_prod
 
 end fin

src/linear_algebra/basic.lean

@@ -117,6 +117,22 @@ end
   (linear_equiv_fun_on_fintype R M α).symm f = f :=
 by { ext, simp [linear_equiv_fun_on_fintype], }
 
+/-- If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is
+`R`-linearly equivalent to `M`. -/
+noncomputable def linear_equiv.finsupp_unique (α : Type*) [unique α] : (α →₀ M) ≃ₗ[R] M :=
+{ map_add' := λ x y, rfl,
+  map_smul' := λ r x, rfl,
+  ..finsupp.equiv_fun_on_fintype.trans (equiv.fun_unique α M) }
+
+variables {R M α}
+
+@[simp] lemma linear_equiv.finsupp_unique_apply (α : Type*) [unique α] (f : α →₀ M) :
+  linear_equiv.finsupp_unique R M α f = f default := rfl
+
+@[simp] lemma linear_equiv.finsupp_unique_symm_apply {α : Type*} [unique α] (m : M) :
+  (linear_equiv.finsupp_unique R M α).symm m = finsupp.single default m :=
+by ext; simp [linear_equiv.finsupp_unique]
+
 end finsupp
 
 /-- decomposing `x : ι → R` as a sum along the canonical basis -/

src/logic/equiv/basic.lean

@@ -629,10 +629,28 @@ calc punit × α ≃ α × punit : prod_comm _ _
 def prod_unique (α β : Type*) [unique β] : α × β ≃ α :=
 ((equiv.refl α).prod_congr $ equiv_punit β).trans $ prod_punit α
 
+@[simp] lemma coe_prod_unique {α β : Type*} [unique β] :
+  ⇑(prod_unique α β) = prod.fst := rfl
+
+lemma prod_unique_apply {α β : Type*} [unique β] (x : α × β) :
+  prod_unique α β x = x.1 := rfl
+
+@[simp] lemma prod_unique_symm_apply {α β : Type*} [unique β] (x : α) :
+  (prod_unique α β).symm x = (x, default) := rfl
+
 /-- Any `unique` type is a left identity for type product up to equivalence. -/
 def unique_prod (α β : Type*) [unique β] : β × α ≃ α :=
 ((equiv_punit β).prod_congr $ equiv.refl α).trans $ punit_prod α
 
+@[simp] lemma coe_unique_prod {α β : Type*} [unique β] :
+  ⇑(unique_prod α β) = prod.snd := rfl
+
+lemma unique_prod_apply {α β : Type*} [unique β] (x : β × α) :
+  unique_prod α β x = x.2 := rfl
+
+@[simp] lemma unique_prod_symm_apply {α β : Type*} [unique β] (x : α) :
+  (unique_prod α β).symm x = (default, x) := rfl
+
 /-- `empty` type is a right absorbing element for type product up to an equivalence. -/
 def prod_empty (α : Type*) : α × empty ≃ empty :=
 equiv_empty _

src/representation_theory/basic.lean

@@ -93,7 +93,7 @@ which we equip with an instance `module (monoid_algebra k G) ρ.as_module`.
 
 You should use `as_module_equiv : ρ.as_module ≃+ V` to translate terms.
 -/
-@[nolint unused_arguments, derive add_comm_monoid]
+@[nolint unused_arguments, derive [add_comm_monoid, module (module.End k V)]]
 def as_module (ρ : representation k G V) := V
 
 instance : inhabited ρ.as_module := ⟨0⟩
@@ -103,10 +103,7 @@ A `k`-linear representation of `G` on `V` can be thought of as
 a module over `monoid_algebra k G`.
 -/
 noncomputable instance as_module_module : module (monoid_algebra k G) ρ.as_module :=
-begin
-  change module (monoid_algebra k G) V,
-  exact module.comp_hom V (as_algebra_hom ρ).to_ring_hom,
-end
+module.comp_hom V (as_algebra_hom ρ).to_ring_hom
 
 /--
 The additive equivalence from the `module (monoid_algebra k G)` to the original vector space
@@ -264,6 +261,20 @@ begin
   simp only [of_mul_action_def, finsupp.lmap_domain_apply, finsupp.map_domain_apply, hg],
 end
 
+lemma of_mul_action_self_smul_eq_mul
+  (x : monoid_algebra k G) (y : (of_mul_action k G G).as_module) :
+  x • y = (x * y : monoid_algebra k G) :=
+x.induction_on (λ g, by show as_algebra_hom _ _ _ = _; ext; simp)
+  (λ x y hx hy, by simp only [hx, hy, add_mul, add_smul])
+  (λ r x hx, by show as_algebra_hom _ _ _ = _; simpa [←hx])
+
+/-- If we equip `k[G]` with the `k`-linear `G`-representation induced by the left regular action of
+`G` on itself, the resulting object is isomorphic as a `k[G]`-module to `k[G]` with its natural
+`k[G]`-module structure. -/
+@[simps] noncomputable def of_mul_action_self_as_module_equiv :
+  (of_mul_action k G G).as_module ≃ₗ[monoid_algebra k G] monoid_algebra k G :=
+{ map_smul' := of_mul_action_self_smul_eq_mul, ..as_module_equiv _ }
+
 /--
 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`.
@@ -298,6 +309,27 @@ local notation ρV ` ⊗ ` ρW := tprod ρV ρW
 @[simp]
 lemma tprod_apply (g : G) : (ρV ⊗ ρW) g = tensor_product.map (ρV g) (ρW g) := rfl
 
+lemma smul_tprod_one_as_module (r : monoid_algebra k G) (x : V) (y : W) :
+  (r • (x ⊗ₜ y) : (ρV.tprod 1).as_module) = (r • x : ρV.as_module) ⊗ₜ y :=
+begin
+  show as_algebra_hom _ _ _ = as_algebra_hom _ _ _ ⊗ₜ _,
+  simp only [as_algebra_hom_def, monoid_algebra.lift_apply,
+    tprod_apply, monoid_hom.one_apply, linear_map.finsupp_sum_apply,
+    linear_map.smul_apply, tensor_product.map_tmul, linear_map.one_apply],
+  simp only [finsupp.sum, tensor_product.sum_tmul],
+  refl,
+end
+
+lemma smul_one_tprod_as_module (r : monoid_algebra k G) (x : V) (y : W) :
+  (r • (x ⊗ₜ y) : ((1 : representation k G V).tprod ρW).as_module) = x ⊗ₜ (r • y : ρW.as_module) :=
+begin
+  show as_algebra_hom _ _ _ = _ ⊗ₜ as_algebra_hom _ _ _,
+  simp only [as_algebra_hom_def, monoid_algebra.lift_apply,
+    tprod_apply, monoid_hom.one_apply, linear_map.finsupp_sum_apply,
+    linear_map.smul_apply, tensor_product.map_tmul, linear_map.one_apply],
+  simp only [finsupp.sum, tensor_product.tmul_sum, tensor_product.tmul_smul],
+end
+
 end tensor_product
 
 section linear_hom

src/representation_theory/group_cohomology_resolution.lean

@@ -13,20 +13,22 @@ This file contains facts about an important `k[G]`-module structure on `k[Gⁿ]`
 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
+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.
+
 ## Main definitions
 
  * `group_cohomology.resolution.to_tensor`
  * `group_cohomology.resolution.of_tensor`
  * `Rep.of_mul_action`
+ * `group_cohomology.resolution.equiv_tensor`
+ * `group_cohomology.resolution.of_mul_action_basis`
 
 ## 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.
 
@@ -79,8 +81,7 @@ 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 only [to_tensor_aux, lift_apply, sum_single_index, tensor_product.smul_tmul'],
   { simp },
 end
 
@@ -99,10 +100,36 @@ lemma of_tensor_aux_comm_of_mul_action (g h : G) (x : 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
 
+lemma to_tensor_aux_left_inv (x : Gⁿ⁺¹ →₀ k) :
+  of_tensor_aux _ _ _ (to_tensor_aux _ _ _ x) = x :=
+begin
+  refine linear_map.ext_iff.1 (@finsupp.lhom_ext _ _ _ k _ _ _ _ _
+    (linear_map.comp (of_tensor_aux _ _ _) (to_tensor_aux _ _ _)) linear_map.id (λ x y, _)) x,
+  dsimp,
+  rw [to_tensor_aux_single x y, of_tensor_aux_single, finsupp.lift_apply, finsupp.sum_single_index,
+    one_smul, fin.partial_prod_left_inv],
+  { rw zero_smul }
+end
+
+lemma to_tensor_aux_right_inv (x : (G →₀ k) ⊗[k] (Gⁿ →₀ k)) :
+  to_tensor_aux _ _ _ (of_tensor_aux _ _ _ x) = x :=
+begin
+  refine tensor_product.induction_on x (by simp) (λ y z, _) (λ z w hz hw, by simp [hz, hw]),
+  rw [←finsupp.sum_single y, finsupp.sum, tensor_product.sum_tmul],
+  simp only [finset.smul_sum, linear_map.map_sum],
+  refine finset.sum_congr rfl (λ f hf, _),
+  simp only [of_tensor_aux_single, finsupp.lift_apply, finsupp.smul_single',
+    linear_map.map_finsupp_sum, to_tensor_aux_single, fin.partial_prod_right_inv],
+  dsimp,
+  simp only [fin.partial_prod_zero, mul_one],
+  conv_rhs {rw [←finsupp.sum_single z, finsupp.sum, tensor_product.tmul_sum]},
+  exact finset.sum_congr rfl (λ g hg, show _ ⊗ₜ _ = _, by
+    rw [←finsupp.smul_single', tensor_product.smul_tmul, finsupp.smul_single_one])
+end
+
 variables (k G n)
 
 /-- Given a `G`-action on `H`, this is `k[H]` bundled with the natural representation
@@ -144,4 +171,55 @@ lemma of_tensor_single' (g : G →₀ k) (x : Gⁿ) (m : k) :
   finsupp.lift _ k G (λ a, single (a • partial_prod x) m) g :=
 by simp [of_tensor, of_tensor_aux]
 
+variables (k G n)
+
+/-- 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ₙ)`. -/
+def equiv_tensor : (Rep.of_mul_action k G (fin (n + 1) → G)) ≅ Rep.of
+  ((representation.of_mul_action k G G).tprod (1 : representation k G ((fin n → G) →₀ k))) :=
+Action.mk_iso (linear_equiv.to_Module_iso
+{ inv_fun := of_tensor_aux k G n,
+  left_inv := to_tensor_aux_left_inv,
+  right_inv := λ x, by convert to_tensor_aux_right_inv x,
+  ..to_tensor_aux k G n }) (to_tensor k G n).comm
+
+-- not quite sure which simp lemmas to make here
+@[simp] lemma equiv_tensor_def :
+  (equiv_tensor k G n).hom = to_tensor k G n := rfl
+
+@[simp] lemma equiv_tensor_inv_def :
+  (equiv_tensor k G n).inv = of_tensor k G n := rfl
+
+/-- 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. -/
+def of_mul_action_basis_aux : (monoid_algebra k G ⊗[k] ((fin n → G) →₀ k)) ≃ₗ[monoid_algebra k G]
+  (of_mul_action k G (fin (n + 1) → G)).as_module :=
+{ map_smul' := λ r x,
+  begin
+    rw [ring_hom.id_apply, linear_equiv.to_fun_eq_coe, ←linear_equiv.map_smul],
+    congr' 1,
+    refine x.induction_on _ (λ x y, _) (λ y z hy hz, _),
+    { simp only [smul_zero] },
+    { simp only [tensor_product.smul_tmul'],
+      show (r * x) ⊗ₜ y = _,
+      rw [←of_mul_action_self_smul_eq_mul, smul_tprod_one_as_module] },
+    { rw [smul_add, hz, hy, smul_add], }
+  end, .. ((Rep.equivalence_Module_monoid_algebra.1).map_iso
+    (equiv_tensor k G n).symm).to_linear_equiv }
+
+/-- A `k[G]`-basis of `k[Gⁿ⁺¹]`, coming from the `k[G]`-linear isomorphism
+`k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹].` -/
+def of_mul_action_basis  :
+  basis (fin n → G) (monoid_algebra k G) (of_mul_action k G (fin (n + 1) → G)).as_module :=
+@basis.map _ (monoid_algebra k G) (monoid_algebra k G ⊗[k] ((fin n → G) →₀ k))
+  _ _ _ _ _ _ (@algebra.tensor_product.basis k _ (monoid_algebra k G) _ _ ((fin n → G) →₀ k) _ _
+  (fin n → G) (⟨linear_equiv.refl k _⟩)) (of_mul_action_basis_aux k G n)
+
+lemma of_mul_action_free :
+  module.free (monoid_algebra k G) (of_mul_action k G (fin (n + 1) → G)).as_module :=
+module.free.of_basis (of_mul_action_basis k G n)
+
 end group_cohomology.resolution

src/ring_theory/tensor_product.lean

@@ -799,7 +799,6 @@ by rw [product_map, alg_hom.range_comp, map_range, map_sup, ←alg_hom.range_com
     lmul'_comp_include_right, alg_hom.id_comp, alg_hom.id_comp]
 
 end
-
 section
 
 variables {R A A' B S : Type*}
@@ -814,7 +813,50 @@ and `g : B →ₐ[R] S` is an `A`-algebra homomorphism. -/
   ..(product_map (f.restrict_scalars R) g).to_ring_hom }
 
 end
+section basis
+
+variables {k : Type*} [comm_ring k] (R : Type*) [ring R] [algebra k R] {M : Type*}
+  [add_comm_monoid M] [module k M] {ι : Type*} (b : basis ι k M)
+
+/-- Given a `k`-algebra `R` and a `k`-basis of `M,` this is a `k`-linear isomorphism
+`R ⊗[k] M ≃ (ι →₀ R)` (which is in fact `R`-linear). -/
+noncomputable def basis_aux : R ⊗[k] M ≃ₗ[k] (ι →₀ R) :=
+(_root_.tensor_product.congr (finsupp.linear_equiv.finsupp_unique k R punit).symm b.repr) ≪≫ₗ
+  (finsupp_tensor_finsupp k R k punit ι).trans (finsupp.lcongr (equiv.unique_prod ι punit)
+  (_root_.tensor_product.rid k R))
+
+variables {R}
+
+lemma basis_aux_tmul (r : R) (m : M) :
+  basis_aux R b (r ⊗ₜ m) = r • (finsupp.map_range (algebra_map k R)
+    (map_zero _) (b.repr m)) :=
+begin
+  ext,
+  simp [basis_aux, ←algebra.commutes, algebra.smul_def],
+end
+
+lemma basis_aux_map_smul (r : R) (x : R ⊗[k] M) :
+  basis_aux R b (r • x) = r • basis_aux R b x :=
+tensor_product.induction_on x (by simp) (λ x y, by simp only [tensor_product.smul_tmul',
+  basis_aux_tmul, smul_assoc]) (λ x y hx hy, by simp [hx, hy])
+
+variables (R)
+
+/-- Given a `k`-algebra `R`, this is the `R`-basis of `R ⊗[k] M` induced by a `k`-basis of `M`. -/
+noncomputable def basis : basis ι R (R ⊗[k] M) :=
+{ repr := { map_smul' := basis_aux_map_smul b, .. basis_aux R b } }
+
+variables {R}
+
+@[simp] lemma basis_repr_tmul (r : R) (m : M) :
+  (basis R b).repr (r ⊗ₜ m) = r • (finsupp.map_range (algebra_map k R) (map_zero _) (b.repr m)) :=
+basis_aux_tmul _ _ _
+
+@[simp] lemma basis_repr_symm_apply (r : R) (i : ι) :
+  (basis R b).repr.symm (finsupp.single i r) = r ⊗ₜ b.repr.symm (finsupp.single i 1) :=
+by simp [basis, equiv.unique_prod_symm_apply, basis_aux]
 
+end basis
 end tensor_product
 end algebra