Torsion pairs on a heart, and the tilted aisles #
The Happel–Reiten–Smalø tilt: from a torsion pair on the heart of a t-structure, a second t-structure whose heart is the extension of the torsion class by the shifted torsion-free class.
The tilt is constructed here, as HeartTorsionPair.tilt, with every field
proved and nothing declared with sorry.
The one design decision worth explaining #
The tilted aisles are normally written with cohomology functors:
D^{≤0}_† = {X ∈ D^{≤0} : H⁰(X) ∈ T}, D^{≥0}_† = {X ∈ D^{≥-1} : H^{-1}(X) ∈ F}.
Mathlib has no Hⁿ for a t-structure at the pin — TStructure/ carries
truncLE, truncGE and the truncation triangle, but no cohomology functor
into the heart. This project now constructs that functor and proves it
homological in WeakStabilityCondition/Tilting/Cohomology/Homological.lean;
WeakStabilityCondition/StabilityCondition/Metric/Mass/Subadditivity/CohomologyExactness.lean
transports the result to the stability-condition API. The aisle construction
here predates that bridge and does not depend on it.
So the aisles here are defined by Hom-orthogonality instead, which needs no
cohomology functor at all. For X ∈ D^{≤0} and F in the heart the counit
gives Hom(X, F) ≅ Hom(H⁰X, F), and T is exactly the left orthogonal of F
in the heart, so
H⁰(X) ∈ T ⟺ Hom(X, F) = 0 for every F ∈ F.
The right-hand side is what tiltLE says. It is equivalent to the usual
definition wherever the usual definition can be stated, and it is available
here, where the usual one is not. That equivalence is not only prose: with
τ^{≥0} (resp. τ^{≤0}) in the role of H⁰, it is the theorems
tiltLE_iff_tors_truncGE and tiltGE_iff_free_truncLE at the end of this
file.
Status #
Established here: the datum, the aisles at every integer level with their
isomorphism-closure, both factorisation lemmas standing in for the two counit
isomorphisms, the orthogonality characterisations of both classes, the
agreement of both aisles with the textbook H⁰ formulation, and the
identification of the tilted heart with the extensions of T by F⟦1⟧.
All six non-trivial TStructure fields are proved, and tilt assembles them.
exists_triangle_zero_one — the last and hardest — is exists_tilt_triangle,
built from two octahedra and no cohomology functor.
tilt requires [IsTriangulated C]. That is not incidental: the octahedral
axiom is what makes τ^{≥0} preserve D^{≤0}, which is what puts H⁰ in the
heart, and it is also what supplies the two octahedra. It is carried
explicitly rather than assumed globally.
A torsion pair on the heart of t, phrased inside C rather than inside
the heart as a category.
Stating it in C avoids the full-subcategory plumbing that carrying an
Abelian instance on the heart would require, and the decomposition axiom
becomes a distinguished triangle — which for objects of the heart is the same
thing as a short exact sequence there. WeakStabilityCondition/Tilting/TorsionPair/Basic.lean is the
abelian-category version of the same notion; neither is derived from the other
here.
- tors : ObjectProperty C
the torsion class
- free : ObjectProperty C
the torsion-free class
- tors_isClosedUnderIsomorphisms : self.tors.IsClosedUnderIsomorphisms
- free_isClosedUnderIsomorphisms : self.free.IsClosedUnderIsomorphisms
no nonzero map from a torsion object to a torsion-free one
- exists_triangle (X : C) : t.IsLE X 0 → t.IsGE X 0 → ∃ (T : C) (F : C) (_ : self.tors T) (_ : self.free F) (f : T ⟶ X) (g : X ⟶ F) (h : F ⟶ (shiftFunctor C 1).obj T), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles
every object of the heart is an extension of a torsion-free object by a torsion one
Instances For
The tilted aisles #
Stated first at the level the tilt is defined at; tiltLEAt / tiltGEAt below
extend them to every integer, which is what a TStructure needs.
The tilted co-aisle D^{≤0}_†: objects of D^{≤0} with no nonzero map to
a torsion-free object. Under the counit isomorphism this says H⁰(X) ∈ T.
Instances For
The tilted aisle D^{≥1}_†: objects of D^{≥0} with no nonzero map from a
torsion object. Under the counit isomorphism this says H⁰(X) ∈ F.
Instances For
The factorisation lemmas #
Everything the Hom-vanishing axiom needs, and the substitute for the counit
isomorphism Hom(X, F) ≅ Hom(H⁰X, F) that a cohomology functor would supply.
The dual pair below it is the substitute for the other adjunction's
Hom(T, X) ≅ Hom(T, H⁰X), and is what the aisle-side textbook agreement
(freeOrth_iff_free_truncLE) runs on.
Every map into D^{≥0} factors through the truncation τ^{≥0}.
This is the half of the counit isomorphism the tilt actually uses. When
additionally X ∈ D^{≤0} the target τ^{≥0}X lies in the heart and plays the
role of H⁰(X), so this is what lets an orthogonality hypothesis on X be
transported to one on H⁰(X).
No hypothesis on X is needed: the truncation triangle exists for every
object, and Hom(τ^{<0}X, F) vanishes for degree reasons alone.
The factorisation is unique: τ^{≥0}X really does corepresent maps out of
X into D^{≥0}, not merely dominate them.
Every map from D^{≤0} factors through the truncation τ^{≤0}.
The dual of exists_factor_truncGE. When additionally X ∈ D^{≥0} the source
τ^{≤0}X lies in the heart and plays the role of H⁰(X), so this is what
lets an orthogonality hypothesis on X be transported to one on H⁰(X) from
the torsion side.
As with its dual, no hypothesis on X is needed: the truncation triangle
exists for every object, and Hom(A, τ^{≥1}X) vanishes for degree reasons
alone.
The factorisation is unique: τ^{≤0}X really does represent maps from
D^{≤0} into X, not merely dominate them. The inverse rotation replaces
the rotation of the dual proof, and no rotation sign is ever inspected.
Orthogonality characterisations #
Each class is the orthogonal of the other inside the heart. The forward
direction is the hom_eq_zero axiom; the converse is where the decomposition
axiom earns its place, and it needs no cohomology functor — only that a
distinguished triangle whose second map vanishes has a zero third object, which
here follows from a degree count.
An object of the heart with no nonzero map to a torsion-free object is torsion.
An object of the heart with no nonzero map from a torsion object is
torsion-free. The dual of tors_of_orthogonal: the inverse rotation replaces
the rotation, and no rotation sign is ever inspected.
The Hom-vanishing axiom #
zero' for the tilted t-structure, proved without any cohomology functor: the
factorisation lemma moves the orthogonality hypothesis from X onto
τ^{≥0}X, and tors_of_orthogonal then puts that truncation in the torsion
class, where the second aisle's hypothesis kills it.
No nonzero map from the tilted co-aisle to the tilted aisle.
The indexed families #
A Triangulated.TStructure needs an aisle at every integer, not just at the
level the tilt is defined. Splitting the orthogonality condition off as its own
isomorphism-closed predicate is what keeps the shift axioms to a single
application of shiftFunctorAdd' each.
Objects with no nonzero map to a torsion-free object.
Instances For
Objects with no nonzero map from a torsion object.
Instances For
The tilted co-aisle at level n: X ∈ D^{≤n}_† iff X⟦n⟧ ∈ D^{≤0}_†.
Instances For
The tilted aisle at level n: X ∈ D^{≥n}_† iff X⟦n-1⟧ ∈ D^{≥1}_†,
and tiltGE is the level-one member.
Equations
Instances For
Agreement with the level at which the tilt was defined #
The shift axioms #
Each is one application of shiftFunctorAdd' against the orthogonality
predicate's isomorphism-closure, plus the corresponding IsLE/IsGE shift.
The le_shift field for the tilted co-aisle.
The ge_shift field for the tilted aisle.
The two inclusions #
Both are pure degree counts: neither uses the orthogonality hypothesis it is
handed, because the shifted object is already separated from the heart by
t.zero.
The le_zero_le field.
The ge_one_le field.
The zero' field, transported to the indexed families.
Recognising the two aisles from a triangle #
These are the shapes the two halves of a tilted truncation take, and they are the reason the tilt does not need a cohomology functor after all.
The textbook construction of exists_triangle_zero_one says: cut H⁰(A) by
the torsion pair as 0 → T₀ → H⁰(A) → F₀ → 0, then take
X = extension of T₀ by τ^{≤-1}A, Y = extension of τ^{≥1}A by F₀.
Membership of X and Y in the two aisles is then usually read off a long
exact cohomology sequence. The two lemmas below get it instead from
isLE₂/isGE₂ plus a single factorisation through the triangle — no Hⁿ
anywhere.
A first attempt built X as the fibre of τ^{≤0}A → F₀ instead. That shape
does not work formally: IsLE X 0 then sits between 0 and
Hom(F₀⟦-1⟧, Z), which does not vanish for degree reasons, and recovering it
genuinely needs that H⁰(A) → F₀ is epi. The extension shape below avoids that
entirely, because both of its ends are already in D^{≤0}.
An extension of a torsion object by an object of D^{≤-1} lies in the
tilted co-aisle.
An extension of an object of D^{≥1} by a torsion-free object lies in
the tilted aisle.
The co-aisle recognition, in the indexed form a TStructure field wants.
The aisle recognition, in the indexed form a TStructure field wants.
The truncation triangle for the tilted aisles #
The last field. Two octahedra do all the work, and the choice of which octahedron is the whole trick:
Octahedron'works with fibres, and applied toB ⟶ H ⟶ F₀its three fibres areZ,X,T₀— deliveringZ ⟶ X ⟶ T₀with no desuspension. The cone-flavouredOctahedronwould give the same triangle shifted once, and unshifting it costs sign bookkeeping for nothing.Octahedronworks with cones, and applied toX ⟶ B ⟶ Aits three cones areF₀,Y,W— deliveringF₀ ⟶ Y ⟶ Wdirectly.
Both outputs are exactly what tiltLE_of_triangle and tiltGE_of_triangle
consume.
The tilted truncation triangle, from abstract triangle data.
Separated from the instantiation so that the octahedral content is visible on
its own: given the two t-structure truncation triangles and the torsion
decomposition of the heart object between them, this produces the tilted
truncation of A.
exists_triangle_zero_one for the tilted aisles.
Every object has a tilted truncation. With the five fields already proved
above, this completes the Happel–Reiten–Smalø tilt as a TStructure.
The tilt #
All six non-trivial fields are proved, so the tilted aisles assemble into an
honest Triangulated.TStructure.
The Happel–Reiten–Smalø tilt of t at the torsion pair P.
The aisles are tiltLEAt and tiltGEAt; every field is one of the theorems
above. No cohomology functor appears anywhere in the construction — see the
module docstring for why the usual one is unavailable here and what replaces
it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tilt of the degenerate torsion pair changes nothing at level zero on
the co-aisle side, in the sense that its membership is the original IsLE
condition together with a vacuous orthogonality clause. Recorded as a sanity
check on the indexing rather than as a result.
Agreement with the textbook aisles #
The module docstring claims the Hom-orthogonal aisles agree with the textbook
H⁰ formulation wherever the latter can be stated. At this pin the textbook
side is statable, with τ^{≥0} (resp. τ^{≤0}) in the role of H⁰ on
D^{≤0} (resp. D^{≥0}), and the four theorems below are that claim. Each
direction is the factorisation lemma on one side and the orthogonality
characterisation or the hom_eq_zero axiom on the other; [IsTriangulated C]
is what puts the truncation in the heart, exactly as in zero'.
The co-aisle orthogonality condition is the textbook H⁰ condition:
for X ∈ D^{≤0}, orthogonality to the torsion-free class is torsionness of
τ^{≥0}X.
The aisle orthogonality condition is the textbook H⁰ condition: for
X ∈ D^{≥0}, orthogonality to the torsion class is torsion-freeness of
τ^{≤0}X.
The tilted co-aisle is the textbook one: X ∈ D^{≤0}_† iff
X ∈ D^{≤0} and H⁰(X) ∈ T, with τ^{≥0}X in the role of H⁰(X).
The tilted aisle is the textbook one: X ∈ D^{≥1}_† iff X ∈ D^{≥0}
and H⁰(X) ∈ F, with τ^{≤0}X in the role of H⁰(X).
The tilted heart #
The textbook description A† = ⟨F⟦1⟧, T⟩. Because (T, F) is a torsion
pair the extension closure collapses to a single step, so the identification
is an iff: an object lies in the tilted heart exactly when it is an extension
of a torsion object by a shifted torsion-free one. No cohomology functor and
no truncation–shift commutation appears anywhere: the forward direction reads
both memberships off the truncation triangle of X and its ⟦-1⟧-shift, and
the backward direction is the two recognition lemmas, once directly and once
through the ⟦-1⟧-shift of the given triangle.
An extension of a torsion object by a shifted torsion-free object lies in the tilted heart.
Every object of the tilted heart is an extension of a torsion object by
a shifted torsion-free one — the truncation triangle of X, with τ^{≥0}X
torsion by torsOrth_iff_tors_truncGE and (τ^{<0}X)⟦-1⟧ torsion-free by
free_of_orthogonal and one coyoneda factorisation.
The tilted heart is the textbook one: extensions of T by F⟦1⟧.
The single-step form is exact because (T, F) is a torsion pair, so this is
the identification A† = ⟨F⟦1⟧, T⟩ with no extension-closure operator
needed.
What is proved, and what is not #
Every field of Triangulated.TStructure is proved, and tilt is the
resulting t-structure:
| field | theorem |
|---|---|
le_isClosedUnderIsomorphisms / ge_… | tiltLEAt_isClosedUnderIsomorphisms / tiltGEAt_… |
le_shift / ge_shift | tiltLEAt_shift / tiltGEAt_shift |
le_zero_le / ge_one_le | tiltLEAt_zero_le / tiltGEAt_one_le |
zero' | tiltAt_zero', on hom_eq_zero_of_tiltLE_of_tiltGE |
exists_triangle_zero_one | exists_tilt_triangle |
Neither inclusion uses the orthogonality hypothesis it is handed — both are
pure degree counts against t.zero.
What is still not here #
free_of_orthogonal is no longer on this list: the independent review of the
tilt (#86, finding F1) observed that the textbook-agreement claim above was
prose-only on the aisle side, and the dual pair — exists_factor_truncLE /
factor_truncLE_unique and free_of_orthogonal — now exists, together with
the four agreement theorems. Its inverse-rotation bookkeeping turned out to
cost nothing: coyoneda_exact₂ on the inverse rotation never inspects a
rotated map, so no sign appears.
- Any connection to a stability condition.
tiltis a t-structure on a triangulated category. That the tilted heart is the heart of a stability condition, or that tilting is how stability conditions on surfaces are built, is motivation for this file and is not formalised in it.
The identification of the tilted heart, formerly on this list, is
tilt_heart_iff (#106): the heart is exactly the extensions of T by
F⟦1⟧, the single-step form of the extension closure ⟨F⟦1⟧, T⟩, exact
here because (T, F) is a torsion pair.
The correction that made this possible #
Kept because the wrong turn is what a reader would otherwise repeat. Earlier
revisions of this file asserted that exists_triangle_zero_one needs the long
exact cohomology sequence of H⁰, and treated it as blocked on machinery
Mathlib does not have.
That was inferred from the textbook construction, which cuts X as the
fibre of τ^{≤0}A ⟶ F₀. That shape genuinely does need cohomology:
IsLE X 0 then depends on H⁰(A) ⟶ F₀ being epi, and formally Hom(X, Z)
only injects into Hom(F₀⟦-1⟧, Z), which does not vanish for degree reasons.
The shape used here builds X as an extension of T₀ by τ^{≤-1}A, whose
two ends are already in D^{≤0}, so isLE₂ closes the degree half and one
factorisation closes the orthogonality half. The obstruction was in the chosen
construction, not in the theorem.
The same substitution runs throughout: τ^{≥0}X plays the role of H⁰(X),
exists_factor_truncGE plays the role of the counit isomorphism, and
Hom-orthogonality plays the role of membership in T. None of the three needs
a cohomology functor to exist.