English
The cochains functoriality respects both maps and identity in a functor from representations to cochain complexes.
Русский
Сопряжённость коцепей сохраняется под действием отображений и единичного гомоморфизма в соответствующем функторе.
LaTeX
$$$\mathrm{cochainsFunctor}$$$
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
`Fun(H, A) --d₁₂--> Fun(H × H, A) --d₂₃--> Fun(H × H × H, A)` to
`Fun(G, B) --d₁₂--> Fun(G × G, B) --d₂₃--> Fun(G × G × G, B)`. -/
@[simps]
noncomputable def mapShortComplexH2 : shortComplexH2 A ⟶ shortComplexH2 B
where
τ₁ := cochainsMap₁ f φ
τ₂ := cochainsMap₂ f φ
τ₃ := cochainsMap₃ f φ
comm₁₂ := by
ext x
funext g
simpa [shortComplexH2, d₁₂, cochainsMap₁, cochainsMap₂] using (hom_comm_apply φ _ _).symm
comm₂₃ := by
ext x
funext g
simpa [shortComplexH2, d₂₃, cochainsMap₂, cochainsMap₃] using (hom_comm_apply φ _ _).symm
