desc_commutes — Mathlib

English

The descent morphism commutes with the inclusion maps of the injective resolutions: J.ι ≫ desc f I J = map f ≫ I.ι.

Русский

Проводя спуск, диаграмма удовлетворяет commuting: J.ι ∘ desc f I J = map f ∘ I.ι.

LaTeX

$$$J.\iota \\circ \\text{desc}(f,I,J) = (\\text{map} f) \\circ I.\\iota$$$

Lean4

/-- The resolution maps intertwine the descent of a morphism and that morphism. -/
@[reassoc (attr := simp)]
theorem desc_commutes {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) :
    J.ι ≫ desc f I J = (CochainComplex.single₀ C).map f ≫ I.ι :=
  by
  ext
  simp [desc, descFOne, descFZero]

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