English
For f and g, φ and ψ, and n, the level-n cycles maps compose coherently with chain maps: (cyclesMap f φ).f n ≫ (chainsIso₂ B).hom = (chainsIso₂ A).hom ≫ cyclesMap₂ f φ.
Русский
На уровне n карты циклов компонуются согласованно с цепными отображениями: (cyclesMap f φ).f n ≫ (chainsIso₂ B).hom = (chainsIso₂ A).hom ≫ cyclesMap₂ f φ.
LaTeX
$$$(\mathrm{cyclesMap} f φ).f n \; ; \; (\mathrm{chainsIso}_2 B).hom = (\mathrm{chainsIso}_2 A).hom \; ; \; \mathrm{cyclesMap}_2 f φ$$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map sending `∑ aᵢ·(gᵢ₁, gᵢ₂) : G × G →₀ A` to
`∑ φ(aᵢ)·(f(gᵢ₁), f(gᵢ₂)) : H × H →₀ B`. -/
noncomputable abbrev chainsMap₂ : ModuleCat.of k (G × G →₀ A) ⟶ ModuleCat.of k (H × H →₀ B) :=
ModuleCat.ofHom <| mapRange.linearMap φ.hom.hom ∘ₗ lmapDomain A k (Prod.map f f)
