triangleOfSES_distinguished — Mathlib

English

The triangle attached to a short exact sequence SES is a distinguished triangle in the derived category.

Русский

Треугольник, связанный с SES, является выделенным треугольником в производной категории.

LaTeX

$$$$ \triangleOfSES(hS) \in \text{distinguished triangles} \mathrm{DerivedCategory}(C) $$$$

Lean4

theorem triangleOfSES_distinguished : triangleOfSES hS ∈ distTriang (DerivedCategory C) :=
  by
  rw [mem_distTriang_iff]
  exact ⟨_, _, S.f, ⟨triangleOfSESIso hS⟩⟩

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