Constructing projections for scheme base change

This file packages the projection step of Proposition 3.15 of arXiv:1902.08184.

For each source component, compact-generator approximation data construct a chosen right projection from Dqc(X_T) onto the corresponding coproduct closure. If those ambient projectors preserve compact objects, they restrict to the compact-object carrier. An explicit compact-intersection equality then identifies the restricted component with the perfect base-change component.

The two geometric inputs which are not formal are visible in the interfaces: continuity of the compactly generated truncations, and the identification of compact objects in the coproduct closure with the perfect envelope.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.QuasicoherentProjectionApproximationData {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : Prop

Componentwise compact-generator approximations for the perfect envelopes. Their zero aisles are definitionally the quasicoherent base-change components.

• componentApproximation (i : ι) : CategoryTheory.Triangulated.TStructure.CompactGeneratorApproximation (D.perfectEnvelope (A.component i))

  Brown-style approximation data for each perfect envelope.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.QuasicoherentProjectionApproximationData.quasicoherentProjections {S : Scheme} {X T : SchemeBaseChange S} {D : X.DerivedBaseChangeData T} {ι : Type w} [Preorder ι] {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} (B : D.QuasicoherentProjectionApproximationData A) (hcompact : D.PreservesCompactObjects) (horth : D.PerfectComponentsSemiorthogonal A) : (D.quasicoherentSequence A hcompact horth).RightProjectionData

Assemble the componentwise compactly generated projections into chosen projection data for the quasicoherent sequence.

Equations

• B.quasicoherentProjections hcompact horth = { componentProjection := fun (i : ι) => ⋯.rightProjectionData }

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.QuasicoherentProjectionApproximationData.quasicoherentProjectionCocontinuous {S : Scheme} {X T : SchemeBaseChange S} {D : X.DerivedBaseChangeData T} {ι : Type w} [Preorder ι] {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} (B : D.QuasicoherentProjectionApproximationData A) (hcompact : D.PreservesCompactObjects) (horth : D.PerfectComponentsSemiorthogonal A) (htrunc : ∀ (i : ι), (⋯.tStructure.truncLE 0).PreservesSmallCoproducts) (i : ι) : ((B.quasicoherentProjections hcompact horth).ambientProjection i).PreservesSmallCoproducts

Continuity of the component truncations gives continuity of every quasicoherent ambient projector.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.QuasicoherentProjectionApproximationData.quasicoherentIsStrong {S : Scheme} {X T : SchemeBaseChange S} {D : X.DerivedBaseChangeData T} {ι : Type w} [Preorder ι] {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} (B : D.QuasicoherentProjectionApproximationData A) (hA : A.HasTriangulatedComponents) (hcompact : D.PreservesCompactObjects) (horth : D.PerfectComponentsSemiorthogonal A) : (D.quasicoherentSequence A hcompact horth).IsStrong

The constructed quasicoherent projections prove strongness once the source components are triangulated.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PerfectProjectionRestrictionData {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : D.PreservesCompactObjects) (horth : D.PerfectComponentsSemiorthogonal A) (Q : (D.quasicoherentSequence A hcompact horth).RightProjectionData) : Prop

Data identifying the compact restriction of chosen quasicoherent projectors with the perfect base-change sequence.

• projectionPreservesCompact (i : ι) : CategoryTheory.ObjectProperty.compactObjects ≤ CategoryTheory.ObjectProperty.compactObjects.inverseImage (Q.ambientProjection i)

  Each ambient quasicoherent projector preserves compact objects.

• compactIntersection (i : ι) : ((D.quasicoherentSequence A hcompact horth).component i).inverseImage (X.targetPerfectToDqc T) = (D.perfectCategorySequence A horth).component i

  The compact objects in a quasicoherent component are exactly its perfect-envelope component.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PerfectProjectionRestrictionData.perfectProjections {S : Scheme} {X T : SchemeBaseChange S} {D : X.DerivedBaseChangeData T} {ι : Type w} [Preorder ι] {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} {hcompact : D.PreservesCompactObjects} {horth : D.PerfectComponentsSemiorthogonal A} {Q : (D.quasicoherentSequence A hcompact horth).RightProjectionData} (B : D.PerfectProjectionRestrictionData A hcompact horth Q) : (D.perfectCategorySequence A horth).RightProjectionData

Restrict the quasicoherent projectors to compact objects and identify the result with the perfect base-change components.

Equations

• B.perfectProjections = { componentProjection := fun (i : ι) => ((Q.componentProjection i).restrict ⋯).ofEq ⋯ }

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PerfectProjectionRestrictionData.perfectIsStrong {S : Scheme} {X T : SchemeBaseChange S} {D : X.DerivedBaseChangeData T} {ι : Type w} [Preorder ι] {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} {hcompact : D.PreservesCompactObjects} {horth : D.PerfectComponentsSemiorthogonal A} {Q : (D.quasicoherentSequence A hcompact horth).RightProjectionData} (B : D.PerfectProjectionRestrictionData A hcompact horth Q) (hA : A.HasTriangulatedComponents) : (D.perfectCategorySequence A horth).IsStrong

Compact restriction proves strongness of the perfect sequence when the source components are triangulated.