S-local t-structures on a base-change category #
Section 4 of arXiv:1902.08184 calls a t-structure on ๐ S-local when
every quasi-compact open U โ S carries a t-structure on ๐_U making
restriction t-exact. TStructure/Local.lean supplies the one-functor half of
that sentence -- RestrictsAlong -- and observes that the restricted
t-structure is determined by its aisle. This file takes the quantifier.
Three things make the quantifier cheap to state.
๐is already a base-change category. It is๐_SatidentityBaseChange S, the terminal object ofOver S, so no separate source category is needed and restriction is an ordinary base-change pullback.- An open is already an object of
Over S, byopensBaseChange. - Base change is already functorial in the index, by
KFlatBaseChangeData.quasicoherentPullback.
What is not cheap, and is therefore an explicit input, is the base-change data
over each open. The repository's base change consumes bundled K-flat
resolutions, not just a morphism, so a family of them is what S-locality has
to quantify over; OpenRestrictionFamily is that family, and it carries the
restriction functors with it rather than deriving them.
The family and its component t-exactness remain geometric inputs. The formal
Families layer does, however, provide adapters for the affine Remark A.20
situation, the noetherian-locality equivalence, and filtration lifting. The
phase-level slicing quantifier lives in the geometric stability layer, so that
the Families layer does not import stability conditions. All adapters expose
their remaining base-change hypotheses rather than manufacturing them from
the word affine.
The restriction data S-locality quantifies over.
For each quasi-compact open of the base: a base change of X to it, and a
restriction functor from the base-change category over S itself. The functor
is carried rather than derived, because deriving it needs a derived pullback and
the component-preservation statement that quasicoherentPullback consumes, and
both are geometry.
The base change of
Xto each quasi-compact open of the base.- restriction (U : S.Opens) (hU : CompactSpace โฅโU) : CategoryTheory.Functor (DS.QuasicoherentCategory P) ((self.data U hU).QuasicoherentCategory P)
Restriction from the base to that open.
Instances For
S-locality (ยง4 of arXiv:1902.08184): the t-structure restricts along
the restriction to every quasi-compact open of the base.
This is TStructure.RestrictsAlong quantified over the family. The t-structures
on the ๐_U are existential here rather than chosen, which is the paper's
statement; Remark 4.6(1) is what makes that harmless, since
TStructure.ext_le pins each of them once its aisle is.
Equations
- R.IsSLocal t = โ (U : S.Opens) (hU : CompactSpace โฅโU), t.RestrictsAlong (R.restriction U hU)
Instances For
The chosen form: a restriction of the t-structure at every quasi-compact open, rather than the bare existence of one.
The restricted t-structure over each quasi-compact open.
Instances For
Chosen restrictions witness S-locality.
Two choices of S-local data agree at an open as soon as their aisles do.
This is Remark 4.6(1) with its geometric half left visible: what pins the aisle
of the restricted t-structure is that ๐_U is generated by the image of ๐,
which is a generation theorem about base change and is not proved here.
The equality below is the chosen-data form of Remark 4.6(1). It still
needs the geometric aisle comparison at every open; the categorical part is
the extensionality of TStructure.
Lemma 4.15 and Lemma 4.16(3) #
The repository owns the heart predicate and the shape of an arbitrary filtration. The finite-cover direction of noetherian locality is proved from the repository's finite-family detector, conditional on the geometric facts that restrictions preserve heart monomorphisms and jointly detect isomorphisms. The converse direction and the geometric filtration lift remain owner inputs.
Apply CategoryTheory.isNoetherianObject_of_finite_jointlyReflectsIsomorphisms
to each object of the global heart. Joint isomorphism reflection is the
categorical detection hypothesis used here; no topological covering proof is
stored in the restriction family.
Owner data for the noetherian-locality equivalence of Lemma 4.15.
The finite family below is intended to come from a quasi-compact open cover.
Since OpenRestrictionFamily carries abstract functors, a topological cover
alone would not prove that they detect isomorphisms; the categorical
conservativity and mono-preservation obligations are retained as fields.
- localData : R.SLocalData t
The S-local data the two implications below are stated against. Carried rather than existentially quantified, because
lemma_4_15hands its callerH.localData.restriction U hUand a proposition would not. - global_to_local : t.IsNoetherian โ โ (U : S.Opens) (hU : CompactSpace โฅโU), (self.localData.restriction U hU).tStructure.IsNoetherian
- index : Type u
A finite index for the detecting restrictions.
The quasi-compact opens used for detection.
- compact (i : self.index) : CompactSpace โฅโ(self.opens i)
- preservesMonomorphisms (i : self.index) : (self.localData.restriction (self.opens i) โฏ).heartFunctor.PreservesMonomorphisms
Exactness on hearts, or another proof that restriction preserves monos.
- jointlyReflectsIsomorphisms {Y Z : t.heart.FullSubcategory} (f : Y โถ Z) : (โ (i : self.index), CategoryTheory.IsIso ((self.localData.restriction (self.opens i) โฏ).heartFunctor.map f)) โ CategoryTheory.IsIso f
The geometric conservativity of restriction on this finite cover.
Instances For
The local-to-global half of Lemma 4.15 follows from the chosen finite
detecting family. This adapter supplies the finite detector above with the
record's categorical hypotheses; the converse global_to_local is not used.
An arbitrary (not necessarily finite) chain of monomorphisms.
- object : โ โ C
The
n-th object of the chain. The map from the
n-th object to then+1-st.monobelow is what makes it an inclusion; this field alone claims only a morphism.- mono (n : โ) : CategoryTheory.Mono (self.inclusion n)
Instances For
Owner data for lifting an arbitrary heart filtration as in Lemma 4.16(3).
Named Lemma416Part3Data rather than Lemma416_3Data: the defsWithUnderscore
linter reads the underscore separating the lemma number from its clause and
flags every field of the structure, and this repository's nolints.json is a
shrink-only ratchet, so silencing it is not available. The paper reference is
unchanged -- Lemma 4.16, clause (3).
- lift (U : S.Opens) (hU : CompactSpace โฅโU) (F : Filtration (L.restriction U hU).tStructure.heart.FullSubcategory) : Filtration t.heart.FullSubcategory
Lifts a filtration in the heart restricted to
Uto one in the global heart. It is owner data, not a construction: nothing here builds the lift. - comparison (U : S.Opens) (hU : CompactSpace โฅโU) (F : Filtration (L.restriction U hU).tStructure.heart.FullSubcategory) (n : โ) : (L.restriction U hU).heartFunctor.obj ((self.lift U hU F).object n) โ F.object n
Identifies the
n-th object of the lifted filtration, restricted back toU, with then-th object it was lifted from.commbelow is what makes the identification compatible with the inclusions. - comm (U : S.Opens) (hU : CompactSpace โฅโU) (F : Filtration (L.restriction U hU).tStructure.heart.FullSubcategory) (n : โ) : CategoryTheory.CategoryStruct.comp (self.comparison U hU F n).hom (F.inclusion n) = CategoryTheory.CategoryStruct.comp ((L.restriction U hU).heartFunctor.map ((self.lift U hU F).inclusion n)) (self.comparison U hU F (n + 1)).hom
Instances For
The filtration-lifting conclusion in the orientation of Lemma 4.16(3).