Bounded coherent realization of categorical pre-stability base change

This file connects the actual bounded coherent pullback from Families.BoundedGeometry, with its identity and composition laws from Families.CoherentPullbackCoherence, to FiberPreStabilityBaseChangeData.

The bridge has three layers.

• BoundedCoherentPullbackPreimageData is the explicit preimage witness for one geometric pullback. Its identity and composition constructors use the bounded derived-pullback unit and compositor.
• BoundedCoherentPullbackInducingData records the actual phase-indexed A.17 output for that pullback. The owned Corollary-A.23 theorem converts this output into preimage data.
• BoundedCoherentDerivedRealization identifies an abstract strict fiber family with the genuine Dᵇ(Coh) fibers and their pullbacks. GeometricPreStabilityBaseChangeData.toFiberPreStabilityBaseChangeData then exports the downstream witness without accepting Slicing.PreimageData from the caller.

This file does not manufacture the scheme-specific A.17 realization from flatness. It does, however, consume its honest phase-indexed output directly: there is no global theorem switch and no preconstructed Slicing.PreimageData input. Openness and relative-HN consequences are exported downstream.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackPreimageData {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] (s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber) : Prop

Explicit preimage-slicing data for bounded coherent derived pullback along one morphism of locally Noetherian scheme base changes.

• preimageData : s.PreimageData (boundedCoherentDerivedPullback f)

  The two non-formal slicing axioms for the actual bounded coherent pullback.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackPreimageData.preimage {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] {s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber} (h : BoundedCoherentPullbackPreimageData f s) : CategoryTheory.Triangulated.Slicing U.BoundedCoherentDerivedFiber

The slicing constructed on the target bounded coherent fiber.

Equations

• h.preimage = s.preimage (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedCoherentDerivedPullback f) ⋯

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackPreimageData.identity {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasCoherentPullback (CategoryTheory.CategoryStruct.id T)] (s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber) : BoundedCoherentPullbackPreimageData (CategoryTheory.CategoryStruct.id T) s

The bounded coherent pullback unit supplies the identity preimage witness.

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackPreimageData.preimage_identity {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasCoherentPullback (CategoryTheory.CategoryStruct.id T)] (s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber) : ⋯.preimage = s

The slicing induced along the identity is the original slicing.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackPreimageData.comp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [IsLocallyNoetherian (CategoryTheory.Over.left V)] [HasCoherentPullback f] [HasCoherentPullback g] [HasCoherentPullback (CategoryTheory.CategoryStruct.comp f g)] {s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber} (hf : BoundedCoherentPullbackPreimageData f s) (hg : BoundedCoherentPullbackPreimageData g hf.preimage) : BoundedCoherentPullbackPreimageData (CategoryTheory.CategoryStruct.comp f g) s

Geometric bounded coherent preimage witnesses compose through the actual bounded derived-pullback compositor.

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackPreimageData.preimage_comp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [IsLocallyNoetherian (CategoryTheory.Over.left V)] [HasCoherentPullback f] [HasCoherentPullback g] [HasCoherentPullback (CategoryTheory.CategoryStruct.comp f g)] {s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber} (hf : BoundedCoherentPullbackPreimageData f s) (hg : BoundedCoherentPullbackPreimageData g hf.preimage) : ⋯.preimage = hg.preimage

One-step and two-step geometric bounded coherent preimages agree.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackInducingData {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] (s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber) : Type (u + 1)

The phase-indexed A.17 output specialized to actual bounded coherent derived pullback.

• inducedTStructures : s.InducedTStructures (boundedCoherentDerivedPullback f)

  The induced source t-structures with the A.8 recognition formulas.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackInducingData.identity {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasCoherentPullback (CategoryTheory.CategoryStruct.id T)] (s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber) : BoundedCoherentPullbackInducingData (CategoryTheory.CategoryStruct.id T) s

