desc — Mathlib

English

A morphism f descends to a morphism of injective resolutions between J and I.

Русский

Пусть f спускается к отображению между разрешениями инъективных резолюций J и I.

LaTeX

$$$\text{desc}(f,I,J) : J.cocomplex \to I.cocomplex$$$

Lean4

/-- A morphism in `C` descends to a chain map between injective resolutions. -/
def desc {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y) (J : InjectiveResolution Z) : J.cocomplex ⟶ I.cocomplex :=
  CochainComplex.mkHom _ _ (descFZero f _ _) (descFOne f _ _) (descFOne_zero_comm f I J).symm fun n ⟨g, g', w⟩ =>
    ⟨(descFSucc I J n g g' w.symm).1, (descFSucc I J n g g' w.symm).2.symm⟩

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