ofCocomplex — Mathlib

English

Two descents of a composition f ≫ g are homotopic: desc (f ≫ g) K I is homotopic to desc f J I followed by desc g K J.

Русский

Два спуска композиции f ∘ g гомотопны: spуск desc (f ∘ g) K I гомотопичен к desc f J I затем desc g K J.

LaTeX

$$desc (f ≫ g) K I \; \sim_{hom} \; (desc f J I) ≫ (desc g K J)$$

Lean4

/-- Auxiliary definition for `InjectiveResolution.of`. -/
def ofCocomplex : CochainComplex C ℕ :=
  CochainComplex.mk' (Injective.under Z) (Injective.syzygies (Injective.ι Z)) (Injective.d (Injective.ι Z)) fun f =>
    ⟨_, Injective.d f, by simp⟩

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