scIso
plain-language theorem explainer
Canonical isomorphism identifying the short complex at degree n+1 with the honest three-term complex X_{n+2} → X_{n+1} → X_n. Homology constructions in ArcComplementAcyclic cite it to move between mathlib's sc and sc' presentations when forming classes of cycles. The body is a direct call to isoSc' with the predecessor and successor index witnesses.
Claim. For each natural number $n$ and chain complex $K$, there is a canonical isomorphism of short complexes $K.\mathrm{sc}(n+1)\cong K.\mathrm{sc}'(n+2,n+1,n)$, identifying the short complex at degree $n+1$ with the three-term complex $K_{n+2}\to K_{n+1}\to K_n$.
background
In mathlib, a homological complex $K$ over the down-shape on $\mathbb{N}$ carries two presentations of the three-term data at a degree. The bundled short complex $K.\mathrm{sc}(m)$ packages differentials around degree $m$, while $K.\mathrm{sc}'(i,j,k)$ is the honest-index short complex $K_i\to K_j\to K_k$ for specified consecutive indices.
The module ArcComplementAcyclic builds concrete homology classes for such complexes (over $\mathrm{ModuleCat},\mathbb{Z}$) in service of vanishing statements for arc complements. Downstream definitions need a fixed bridge from the abstract short-complex API to the three consecutive chain groups $X(n+2),X(n+1),X(n)$ so that cycles can be quotiented by boundaries in the usual way.
The doc-comment states the content directly: the map is the canonical isomorphism from $K.\mathrm{sc}(n+1)$ to the honest-index short complex $K.X(n+2)\to K.X(n+1)\to K.X(n)$.
proof idea
One-line definitional wrapper. It applies $K.\mathrm{isoSc}'$ at indices $(n+2,n+1,n)$, supplying the two shape witnesses $\mathrm{ChainComplex.prev},\mathbb{N},(n+1)$ and $\mathrm{ChainComplex.next_nat_succ},n$ that certify the consecutive down-shape relations. No further rewriting is needed; the isomorphism is the library's standard sc/sc' comparison at those indices.
why it matters
This iso is the transport used by every concrete homology constructor in the module. The definition classOf builds the homology class of a cycle by pushing a quotient class along homologyMap of (scIso).inv (and the moduleCat left-homology iso). The vanishing criterion classOf_eq_zero_iff, the representability lemma exists_classOf, and the naturality lemma classOf_natural all thread through the same iso.
In the Recognition foundation layer, those lemmas underwrite acyclicity arguments for arc complements: a cycle is null-homologous precisely when it is a boundary, and classes push along chain maps. The declaration itself is pure homological bookkeeping, not a physics claim, but it is the interface that lets the ArcComplementAcyclic vanishing results speak in mathlib's homology language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.