desc_commutes_zero — Mathlib

English

Let f: Z → Y be a morphism in an Abelian category with injective resolutions I of Y and J of Z. Then the 0-th component of the descent morphism desc f I J intertwines the vertex inclusions: Jι_0 ; (desc f I J)_0 = f ; Iι_0.

Русский

Пусть f: Z → Y — морфизм в абелевой категории, имеющей инъективные резолюции I(Y) и J(Z). Тогда нулевой компонент морфизма спуска desc f I J связывает вершины включений: Jι_0 ; (desc f I J)_0 = f ; Iι_0.

LaTeX

$$$J_{\iota}^{0} \circ (\mathrm{desc}\ f\ I\ J)^{0} = f \circ I_{\iota}^{0}$$$

Lean4

@[reassoc (attr := simp)]
theorem desc_commutes_zero {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) :
    J.ι.f 0 ≫ (desc f I J).f 0 = f ≫ I.ι.f 0 :=
  (HomologicalComplex.congr_hom (desc_commutes f I J) 0).trans
    (by simp)
      -- Now that we've checked this property of the descent, we can seal away the actual definition.

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