singleFunctorIsoCompQ — Mathlib

English

There is a canonical isomorphism between the functor singleFunctor C n and the composition CochainComplex.singleFunctor C n after applying Q.

Русский

Существует каноническое изоморфизм между выражениями singleFunctor C n и (CochainComplex.singleFunctor C n) ∘ Q.

LaTeX

$$$singleFunctor\ C\ n\;\cong\ (CochainComplex.singleFunctor\ C\ n)\;\circ\ Q$$$

Lean4

/-- The isomorphism `singleFunctor C n ≅ CochainComplex.singleFunctor C n ⋙ Q`. -/
noncomputable def singleFunctorIsoCompQ (n : ℤ) : singleFunctor C n ≅ CochainComplex.singleFunctor C n ⋙ Q :=
  Iso.refl _

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