Bounded t-structures and t-exact functors #
Both 2026 target papers state their central hypotheses in this vocabulary.
Polishchuk's inducing theorem (arXiv:2601.22994 Prop 3.4, arXiv:2607.28411
Thm A.17) asks for a bounded t-structure and for Φ Φᴸ to be right t-exact;
without those as definitions the hypothesis cannot be written down at all.
Main definitions #
TStructure.IsBounded: every object ist-bounded.TStructure.IsNondegenerate: no nonzero object ist-coconnective in every degree, nort-connective in every degree.Functor.IsRightTExact/Functor.IsLeftTExact/Functor.IsTExact: a functor's compatibility with a t-structure on its source and one on its target.
Main results #
Functor.isRightTExact_of_isLE_zero/Functor.isLeftTExact_of_isGE_zero: for a shift-commuting functor, degree0suffices.Functor.isTExact_of: assembleIsTExactfrom its two halves.Functor.isLeftTExact_rightAdjoint/Functor.isRightTExact_leftAdjoint: right t-exactness of a left adjoint and left t-exactness of its right adjoint determine each other.Functor.isRightTExact_comp/isLeftTExact_comp/isTExact_comp, and the identity functor.
Namespacing #
The t-structure notions live in CategoryTheory.Triangulated.TStructure, and
the functorial notions in CategoryTheory.Functor, matching their mathematical
owners. The slicing construction connects this interface to the canonical
t-structure through repository-owned bridge theorems.
Conventions #
Mathlib writes the t-structure as t.IsLE X n (X ∈ Dᵗ≤ⁿ) and t.IsGE X n
(X ∈ Dᵗ≥ⁿ), and already supplies t.plus, t.minus and t.bounded as
ObjectProperty C. Boundedness of the t-structure itself is then just
t.bounded = ⊤, which is the definition taken here.
Right t-exactness preserves the coconnective half (IsLE), left t-exactness
the connective half (IsGE). This is the convention under which the derived
functor Lf* is right t-exact and Rf_* is left t-exact, and it is the one
both papers use.
A correction to the issue that requested this file #
Issue #146 asked for "the nondegenerate ⟺ bounded equivalence". Only one
direction is a theorem: bounded implies nondegenerate (isNondegenerate_of_isBounded).
The converse is false. A nondegenerate t-structure can have objects that are
bounded in neither direction — nondegeneracy only forbids an object from being
coconnective in every degree, which says nothing about an object that is
coconnective in no degree at all. The unbounded derived category of a nonzero
abelian category with its standard t-structure is nondegenerate and not bounded.
So the equivalence is not stated here, and #146's acceptance criterion should be
read as the implication.
def
CategoryTheory.Triangulated.TStructure.IsBounded
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(t : TStructure C)
:
A t-structure is bounded when every object of the ambient category is
t-bounded, i.e. lies in Dᵗ≤ⁿ for some n and in Dᵗ≥ᵐ for some m.
Instances For
theorem
CategoryTheory.Triangulated.TStructure.isBounded_iff
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{t : TStructure C}
:
theorem
CategoryTheory.Triangulated.TStructure.exists_isLE
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{t : TStructure C}
(h : t.IsBounded)
(X : C)
:
On a bounded t-structure every object admits a coconnective bound.
theorem
CategoryTheory.Triangulated.TStructure.exists_isGE
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{t : TStructure C}
(h : t.IsBounded)
(X : C)
:
On a bounded t-structure every object admits a connective bound.
structure
CategoryTheory.Triangulated.TStructure.IsNondegenerate
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(t : TStructure C)
:
A t-structure is nondegenerate when the only object lying in Dᵗ≤ⁿ for
every n is zero, and likewise for Dᵗ≥ⁿ.
- isZero_of_forall_isLE (X : C) : (∀ (n : ℤ), t.IsLE X n) → Limits.IsZero X
An object coconnective in every degree is zero.
- isZero_of_forall_isGE (X : C) : (∀ (n : ℤ), t.IsGE X n) → Limits.IsZero X
An object connective in every degree is zero.
Instances For
theorem
CategoryTheory.Triangulated.TStructure.isNondegenerate_of_isBounded
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{t : TStructure C}
(h : t.IsBounded)
:
Bounded implies nondegenerate.
If X is coconnective in every degree then it is in particular coconnective in
degree n - 1 for the n supplied by boundedness on the connective side, so
X lies in Dᵗ≥ⁿ ∩ Dᵗ≤ⁿ⁻¹, which is zero.
The converse is false; see the module docstring.
class
CategoryTheory.Functor.IsRightTExact
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
:
F is right t-exact for t on the source and t' on the target when it
carries Dᵗ≤ⁿ into D'ᵗ'≤ⁿ for every n.
Right t-exactness preserves the coconnective half.
Instances
class
CategoryTheory.Functor.IsLeftTExact
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
:
F is left t-exact for t on the source and t' on the target when it
carries Dᵗ≥ⁿ into D'ᵗ'≥ⁿ for every n.
Left t-exactness preserves the connective half.
Instances
class
CategoryTheory.Functor.IsTExact
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
extends F.IsRightTExact t t', F.IsLeftTExact t t' :
F is t-exact when it is both left and right t-exact.
Instances
theorem
CategoryTheory.Functor.isLE_map_of_isRightTExact
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{t' : Triangulated.TStructure D}
[F.IsRightTExact t t']
(X : C)
(n : ℤ)
[t.IsLE X n]
:
theorem
CategoryTheory.Functor.isGE_map_of_isLeftTExact
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{t' : Triangulated.TStructure D}
[F.IsLeftTExact t t']
(X : C)
(n : ℤ)
[t.IsGE X n]
:
theorem
CategoryTheory.Functor.isTExact_of
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{t' : Triangulated.TStructure D}
[F.IsRightTExact t t']
[F.IsLeftTExact t t']
:
F.IsTExact t t'
Both halves assemble into IsTExact.
This is not an instance: IsTExact's parents are already instances by
projection, so registering the converse would let instance search cycle between
them. IsTExact.mk has no explicit fields, so neither ⟨_, _⟩ nor
inferInstance reaches this — the lemma is the intended route.
theorem
CategoryTheory.Functor.isRightTExact_of_isLE_zero
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{t' : Triangulated.TStructure D}
[F.CommShift ℤ]
(h : ∀ (X : C), t.IsLE X 0 → t'.IsLE (F.obj X) 0)
:
F.IsRightTExact t t'
For a shift-commuting functor, right t-exactness at degree 0 gives it at
every degree.
The class is quantified over all n because a bare functor need not commute
with the shift, and then the degrees are genuinely independent. Every functor
one applies this to in practice does commute with the shift, so this is the
constructor to reach for.
theorem
CategoryTheory.Functor.isLeftTExact_of_isGE_zero
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{t' : Triangulated.TStructure D}
[F.CommShift ℤ]
(h : ∀ (X : C), t.IsGE X 0 → t'.IsGE (F.obj X) 0)
:
F.IsLeftTExact t t'
For a shift-commuting functor, left t-exactness at degree 0 gives it at
every degree.
theorem
CategoryTheory.Functor.isLeftTExact_rightAdjoint
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{t' : Triangulated.TStructure D}
{G : Functor D C}
[G.Additive]
(adj : F ⊣ G)
[F.IsRightTExact t t']
:
G.IsLeftTExact t' t
The right adjoint of a right t-exact functor is left t-exact.
This is the closure lemma the inducing theorem actually consumes: its hypothesis
is right t-exactness of Φ Φᴸ, and what one has in hand is an adjunction.
The proof is the orthogonality characterization of Dᵗ≥ⁿ: a map A ⟶ G Y with
A in Dᵗ≤ⁿ⁻¹ transposes to F A ⟶ Y with F A in D'ᵗ'≤ⁿ⁻¹ and Y in
D'ᵗ'≥ⁿ, hence zero.
theorem
CategoryTheory.Functor.isRightTExact_leftAdjoint
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{t' : Triangulated.TStructure D}
{G : Functor D C}
[F.Additive]
(adj : F ⊣ G)
[G.IsLeftTExact t' t]
:
F.IsRightTExact t t'
The left adjoint of a left t-exact functor is right t-exact.
Dual to isLeftTExact_rightAdjoint, through the orthogonality characterization
of Dᵗ≤ⁿ.
noncomputable def
CategoryTheory.Functor.mapTriangleLEGEIso
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
(X : C)
:
F.mapTriangle.obj ((t.triangleLEGE n (n + 1) ⋯).obj X) ≅ (t'.triangleLEGE n (n + 1) ⋯).obj (F.obj X)
The triangle isomorphism comparing a t-exact functor applied to the canonical truncation triangle with the target truncation triangle.
Equations
- F.mapTriangleLEGEIso t t' n X = ⋯.choose
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapTriangleLEGEIso_hom₂
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
(X : C)
:
(F.mapTriangleLEGEIso t t' n X).hom.hom₂ = (Iso.refl (F.mapTriangle.obj ((t.triangleLEGE n (n + 1) ⋯).obj X)).obj₂).hom
The middle component of the truncation-triangle comparison is the identity on the mapped object.
noncomputable def
CategoryTheory.Functor.mapTruncLEIso
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
(X : C)
:
The coconnective truncation comparison of a t-exact functor.
Equations
- F.mapTruncLEIso t t' n X = CategoryTheory.Pretriangulated.Triangle.π₁.mapIso (F.mapTriangleLEGEIso t t' n X)
Instances For
theorem
CategoryTheory.Functor.mapTruncLEIso_hom_comp_ι
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
(X : C)
:
CategoryStruct.comp (F.mapTruncLEIso t t' n X).hom ((t'.truncLEι n).app (F.obj X)) = F.map ((t.truncLEι n).app X)
theorem
CategoryTheory.Functor.mapTruncLEIso_hom_comp_ι_assoc
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (F.mapTruncLEIso t t' n X).hom (CategoryStruct.comp ((t'.truncLEι n).app (F.obj X)) h) = CategoryStruct.comp (F.map ((t.truncLEι n).app X)) h
theorem
CategoryTheory.Functor.mapTruncLEIso_hom_naturality
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
{X Y : C}
(f : X ⟶ Y)
:
CategoryStruct.comp (F.map ((t.truncLE n).map f)) (F.mapTruncLEIso t t' n Y).hom = CategoryStruct.comp (F.mapTruncLEIso t t' n X).hom ((t'.truncLE n).map (F.map f))
The coconnective truncation comparison is natural in the object.
theorem
CategoryTheory.Functor.mapTruncLEIso_hom_naturality_assoc
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
{X Y : C}
(f : X ⟶ Y)
{Z : D}
(h : (t'.truncLE n).obj (F.obj Y) ⟶ Z)
:
CategoryStruct.comp (F.map ((t.truncLE n).map f)) (CategoryStruct.comp (F.mapTruncLEIso t t' n Y).hom h) = CategoryStruct.comp (F.mapTruncLEIso t t' n X).hom (CategoryStruct.comp ((t'.truncLE n).map (F.map f)) h)
The coconnective truncation comparison is natural in the object.
noncomputable def
CategoryTheory.Functor.mapTruncGEIso
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
(X : C)
:
The connective truncation comparison of a t-exact functor.
Equations
- F.mapTruncGEIso t t' n X = ⋯.mp (CategoryTheory.Pretriangulated.Triangle.π₃.mapIso (F.mapTriangleLEGEIso t t' (n - 1) X))
Instances For
theorem
CategoryTheory.Functor.mapTruncGEIso_π_comp_hom
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
(X : C)
:
CategoryStruct.comp (F.map ((t.truncGEπ n).app X)) (F.mapTruncGEIso t t' n X).hom = (t'.truncGEπ n).app (F.obj X)
theorem
CategoryTheory.Functor.mapTruncGEIso_π_comp_hom_assoc
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
(X : C)
{Z : D}
(h : (t'.truncGE n).obj (F.obj X) ⟶ Z)
:
CategoryStruct.comp (F.map ((t.truncGEπ n).app X)) (CategoryStruct.comp (F.mapTruncGEIso t t' n X).hom h) = CategoryStruct.comp ((t'.truncGEπ n).app (F.obj X)) h
theorem
CategoryTheory.Functor.mapTruncGEIso_hom_naturality
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
{X Y : C}
(f : X ⟶ Y)
:
CategoryStruct.comp (F.map ((t.truncGE n).map f)) (F.mapTruncGEIso t t' n Y).hom = CategoryStruct.comp (F.mapTruncGEIso t t' n X).hom ((t'.truncGE n).map (F.map f))
The connective truncation comparison is natural in the object.
theorem
CategoryTheory.Functor.mapTruncGEIso_hom_naturality_assoc
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(n : ℤ)
{X Y : C}
(f : X ⟶ Y)
{Z : D}
(h : (t'.truncGE n).obj (F.obj Y) ⟶ Z)
:
CategoryStruct.comp (F.map ((t.truncGE n).map f)) (CategoryStruct.comp (F.mapTruncGEIso t t' n Y).hom h) = CategoryStruct.comp (F.mapTruncGEIso t t' n X).hom (CategoryStruct.comp ((t'.truncGE n).map (F.map f)) h)
The connective truncation comparison is natural in the object.
theorem
CategoryTheory.Functor.isLE_iff_of_reflectsZeroObjects
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(hzero : ∀ (E : C), Limits.IsZero (F.obj E) → Limits.IsZero E)
(X : C)
(n : ℤ)
:
A t-exact functor which reflects zero objects also reflects the coconnective half of a t-structure. This is formula (A.3)'s reverse inclusion in the abstract large-category setting.
theorem
CategoryTheory.Functor.isGE_iff_of_reflectsZeroObjects
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(hzero : ∀ (E : C), Limits.IsZero (F.obj E) → Limits.IsZero E)
(X : C)
(n : ℤ)
:
A t-exact functor which reflects zero objects also reflects the connective half of a t-structure. This is formula (A.4)'s reverse inclusion in the abstract large-category setting.
theorem
CategoryTheory.Functor.isBounded_of_target
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
(F : Functor C D)
(t : Triangulated.TStructure C)
(t' : Triangulated.TStructure D)
[F.CommShift ℤ]
[F.IsTriangulated]
[F.IsTExact t t']
(hzero : ∀ (E : C), Limits.IsZero (F.obj E) → Limits.IsZero E)
(hbounded : t'.IsBounded)
:
Boundedness descends along a t-exact zero-reflecting functor. This is the categorical boundedness argument in Step 4 of A.17.
theorem
CategoryTheory.Functor.heart_map_of_isTExact
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{t' : Triangulated.TStructure D}
[F.IsTExact t t']
(X : C)
(hX : t.heart X)
:
A t-exact functor carries the heart into the heart.
theorem
CategoryTheory.Functor.isRightTExact_comp
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{E : Type u_1}
[Category.{u_2, u_1} E]
[Preadditive E]
[Limits.HasZeroObject E]
[HasShift E ℤ]
[∀ (n : ℤ), (shiftFunctor E n).Additive]
[Pretriangulated E]
{G : Functor D E}
{t'' : Triangulated.TStructure E}
(t' : Triangulated.TStructure D)
[F.IsRightTExact t t']
[G.IsRightTExact t' t'']
:
(F.comp G).IsRightTExact t t''
theorem
CategoryTheory.Functor.isLeftTExact_comp
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{E : Type u_1}
[Category.{u_2, u_1} E]
[Preadditive E]
[Limits.HasZeroObject E]
[HasShift E ℤ]
[∀ (n : ℤ), (shiftFunctor E n).Additive]
[Pretriangulated E]
{G : Functor D E}
{t'' : Triangulated.TStructure E}
(t' : Triangulated.TStructure D)
[F.IsLeftTExact t t']
[G.IsLeftTExact t' t'']
:
(F.comp G).IsLeftTExact t t''
theorem
CategoryTheory.Functor.isTExact_comp
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
[Limits.HasZeroObject D]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated D]
{F : Functor C D}
{t : Triangulated.TStructure C}
{E : Type u_1}
[Category.{u_2, u_1} E]
[Preadditive E]
[Limits.HasZeroObject E]
[HasShift E ℤ]
[∀ (n : ℤ), (shiftFunctor E n).Additive]
[Pretriangulated E]
{G : Functor D E}
{t'' : Triangulated.TStructure E}
(t' : Triangulated.TStructure D)
[F.IsTExact t t']
[G.IsTExact t' t'']
:
instance
CategoryTheory.Functor.isRightTExact_id
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{t : Triangulated.TStructure C}
:
(Functor.id C).IsRightTExact t t
instance
CategoryTheory.Functor.isLeftTExact_id
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{t : Triangulated.TStructure C}
:
(Functor.id C).IsLeftTExact t t
instance
CategoryTheory.Functor.isTExact_id
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{t : Triangulated.TStructure C}
:
(Functor.id C).IsTExact t t