A t-structure is determined by its aisle, and restrictions along a functor

Section 4 of arXiv:1902.08184 calls a t-structure τ on 𝒟 S-local when for every quasi-compact open U ⊆ S there is a t-structure τ_U on 𝒟_U making the restriction functor t-exact, and Remark 4.6(1) observes that τ_U is then unique. The categorical layer owns the one-functor restriction and uniqueness vocabulary; the family-level quantifier and its geometric witnesses remain in Families/SLocal.lean.

This file supplies the categorical half, for one functor at a time. It also transfers Noetherianity across an anchored lift of subobject chains. For triangulated t-exact functors, exactness of the induced heart functor supplies preservation of binary joins, so pointwise lifts along each target chain suffice. The image-factorisation step turns fixed-target arrow extension into pointwise subobject lifts; constructing those arrows geometrically remains an explicit input.

Uniqueness is really a statement about aisles. A t-structure carries two object properties, but they determine each other: t.ge (n + 1) is the right orthogonal of t.le n and conversely, by Mathlib's TStructure.isGE_iff_orthogonal and isLE_iff_orthogonal. So two t-structures with the same coconnective half are equal, and ext_le is the form Remark 4.6(1) consumes -- once one knows the aisle of τ_U is pinned, τ_U itself is.

Restriction is the data, RestrictsAlong the proposition. Quantifying either over the quasi-compact opens of a base is what S-locality will be; that quantifier is geometric and is not taken here, because the categories 𝒟_U vary with U and the base-change layer owns them.

Nothing here constructs a t-structure. Restriction is inhabited only by someone who already has τ_U, and the uniqueness statement says which τ_U that must be, not that one exists.

theorem CategoryTheory.Triangulated.TStructure.ext {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t₁ t₂ : TStructure C} (hle : t₁.le = t₂.le) (hge : t₁.ge = t₂.ge) : t₁ = t₂

A t-structure is its two object properties: every remaining field is a proposition.

theorem CategoryTheory.Triangulated.TStructure.ge_eq_of_le_eq {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t₁ t₂ : TStructure C} (hle : t₁.le = t₂.le) : t₁.ge = t₂.ge

The connective half is the right orthogonal of the coconnective half, so the coconnective half determines it.

theorem CategoryTheory.Triangulated.TStructure.ext_le {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t₁ t₂ : TStructure C} (hle : t₁.le = t₂.le) : t₁ = t₂

A t-structure is determined by its aisle. This is the engine behind the uniqueness in Remark 4.6(1) of arXiv:1902.08184: pinning the coconnective half of τ_U pins τ_U.

Noetherian hearts

The paper calls a t-structure noetherian when its heart satisfies the ascending-chain condition. The heart in this repository is an object property, so the literal categorical formulation uses its full subcategory. This predicate is intentionally independent of any geometric finiteness theorem; the latter belongs to the base-change owner.

