plusFunctor_preservesZeroMorphisms

English

A variant of the previous statement with simplification rules; the equality of two expressions given by plusMap and plusLift holds under simp rules, reinforcing the naturality of the construction.

Русский

Вариант предыдущего утверждения с упрощениями; равенство выражений, задаваемых plusMap и plusLift, сохраняется под правилaми упрощения, показывая естественность конструкции.

LaTeX

$$$ J.plusMap η ≫ J.plusLift γ h_R = J.plusLift (η ≫ γ) h_R $$$

Lean4

instance plusFunctor_preservesZeroMorphisms [Preadditive D] : (plusFunctor J D).PreservesZeroMorphisms where
  map_zero F
    G := by
    ext
    dsimp
    rw [J.plusMap_zero, NatTrans.app_zero]

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