singleFunctor_map_comp_hom — Mathlib

English

Compatibility of the single functor map with composition: the map of f followed by x equals the composition of mk0 f with x, in hom form.

Русский

Совместимость отображения единственного функторы с композициями: отображение f затем x равно композиции mk0 f с x (в виде гомоморфизма).

LaTeX

$$$(\\mathrm{DerivedCategory.singleFunctor}\\, C\\,0).\\mathrm{map} f \\; \\gg x.hom = \\big((\\mathrm{mk}_0 f).\\mathrm{comp} x (\\mathrm{zero\_add} n)\\big).\\mathrm{hom}$$$

Lean4

theorem singleFunctor_map_comp_hom [HasDerivedCategory.{w'} C] {X Y Z : C} (f : X ⟶ Y) {n : ℕ} (x : Ext Y Z n) :
    (DerivedCategory.singleFunctor C 0).map f ≫ x.hom = ((mk₀ f).comp x (zero_add n)).hom := by
  simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp]

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