The bounded derived-pullback unit transports the inhabited identity A.17 model to the concrete bounded-coherent identity pullback.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BoundedCoherentPullbackInducingData.toPreimageData {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] {s : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber} (h : BoundedCoherentPullbackInducingData f s) : BoundedCoherentPullbackPreimageData f s

Apply the owned finite phase-truncation theorem to the actual A.17 output.

structure AlgebraicGeometry.DerivedCategory.Families.BoundedCoherentDerivedRealization {S : Scheme} (F : SchemeTriangulatedFiberFamily S) [∀ (T : SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : SchemeBaseChange S} → (f : T ⟶ U) → SchemeBaseChange.HasCoherentPullback f] : Type (max (u + 1) u_1)

A pseudofunctorial triangulated fiber family realized by the genuine bounded coherent derived categories, with every abstract pullback identified with the actual bounded coherent pullback.

• fiberEquivalence (T : SchemeBaseChange S) : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T ≌ T.BoundedCoherentDerivedFiber

  Equivalence from each abstract fiber to Dᵇ(Coh).

• fiberEquivalenceFunctorCommShift (T : SchemeBaseChange S) : (self.fiberEquivalence T).functor.CommShift ℤ

  The chosen forward functor commutes with shifts. Mathlib derives the unique compatible shift structure on the inverse functor from this one.

• fiberEquivalenceCommShift (T : SchemeBaseChange S) : (self.fiberEquivalence T).CommShift ℤ

  Unit and counit coherence for the derived inverse shift structure.

• fiberEquivalenceIsTriangulated (T : SchemeBaseChange S) : (self.fiberEquivalence T).IsTriangulated

  The equivalence is triangulated. Mathlib derives exactness and additivity for both directions from this equivalence-level property.

• pullbackIso {T U : SchemeBaseChange S} (f : T ⟶ U) : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F f ≅ (self.fiberEquivalence U).functor.comp ((SchemeBaseChange.boundedCoherentDerivedPullback f).comp (self.fiberEquivalence T).inverse)

  Abstract pullback is the actual bounded coherent pullback, transported through the two fiber equivalences.

theorem AlgebraicGeometry.DerivedCategory.Families.BoundedCoherentDerivedRealization.inversePreimageData {S : Scheme} {F : SchemeTriangulatedFiberFamily S} [∀ (T : SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : SchemeBaseChange S} → (f : T ⟶ U) → SchemeBaseChange.HasCoherentPullback f] (R : BoundedCoherentDerivedRealization F) (T : SchemeBaseChange S) (s : CategoryTheory.Triangulated.Slicing (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T)) : s.PreimageData (R.fiberEquivalence T).inverse

The standard Mathlib triangulated-equivalence structure supplies preimage data for the inverse fiber equivalence.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.BoundedCoherentDerivedRealization.inversePreimage {S : Scheme} {F : SchemeTriangulatedFiberFamily S} [∀ (T : SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : SchemeBaseChange S} → (f : T ⟶ U) → SchemeBaseChange.HasCoherentPullback f] (R : BoundedCoherentDerivedRealization F) (T : SchemeBaseChange S) (s : CategoryTheory.Triangulated.Slicing (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T)) : CategoryTheory.Triangulated.Slicing T.BoundedCoherentDerivedFiber

Transport a slicing from an abstract fiber to its bounded coherent realization through the inverse equivalence.

Equations

• R.inversePreimage T s = s.preimage (R.fiberEquivalence T).inverse ⋯

theorem AlgebraicGeometry.DerivedCategory.Families.BoundedCoherentDerivedRealization.preimageData {S : Scheme} {F : SchemeTriangulatedFiberFamily S} [∀ (T : SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : SchemeBaseChange S} → (f : T ⟶ U) → SchemeBaseChange.HasCoherentPullback f] (R : BoundedCoherentDerivedRealization F) {T U : SchemeBaseChange S} (f : T ⟶ U) (s : CategoryTheory.Triangulated.Slicing (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T)) (h : SchemeBaseChange.BoundedCoherentPullbackInducingData f (R.inversePreimage T s)) : s.PreimageData (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F f)

