hom_comp_singleFunctor_map_shift — Mathlib

English

Given x ∈ Ext X Y n and a morphism f: Y → Z, the composition with the shifted singleFunctor map equals the hom-composition with mk0 f in Ext.

Русский

Для x ∈ Ext^n(X,Y) и гомоморфизма f: Y → Z, композиция с отображением в сдвинутом единичном функторе эквивалентна hом-композиции с mk0 f в Ext.

LaTeX

$$$x.hom \; \cdot \big(\text{singleFunctor map } f\big) = \big( x \cdot (mk_0 f) \big).hom$$$

Lean4

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

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