def CategoryTheory.Triangulated.TStructure.IsNoetherian {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : Prop

The heart of t is noetherian when every heart object is a noetherian object of the heart full subcategory.

Equations

• t.IsNoetherian = ∀ (X : t.heart.FullSubcategory), CategoryTheory.IsNoetherianObject X

structure CategoryTheory.Triangulated.TStructure.Restriction {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (F : Functor C D) : Type u'

A t-structure on the target of F making F t-exact.

This is one clause of S-locality, at one functor. S-locality quantifies it over the quasi-compact opens of the base; that quantifier is geometric, because the target category varies with the open.

• tStructure : TStructure D

  The t-structure on the target.

• isTExact : F.IsTExact t self.tStructure

  The functor is t-exact for the two.

def CategoryTheory.Triangulated.TStructure.RestrictsAlong {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (F : Functor C D) : Prop

The proposition that t restricts along F, forgetting which t-structure witnesses it.

Equations

• t.RestrictsAlong F = Nonempty (t.Restriction F)

theorem CategoryTheory.Triangulated.TStructure.Restriction.restrictsAlong {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} (r : t.Restriction F) : t.RestrictsAlong F

theorem CategoryTheory.Triangulated.TStructure.Restriction.tStructure_eq_of_le_eq {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} (r₁ r₂ : t.Restriction F) (hle : r₁.tStructure.le = r₂.tStructure.le) : r₁.tStructure = r₂.tStructure

Two restrictions of t along F that agree on aisles are the same t-structure. Remark 4.6(1) is this together with a proof that the aisle of the restriction is pinned -- which is geometric, and is not claimed here.

theorem CategoryTheory.Triangulated.TStructure.Restriction.ext {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} {r₁ r₂ : t.Restriction F} (h : r₁.tStructure = r₂.tStructure) : r₁ = r₂

Equality of restriction data once their target t-structures agree.

The remaining field is a proposition, so proof irrelevance closes the restriction structure after the target equality has been transported.

noncomputable def CategoryTheory.Triangulated.TStructure.Restriction.heartFunctor {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} (r : t.Restriction F) : Functor t.heart.FullSubcategory r.tStructure.heart.FullSubcategory

The functor induced on the two hearts by a t-exact restriction.

This is the categorical map used by the noetherian-locality and filtration interfaces. It is constructed from the ambient functor and the theorem that t-exact functors carry hearts to hearts; no heart-level functor is supplied as a second, potentially inconsistent carrier.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Triangulated.TStructure.Restriction.heartFunctor_obj {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} (r : t.Restriction F) (X : t.heart.FullSubcategory) : (r.heartFunctor.obj X).obj = F.obj X.obj

@[simp]

theorem CategoryTheory.Triangulated.TStructure.Restriction.heartFunctor_map {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} (r : t.Restriction F) {X Y : t.heart.FullSubcategory} (f : X ⟶ Y) : (r.heartFunctor.map f).hom = F.map f.hom

noncomputable def CategoryTheory.Triangulated.TStructure.Restriction.heartH0Comparison {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (X : C) : r.heartFunctor.obj (t.heartH0Functor.obj X) ≅ r.tStructure.heartH0Functor.obj (F.obj X)

The objectwise comparison underlying the natural degree-zero heart cohomology comparison below.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.TStructure.Restriction.heartH0ComparisonNatIso {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) : t.heartH0Functor.comp r.heartFunctor ≅ F.comp r.tStructure.heartH0Functor

Degree-zero heart cohomology commutes naturally with a t-exact triangulated functor, after restriction to the two hearts.

Equations

• r.heartH0ComparisonNatIso = CategoryTheory.NatIso.ofComponents (fun (X : C) => r.heartH0Comparison X) ⋯

theorem CategoryTheory.Triangulated.TStructure.Restriction.fixedTargetArrowExtension_of_ambient {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (X : t.heart.FullSubcategory) (h : Subobject.FixedTargetArrowExtension F X.obj) : Subobject.FixedTargetArrowExtension r.heartFunctor X

Ambient fixed-target arrow extension induces fixed-target arrow extension on hearts after applying degree-zero cohomology. This transfers a geometric ambient extension hypothesis; it does not prove that hypothesis.

instance CategoryTheory.Triangulated.TStructure.Restriction.heartFunctor_additive {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [F.Additive] (r : t.Restriction F) : r.heartFunctor.Additive

The restriction to hearts is additive when the ambient functor is additive.

instance CategoryTheory.Triangulated.TStructure.Restriction.heartFunctor_preservesMonomorphisms {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) : r.heartFunctor.PreservesMonomorphisms

A triangulated, t-exact functor restricts to a functor preserving monomorphisms on hearts. This uses the triangle associated to a heart mono; t-exactness alone, without preservation of triangles, is insufficient.

theorem CategoryTheory.Triangulated.TStructure.Restriction.heartFunctor_shortExact {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (S : ShortComplex t.heart.FullSubcategory) (hS : S.ShortExact) : (S.map r.heartFunctor).ShortExact

A triangulated t-exact functor sends short exact sequences in the source heart to short exact sequences in the target heart.

theorem CategoryTheory.Triangulated.TStructure.Restriction.heartFunctor_finiteExact {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) : Limits.PreservesFiniteLimits r.heartFunctor ∧ Limits.PreservesFiniteColimits r.heartFunctor

Exactness on heart short exact sequences gives preservation of finite limits and colimits.

theorem CategoryTheory.Triangulated.TStructure.Restriction.heartFunctor_mapFunctor_sup {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (X : t.heart.FullSubcategory) (p q : Subobject X) : Subobject.mapFunctor r.heartFunctor (p ⊔ q) = Subobject.mapFunctor r.heartFunctor p ⊔ Subobject.mapFunctor r.heartFunctor q

The restricted heart functor preserves binary joins of subobjects. This is the categorical finite-sum step needed after pointwise lifts.

theorem CategoryTheory.Triangulated.TStructure.Restriction.isNoetherian_of_liftedSubobjectChains {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} (r : t.Restriction F) [r.heartFunctor.PreservesMonomorphisms] (hglobal : t.IsNoetherian) (hlift : ∀ (Y : r.tStructure.heart.FullSubcategory) (c : ℕ →o Subobject Y), ∃ (X : t.heart.FullSubcategory) (e : r.heartFunctor.obj X ≅ Y) (d : ℕ →o Subobject X), ∀ (n : ℕ), (Subobject.map e.hom).obj (Subobject.mapFunctor r.heartFunctor (d n)) = c n) : r.tStructure.IsNoetherian

Noetherianity transfers to a restricted heart when every ascending chain of subobjects of each target-heart object lifts to subobjects of one source-heart object, with the ambient and subobjects identified after applying the heart functor. This is the categorical consequence of an anchored filtration lift; constructing such lifts is a separate geometric obligation.

theorem CategoryTheory.Triangulated.TStructure.Restriction.isNoetherian_of_pointwiseChainLifts {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (hglobal : t.IsNoetherian) (hlift : ∀ (Y : r.tStructure.heart.FullSubcategory) (c : ℕ →o Subobject Y), ∃ (X : t.heart.FullSubcategory) (e : r.heartFunctor.obj X ≅ Y), ∀ (n : ℕ), ∃ (q : Subobject X), (Subobject.map e.hom).obj (Subobject.mapFunctor r.heartFunctor q) = c n) : r.tStructure.IsNoetherian

Pointwise lifts of each member of an ascending target-heart subobject chain into one source-heart ambient object imply Noetherianity. The geometric pointwise-lifting obligation remains explicit; finite-join preservation now follows from the exactness of the restricted heart functor.

theorem CategoryTheory.Triangulated.TStructure.Restriction.isNoetherian_of_pointwiseSubobjectLifts {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (hglobal : t.IsNoetherian) (hlift : ∀ (Y : r.tStructure.heart.FullSubcategory), ∃ (X : t.heart.FullSubcategory) (e : r.heartFunctor.obj X ≅ Y), ∀ (p : Subobject Y), ∃ (q : Subobject X), (Subobject.map e.hom).obj (Subobject.mapFunctor r.heartFunctor q) = p) : r.tStructure.IsNoetherian

A convenient whole-subobject lifting criterion for the chainwise result. The chosen source ambient object is fixed for each target-heart object.

theorem CategoryTheory.Triangulated.TStructure.Restriction.isNoetherian_of_fixedTargetMonoExtensions {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (hglobal : t.IsNoetherian) (hlift : ∀ (Y : r.tStructure.heart.FullSubcategory), ∃ (X : t.heart.FullSubcategory), Nonempty (r.heartFunctor.obj X ≅ Y) ∧ Subobject.FixedTargetMonoExtension r.heartFunctor X) : r.tStructure.IsNoetherian

For each target-heart object, choose a source lift whose fixed target admits extension of monomorphisms. This pointwise criterion implies Noetherianity without requiring arrow extension at unrelated source objects.

theorem CategoryTheory.Triangulated.TStructure.Restriction.isNoetherian_of_fixedTargetArrowExtensions {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (hglobal : t.IsNoetherian) (hExt : ∀ (X : t.heart.FullSubcategory), Subobject.FixedTargetArrowExtension r.heartFunctor X) : r.tStructure.IsNoetherian

Extension of every arrow into every fixed source-heart target is a stronger geometric criterion. The zero arrow also supplies each target-heart object as the image of some source object, so no separate object-lift premise is needed.

theorem CategoryTheory.Triangulated.TStructure.Restriction.isNoetherian_of_ambientFixedTargetArrowExtensions {D : Type u'} [Category.{v', u'} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {F : Functor C D} [IsTriangulated C] [IsTriangulated D] [F.CommShift ℤ] [F.IsTriangulated] (r : t.Restriction F) (hglobal : t.IsNoetherian) (hExt : ∀ (X : t.heart.FullSubcategory), Subobject.FixedTargetArrowExtension F X.obj) : r.tStructure.IsNoetherian

An ambient fixed-target arrow-extension hypothesis suffices for Noetherianity of the restricted heart. Establishing this hypothesis for the bounded-coherent geometric functor remains a separate obligation.

def CategoryTheory.Triangulated.TStructure.Restriction.id {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : t.Restriction (Functor.id C)

The identity functor restricts every t-structure to itself.

Equations

• CategoryTheory.Triangulated.TStructure.Restriction.id t = { tStructure := t, isTExact := ⋯ }