Scheme-derived pullback realizes categorical inducing data

This file connects the concrete exact derived pullback on scheme fibers to the honest preimage-slicing boundary. A DerivedPullbackInducingData records the actual phase-indexed t-structures produced by the owned A.17 theorem for SchemeBaseChange.derivedPullback f. The owned Corollary-A.23 truncation argument then constructs the preimage slicing; no global theorem parameter or caller-supplied Slicing.PreimageData is accepted. Flatness is used only to install exact derived pullback.

Once explicit preimage data has been obtained, identity and composition use the coherence from Phase.Transfer.Basic and the exact derived-pullback unit and compositor. No geometric slicing, openness, relative HN, bounded coherent/perfect restriction, or conclusion of Theorem 22.2 is asserted.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackPreimageData {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] (s : CategoryTheory.Triangulated.Slicing T.DerivedFiber) : Prop

Explicit preimage-slicing data for the concrete exact derived pullback along one morphism of scheme base changes.

• preimageData : s.PreimageData (derivedPullback f)

  The two non-formal slicing axioms for detecting phases by derived pullback.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackPreimageData.preimage {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} [IsExactPullback f] {s : CategoryTheory.Triangulated.Slicing T.DerivedFiber} (h : DerivedPullbackPreimageData f s) : CategoryTheory.Triangulated.Slicing U.DerivedFiber

The slicing on the target derived fiber constructed from the explicit preimage witness.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackPreimageData.identity {S : Scheme} (T : SchemeBaseChange S) (s : CategoryTheory.Triangulated.Slicing T.DerivedFiber) : DerivedPullbackPreimageData (CategoryTheory.CategoryStruct.id T) s

Exact derived pullback along an identity carries the canonical identity preimage witness across the derived unit isomorphism.

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackPreimageData.preimage_identity {S : Scheme} (T : SchemeBaseChange S) (s : CategoryTheory.Triangulated.Slicing T.DerivedFiber) : ⋯.preimage = s

The slicing induced through exact derived pullback along an identity is the original slicing.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackPreimageData.comp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] [IsExactPullback g] {s : CategoryTheory.Triangulated.Slicing T.DerivedFiber} (hf : DerivedPullbackPreimageData f s) (hg : DerivedPullbackPreimageData g hf.preimage) : DerivedPullbackPreimageData (CategoryTheory.CategoryStruct.comp f g) s

Explicit derived-pullback preimage witnesses compose and are transported from the iterated functor to pullback along the composite by the derived compositor.

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackPreimageData.preimage_comp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] [IsExactPullback g] {s : CategoryTheory.Triangulated.Slicing T.DerivedFiber} (hf : DerivedPullbackPreimageData f s) (hg : DerivedPullbackPreimageData g hf.preimage) : ⋯.preimage = hg.preimage

The slicing induced along a composite exact derived pullback agrees with the slicing obtained in two stages.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackInducingData {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] (s : CategoryTheory.Triangulated.Slicing T.DerivedFiber) : Type (u + 1)

The phase-indexed A.17 output specialized to concrete exact derived pullback. This is the recognition-formula output consumed by the owned Corollary-A.23 theorem, not a preconstructed slicing witness.

• inducedTStructures : s.InducedTStructures (derivedPullback f)

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackInducingData.identity {S : Scheme} (T : SchemeBaseChange S) (s : CategoryTheory.Triangulated.Slicing T.DerivedFiber) : DerivedPullbackInducingData (CategoryTheory.CategoryStruct.id T) s

The exact derived-pullback unit transports the inhabited identity A.17 model to the concrete scheme-derived identity pullback.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackInducingData.identity T s = { inducedTStructures := s.inducedTStructuresId.ofIso T.derivedPullbackId.symm }

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackInducingData.toPreimageData {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} [IsExactPullback f] {s : CategoryTheory.Triangulated.Slicing T.DerivedFiber} (h : DerivedPullbackInducingData f s) : DerivedPullbackPreimageData f s

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedPullbackInducingData.toPreimageData_of_flat {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] (s : CategoryTheory.Triangulated.Slicing T.DerivedFiber) (h : DerivedPullbackInducingData f s) : DerivedPullbackPreimageData f s

For a flat scheme morphism, Mathlib flatness supplies exact derived pullback; the A.17 output remains the honest geometric input.