rightDerivedToHomotopyCategory_comp

English

Naturality of inverses of the isomorphisms between right-derived objects with respect to f.

Русский

Естественность обратных изоморфизмов между правыми производными относительно отображения f.

LaTeX

$$$(I.isoRightDerivedObj F n).inv \\circ F.rightDerived n .map f = (F.mapHomologicalComplex _ \\circ ...).map φ \\circ (J.isoRightDerivedObj F n).inv$$$

Lean4

@[simp, reassoc]
theorem rightDerivedToHomotopyCategory_comp {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive]
    [H.Additive] :
    NatTrans.rightDerivedToHomotopyCategory (α ≫ β) =
      NatTrans.rightDerivedToHomotopyCategory α ≫ NatTrans.rightDerivedToHomotopyCategory β :=
  rfl

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