English
There is a map of short complexes induced by f and φ between the short complex H1s; the construction uses τ1, τ2, τ3 that satisfy commutativity relations.
Русский
Существуют отображения между короткими комплексами H1, индуцируемые f и φ; в построение входят τ1, τ2, τ3, удовлетворяющие условиям коммутативности.
LaTeX
$$$mapShortComplexH1 : (A \to B) \to (shortComplexH1 A \to shortComplexH1 B)$$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map from the short complex `(G × G →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A`
to `(H × H →₀ B) --d₂₁--> (H →₀ B) --d₁₀--> B`. -/
@[simps]
noncomputable def mapShortComplexH1 : shortComplexH1 A ⟶ shortComplexH1 B
where
τ₁ := chainsMap₂ f φ
τ₂ := chainsMap₁ f φ
τ₃ := φ.hom
comm₁₂ := by
simp only [shortComplexH1]
ext : 3
simpa [d₂₁, map_add, map_sub, ← map_inv] using congr(single _ $((hom_comm_apply φ _ _).symm))
comm₂₃ := by
simp only [shortComplexH1]
ext : 3
simpa [← map_inv, d₁₀] using (hom_comm_apply φ _ _).symm
