mk₀_comp_mk₀ — Mathlib

English

In the abelian setting with derived category, the composition of mk₀ f with mk₀ g equals mk₀ (f ≫ g); this is the basic compatibility of mk₀ with composition.

Русский

В абелевой категории с производной категорией композиция mk₀ f и mk₀ g равна mk₀ (f ≫ g); это базовая совместимость mk₀ с композициями.

LaTeX

$$$ (mk_0 f).\\mathrm{comp} (mk_0 g) = mk_0 (f \\circ g) $$$

Lean4

@[simp]
theorem mk₀_comp_mk₀ (f : X ⟶ Y) (g : Y ⟶ Z) : (mk₀ f).comp (mk₀ g) (zero_add 0) = mk₀ (f ≫ g) := by
  letI := HasDerivedCategory.standard C; ext; simp

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