English
If K is both GE and LE at n, then K is isomorphic to a stalk complex concentrated in degree n.
Русский
Если K имеет GE и LE в одном уровне n, то K изоморфен стержневому комплексу, концентрационному в степени n.
LaTeX
$$$ [K.IsGE(n)] \\land [K.IsLE(n)] \\Rightarrow \\exists M:\\mathcal{C},\, K \\cong (\\text{single}\\, C(\\text{ComplexShape.up } \\mathbb{Z})\\, n).\\mathrm{obj}M $$$
Lean4
/-- A cochain complex that is both strictly `≤ n` and `≥ n` is isomorphic to
a complex `(single _ _ n).obj M` for some object `M`. -/
theorem exists_iso_single (n : ℤ) [K.IsStrictlyGE n] [K.IsStrictlyLE n] :
∃ (M : C), Nonempty (K ≅ (single _ _ n).obj M) :=
⟨K.X n,
⟨{ hom := mkHomToSingle (𝟙 _) (fun i (hi : i + 1 = n) ↦ (K.isZero_of_isStrictlyGE n i (by cutsat)).eq_of_src _ _)
inv := mkHomFromSingle (𝟙 _) (fun i (hi : n + 1 = i) ↦ (K.isZero_of_isStrictlyLE n i (by cutsat)).eq_of_tgt _ _)
hom_inv_id := by
ext i
obtain hi | rfl | hi := lt_trichotomy i n
· apply (K.isZero_of_isStrictlyGE n i (by cutsat)).eq_of_src
· simp
· apply (K.isZero_of_isStrictlyLE n i (by cutsat)).eq_of_tgt
inv_hom_id := by aesop }⟩⟩
