map_comp — Mathlib

English

Map of a composition equals the composition of maps on total complex level.

Русский

Отображение композиции равно композиции отображений на уровне полного комплекса.

LaTeX

$$$\\mathrm{map}(\\varphi \\circ \\psi) c_{12} = \\mathrm{map}\\; \\varphi c_{12} \\circ \\mathrm{map}\\; \\psi c_{12}$$$

Lean4

@[simp, reassoc]
theorem map_comp : map (φ ≫ ψ) c₁₂ = map φ c₁₂ ≫ map ψ c₁₂ :=
  by
  apply (HomologicalComplex.forget _ _).map_injective
  exact GradedObject.mapMap_comp (toGradedObjectMap φ) (toGradedObjectMap ψ) _

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