Transport the genuine bounded coherent A.17 output through a bounded coherent realization. The result is preimage data for the abstract family pullback, not a caller-supplied preimage witness.

structure AlgebraicGeometry.DerivedCategory.Families.GeometricPreStabilityBaseChangeData {S : Scheme} (F : SchemeTriangulatedFiberFamily S) [∀ (T : SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : SchemeBaseChange S} → (f : T ⟶ U) → SchemeBaseChange.HasCoherentPullback f] (R : BoundedCoherentDerivedRealization F) {V : Type uV} [AddCommGroup V] (classMap : (T : SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V) (sigma : (T : SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)) : Type (u + 1)

Geometric inducing data for a pre-stability family. Unlike FiberPreStabilityBaseChangeData, this structure does not contain a Slicing.PreimageData field: every such witness is constructed from the actual bounded coherent pullback and its phase-indexed A.17 output.

• classMapCompatible : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.CompatibleClassMaps F V classMap

  The common numerical class is invariant under pullback.

• chargeCompatible {T U : SchemeBaseChange S} : ∀ (x : T ⟶ U), (sigma T).Z = (sigma U).Z

  All fibers use the same central charge.

• inducing {T U : SchemeBaseChange S} (f : T ⟶ U) : SchemeBaseChange.BoundedCoherentPullbackInducingData f (R.inversePreimage T (sigma T).slicing)

  The geometric inducing premises on the actual bounded coherent pullback.

• slicingCompatible {T U : SchemeBaseChange S} (f : T ⟶ U) : (sigma U).slicing = (sigma T).slicing.preimage (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F f) ⋯

  The supplied target slicing is the one induced geometrically. The preimage witness occurring here is constructed from inducing; it is not a field of this structure.

theorem AlgebraicGeometry.DerivedCategory.Families.GeometricPreStabilityBaseChangeData.toFiberPreStabilityBaseChangeData {S : Scheme} {F : SchemeTriangulatedFiberFamily S} [∀ (T : SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : SchemeBaseChange S} → (f : T ⟶ U) → SchemeBaseChange.HasCoherentPullback f] {R : BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : GeometricPreStabilityBaseChangeData F R classMap sigma) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma

Export the ordinary categorical base-change witness. Its preimage field is built from bounded coherent geometry and the inducing theorem.

theorem AlgebraicGeometry.DerivedCategory.Families.GeometricPreStabilityBaseChangeData.phase_iff {S : Scheme} {F : SchemeTriangulatedFiberFamily S} [∀ (T : SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : SchemeBaseChange S} → (f : T ⟶ U) → SchemeBaseChange.HasCoherentPullback f] {R : BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : GeometricPreStabilityBaseChangeData F R classMap sigma) {T U : SchemeBaseChange S} (f : T ⟶ U) (phi : ℝ) (E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F U) : (sigma U).slicing.P phi E ↔ (sigma T).slicing.P phi ((CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F f).obj E)

Phase membership is detected by the geometrically realized bounded coherent pullback.

theorem AlgebraicGeometry.DerivedCategory.Families.GeometricPreStabilityBaseChangeData.phase_iff_comp {S : Scheme} {F : SchemeTriangulatedFiberFamily S} [∀ (T : SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : SchemeBaseChange S} → (f : T ⟶ U) → SchemeBaseChange.HasCoherentPullback f] {R : BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : GeometricPreStabilityBaseChangeData F R classMap sigma) {T U V' : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V') (phi : ℝ) (E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F V') : (sigma V').slicing.P phi E ↔ (sigma T).slicing.P phi ((CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F f).obj ((CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F g).obj E))

The geometric witness inherits pseudofunctorial composition compatibility after its pullbacks have been identified with bounded coherent derived pullback.