English
There is a canonical map from H1 A to the tensor product, respecting group action, when A is trivial.
Русский
Существует каноническое отображение из H1 A в тензорный произведение с сохранением действия группы, когда A тривиально.
LaTeX
$$def H1ToTensorOfIsTrivial : H1 A →ₗ[ℤ] (Additive <| Abelianization G) ⊗[ℤ] A$$
Lean4
/-- If a `G`-representation on `A` is trivial, this is the natural map `H₁(G, A) → Gᵃᵇ ⊗[ℤ] A`
sending `⟦single g a⟧` to `⟦g⟧ ⊗ₜ a`. -/
def H1ToTensorOfIsTrivial : H1 A →ₗ[ℤ] (Additive <| Abelianization G) ⊗[ℤ] A :=
((QuotientAddGroup.lift _
((Finsupp.liftAddHom fun g =>
AddMonoidHomClass.toAddMonoidHom (TensorProduct.mk ℤ _ _ (Additive.ofMul (Abelianization.of g)))).comp
(cycles₁ A).toAddSubgroup.subtype)
fun ⟨y, hy⟩ ⟨z, hz⟩ =>
AddMonoidHom.mem_ker.2 <| by
simp [← hz, d₂₁, sum_sum_index, sum_add_index', tmul_add, sum_sub_index, tmul_sub, shortComplexH1]).comp <|
AddMonoidHomClass.toAddMonoidHom (H1Iso A).hom.hom).toIntLinearMap
