cochainsMap₁ — Mathlib

English

There is an equality showing that the cochains map is equal to the homology map derived from cochains in a canonical way, i.e., cocycles map equals homology map on the corresponding chain complexes.

Русский

Существуют эквивалентности: отображение коцепонов эквивалентно отображению на гомологию, получаемому из коцепонов на соответствующих комплексах.

LaTeX

$$$\\\\map f φ n = \\\\mathrm{HomologicalComplex.homologyMap}\\\\left(\\\\mathrm{cochainsMap} f φ\\\\right) n$$$

Lean4

/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map sending `x : H → A` to `(g : G) ↦ φ (x (f g))`. -/
noncomputable abbrev cochainsMap₁ : ModuleCat.of k (H → A) ⟶ ModuleCat.of k (G → B) :=
  ModuleCat.ofHom <| φ.hom.hom.compLeft G ∘ₗ LinearMap.funLeft k A f

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