forget_map — Mathlib

English

The forgetful functor from the total bicomplex preserves the graded-map structure on the total level.

Русский

Функтор забывания из суммарного би-комплекса сохраняет структуру отображения по градам на уровне суммарного объекта.

LaTeX

$$$$ (\\text{forget } C c_{12}).map (map \\varphi c_{12}) = \\mathrm{GradedObject}.mapMap (toGradedObjectMap \\varphi) _ $$$$

Lean4

@[simp]
theorem forget_map : (HomologicalComplex.forget C c₁₂).map (map φ c₁₂) = GradedObject.mapMap (toGradedObjectMap φ) _ :=
  rfl

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