singleFunctorPostcompQuotientIso — Mathlib

English

The isomorphism in the quotient construction aligns with the n-th single functor.

Русский

Сомкнутый изоморфизм в конструкциях через факторизацию согласуется с n-м единичным функтором.

LaTeX

$$$\text{singleFunctorsPostcompQuotientIso }(n) :\; singleFunctor C n \cong CochainComplex.singleFunctor C n \circ quotient _ _ $$$

Lean4

/-- `HomotopyCategory.singleFunctor C n` is induced by `CochainComplex.singleFunctor C n`. -/
noncomputable def singleFunctorPostcompQuotientIso (n : ℤ) :
    singleFunctor C n ≅ CochainComplex.singleFunctor C n ⋙ quotient _ _ :=
  (SingleFunctors.evaluation _ _ n).mapIso (singleFunctorsPostcompQuotientIso C)

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