triangleRotateShortComplex — Mathlib

English

There is an isomorphism of triangles between the rotated triangle of a degreewise split short exact sequence and the triangle attached to the homomorphism of degreewise split.

Русский

Существует изоморфизм треугольников между повёрнутым треугольником степени-разделенной короткой точной последовательности и треугольником, присоединяемым к гомоморфизму degreewise split.

LaTeX

$$$(triangleRotateShortComplex φ).map (eval C (ComplexShape.up Int) n) \cong (triangleOfDegreewiseSplit φ).map (eval C (ComplexShape.up Int) n)$$$

Lean4

/-- Given a morphism of cochain complexes `φ`, this is the short complex
given by `(triangle φ).rotate`. -/
@[simps]
noncomputable def triangleRotateShortComplex : ShortComplex (CochainComplex C ℤ) :=
  ShortComplex.mk (triangle φ).rotate.mor₁ (triangle φ).rotate.mor₂ (by simp)

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