mapHomotopyCategory_map — Mathlib

English

For any F: V ⥤ W, the map through the quotient and the map through F commute, i.e., the functorial image of a morphism is the same whether we first quotients then map, or map then quotient.

Русский

Для любого F: V ⥤ W отображение через квоту и отображение через F коммутируют: образ функторного изображения морфизма совпадает при любом порядке действий.

LaTeX

$$$ (F.mapHomotopyCategory c).map ((\text{quotient } V c).map f) = (\text{quotient } W c).map ((F.mapHomologicalComplex c).map f) $$$

Lean4

@[simp]
theorem mapHomotopyCategory_map (F : V ⥤ W) [F.Additive] {c : ComplexShape ι} {K L : HomologicalComplex V c}
    (f : K ⟶ L) :
    (F.mapHomotopyCategory c).map ((HomotopyCategory.quotient V c).map f) =
      (HomotopyCategory.quotient W c).map ((F.mapHomologicalComplex c).map f) :=
  rfl

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