chainsMap₁ — Mathlib

English

A compatibility result for the level-0 cycles with composition, relating cyclesMap with cyclesIso₀ and hom maps: (cyclesMap f φ 0) followed by (cyclesIso₀ B).hom equals φ.hom followed by (cyclesIso₀ A).hom.

Русский

Совместимость на уровне нулевых циклов: (cyclesMap f φ 0) затем (cyclesIso₀ B).hom равняется φ.hom затем (cyclesIso₀ A).hom.

LaTeX

$$$(\mathrm{cyclesMap} f φ 0) \; ; \; (\mathrm{cyclesIso}_0 B).hom = φ.hom \; ; \; (\mathrm{cyclesIso}_0 A).hom$$$

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 →₀ A` to `∑ φ(aᵢ)·f(gᵢ) : H →₀ B`. -/
noncomputable abbrev chainsMap₁ : ModuleCat.of k (G →₀ A) ⟶ ModuleCat.of k (H →₀ B) :=
  ModuleCat.ofHom <| mapRange.linearMap φ.hom.hom ∘ₗ lmapDomain A k f

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