cochainsMap_id — Mathlib

English

The first component of the cochains map is given by the natural action on i-th level, respecting composition of differential maps.

Русский

Первая компонента отображения cochainsMap задаётся естественным действием на i-м уровне, сохраняющим композицию дифференциалов.

LaTeX

$$$$ (cochainsMap f \\phi).f i : C^i(A) \\to C^i(B) \\quad \\text{linear in } i. $$$$

Lean4

@[simp]
theorem cochainsMap_id : cochainsMap (MonoidHom.id _) (𝟙 A) = 𝟙 (inhomogeneousCochains A) := by rfl

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