English
There is a morphism of short complexes from A’s shortComplexH1 to B’s, built from φ, cochainsMap₁, and cochainsMap₂, with coherence conditions encoded by commutativity diagrams.
Русский
Существует отображение между короткими комплексами groupCohomology.shortComplexH1(A) и groupCohomology.shortComplexH1(B), построенное из φ, cochainsMap₁ и cochainsMap₂, удовлетворяющее условиям совместимости.
LaTeX
$$$$ mapShortComplexH1 A B f φ : \\; shortComplexH1 A \\to shortComplexH1 B $$$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map from the short complex `A --d₀₁--> Fun(H, A) --d₁₂--> Fun(H × H, A)`
to `B --d₀₁--> Fun(G, B) --d₁₂--> Fun(G × G, B)`. -/
@[simps]
noncomputable def mapShortComplexH1 : shortComplexH1 A ⟶ shortComplexH1 B
where
τ₁ := φ.hom
τ₂ := cochainsMap₁ f φ
τ₃ := cochainsMap₂ f φ
comm₁₂ := by
ext x
funext g
simpa [shortComplexH1, d₀₁, cochainsMap₁] using (hom_comm_apply φ g x).symm
comm₂₃ := by
ext x
funext g
simpa [shortComplexH1, d₁₂, cochainsMap₁, cochainsMap₂] using (hom_comm_apply φ _ _).symm
