mapCycles₁ — Mathlib

English

There is a canonical induced map mapCycles₁ : cycles₁ A → cycles₁ B associated to a group homomorphism f and a representation morphism φ: A ⟶ (Res f) B.

Русский

Существует каноническое индуцированное отображение mapCycles₁: cycles₁ A → cycles₁ B, связанное с гомоморфизмом группы f и отображением φ: A ⟶ Res(f) B.

LaTeX

$$$ mapCycles_1(f, \varphi) : \mathrm{cycles}_1(A) \to \mathrm{cycles}_1(B) $$$

Lean4

/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map `Z₁(G, A) ⟶ Z₁(H, B)`. -/
noncomputable abbrev mapCycles₁ : ModuleCat.of k (cycles₁ A) ⟶ ModuleCat.of k (cycles₁ B) :=
  ShortComplex.cyclesMap' (mapShortComplexH1 f φ) (shortComplexH1 A).moduleCatLeftHomologyData
    (shortComplexH1 B).moduleCatLeftHomologyData

Похожие утверждения