Lifting a functor to full subcategories cut out by object properties #
Mathlib's ObjectProperty.lift restricts a functor to the full subcategory a property cuts out,
and ObjectProperty.inverseImage pulls a property back along a functor. This file combines the
two: given F : C ⥤ D and properties P on C and Q on D with P ≤ F⁻¹ Q, it names the
restriction P.FullSubcategory ⥤ Q.FullSubcategory, transports the Additive, CommShift ℤ, and
IsTriangulated instances lift already carries, and restricts an adjunction on either side of
F to those subcategories.
Nothing here mentions a t-structure, a slicing, or a stability condition. The declarations lived in
CategoryTheory/Triangulated/TStructure/Restriction.lean until this cutover because that is where
Theorem A.17 of arXiv:2607.28411v1 first needed them; their carrier is ObjectProperty, whose
lift, ι, ιOfLE, liftCompιIso, and fullyFaithfulι Mathlib defines in
Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean, so this file mirrors that directory.
It is named for the operation it adds rather than for Mathlib's file because
ObjectProperty/FullSubcategory.lean is one of the two paths scripts/check_source_independence.py
keeps retired -- a verbatim copy from the retired stability source once lived there and was replaced
by an owner-native proof, and that gate has no allowlist. The consumers now import this file
directly. That the block is not t-structure theory is settled by its own import list: it needs
Mathlib alone, and nothing from DerivedAlgGeo.
Main definitions #
ObjectProperty.liftOfLE: the restriction ofFto a subcategoryP ≤ F⁻¹ Q, landing inQ, with theAdditive,CommShift ℤ, andIsTriangulatedinstances a triangulated consumer needs.ObjectProperty.preimageLift: its case of a two-way detectionP X ↔ Q (F.obj X).ObjectProperty.preimageLiftEquivalence: that restriction of an equivalence is an equivalence.ObjectProperty.inverseImageLift: itsP = F⁻¹ Qcase.ObjectProperty.liftToInverseImage: the restriction of a functor in the other direction whose composite withFpreservesQ.Adjunction.restrictInverseImageLeftandAdjunction.restrictInverseImageRight: an adjunction on either side ofFrestricted to those subcategories, through Mathlib'sAdjunction.restrictFullyFaithful; the suffix names which adjoint ofFis restricted.
References #
- arXiv:2607.28411v1, Theorem A.17 and Proposition 3.8, where these restrictions are used.
The restriction of F to a full subcategory P ≤ F⁻¹ Q, landing in Q.
Definitionally ObjectProperty.ιOfLE hle ⋙ inverseImageLift F Q, but defined
as Q.lift (P.ι ⋙ F) _ because Mathlib's ιOfLE carries no Additive,
CommShift, or IsTriangulated instance while lift carries all three; the
instances below are those, transported. Its F = 𝟭 case is ιOfLE.
Equations
- CategoryTheory.ObjectProperty.liftOfLE F hle = Q.lift (P.ι.comp F) ⋯
Instances For
Equations
- CategoryTheory.ObjectProperty.instCommShiftLiftOfLE hle = { commShiftIso := CategoryTheory.ObjectProperty.instCommShiftLiftOfLE._aux_1 hle, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }
The functor between the two full subcategories selected by a detection
equivalence: liftOfLE along its forward direction, by definition.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Restricting an essentially surjective functor along a property detected by that functor is still essentially surjective. Every target object has an ambient preimage; invariance under isomorphism puts that preimage in the source property, and the ambient isomorphism lifts to the two full subcategories.
A functor that is an equivalence restricts to an equivalence between the two full subcategories a detection cuts out.
Full faithfulness restricts for free, by Mathlib's instances on lift and the
full faithfulness of a full-subcategory inclusion. Essential surjectivity is the
half that uses the detection: an ambient preimage is carried into P by the
backward direction of hmem, and repleteness of Q lifts the ambient
isomorphism.
Equations
Instances For
The restriction of F to the objects whose image lies in Q, landing
in Q. This is the functor between the selected subcategories under
hypothesis (iv) of Theorem A.17 of arXiv:2607.28411v1, P = F⁻¹ Q, the
form Polishchuk.induce produces.
Kept an abbrev, hence reducible, so that a Polishchuk.InducedTStructureData
field stated with liftOfLE F le_rfl (Polishchuk.induce) is definitionally
this functor; Slicing.IndExtensions.nonempty_inducedTStructures relies on
that.
Equations
Instances For
The restriction of L : D ⥤ C to Q, landing in F⁻¹ Q, when F ∘ L
preserves Q. For L a left adjoint of F this is the bounded left
adjoint of inverseImageLift F Q; geometrically, f_! on Dᵇ(Coh) when it
preserves bounded coherent complexes.
Equations
- CategoryTheory.ObjectProperty.liftToInverseImage F Q L hL = (Q.inverseImage F).lift (Q.ι.comp L) ⋯
Instances For
An adjunction L ⊣ F restricts to Q ⊆ D and F⁻¹ Q ⊆ C when the monad
F L preserves Q; the restricted functors are liftToInverseImage and
inverseImageLift, and the comparison isomorphisms are liftCompιIso, so
nothing is transported. Geometrically this is f_! ⊣ f^* on Dᵇ(Coh), under
the hypothesis that the monad f^* f_! preserves bounded coherent complexes,
which Proposition 3.8 of arXiv:2607.28411v1 obtains from f_!(Dᵇ) ⊆ Dᵇ,
itself a consequence of perfectness of the relative dualizing complex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An adjunction F ⊣ R restricts to F⁻¹ Q ⊆ C and Q ⊆ D when the comonad
F R preserves Q; the restricted functors are inverseImageLift and
liftToInverseImage, and the comparison isomorphisms are liftCompιIso, so
nothing is transported. Geometrically this is f^* ⊣ f_* on Dᵇ(Coh), under
the hypothesis that the comonad f^* f_* preserves bounded coherent
complexes, exactly what condition (3.2) of arXiv:2607.28411v1 needs in order
to be stated there.
Equations
- One or more equations did not get rendered due to their size.