Pullback between derived base-change categories

A morphism f : T ⟶ U over S induces X ×_S T ⟶ X ×_S U. The generic part of this file restricts any supplied Dqc pullback to (Dqc)_U ⟶ (Dqc)_T and D_U ⟶ D_T. The separate KFlatBaseChangeData.pullbackAlong constructor is the K-flat producer for that ambient pullback.

The only component-level hypothesis is preservation of (Dqc). Once the derived pullback also preserves bounded coherent cohomology, preservation of D_U follows formally because D_U was constructed as the inverse image of (Dqc)_U in that intrinsic bounded-coherent locus.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.baseChangeMap {S : Scheme} (X : SchemeBaseChange S) {T U : SchemeBaseChange S} (f : T ⟶ U) : X ⨯ T ⟶ X ⨯ U

The morphism X ×_S T ⟶ X ×_S U induced by f : T ⟶ U.

Equations

• X.baseChangeMap f = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.baseChangeMap_isPullback {S : Scheme} (X : SchemeBaseChange S) {T U : SchemeBaseChange S} (f : T ⟶ U) : CategoryTheory.IsPullback (X.baseChangeSnd T) (X.baseChangeMap f) f (X.baseChangeSnd U)

The square formed by X ×_S f and the second projections is a pullback square in the category of schemes over S.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isOpenImmersion_baseChangeMap {S : Scheme} (X : SchemeBaseChange S) {T U : SchemeBaseChange S} (f : T ⟶ U) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : IsOpenImmersion (CategoryTheory.Over.Hom.left (X.baseChangeMap f))

Open immersions are preserved by the product base change X ×_S -.

@[instance 900]

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isOpenImmersionBaseChangeMap {S : Scheme} (X : SchemeBaseChange S) {T U : SchemeBaseChange S} (f : T ⟶ U) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : IsOpenImmersion (CategoryTheory.Over.Hom.left (X.baseChangeMap f))

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.quasiCompact_baseChangeMap {S : Scheme} (X : SchemeBaseChange S) {T U : SchemeBaseChange S} (f : T ⟶ U) [QuasiCompact (CategoryTheory.Over.Hom.left f)] : QuasiCompact (CategoryTheory.Over.Hom.left (X.baseChangeMap f))

Quasi-compact morphisms are preserved by the product base change X ×_S -.

@[instance 900]

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.quasiCompactBaseChangeMap {S : Scheme} (X : SchemeBaseChange S) {T U : SchemeBaseChange S} (f : T ⟶ U) [QuasiCompact (CategoryTheory.Over.Hom.left f)] : QuasiCompact (CategoryTheory.Over.Hom.left (X.baseChangeMap f))

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isAffineHom_baseChangeMap {S : Scheme} (X : SchemeBaseChange S) {T U : SchemeBaseChange S} (f : T ⟶ U) [IsAffineHom (CategoryTheory.Over.Hom.left f)] : IsAffineHom (CategoryTheory.Over.Hom.left (X.baseChangeMap f))

Affine morphisms are preserved by the product base change X ×_S -. In particular, the induced morphism remains affine when the original morphism is an affine localization.

@[instance 900]

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isAffineHomBaseChangeMap {S : Scheme} (X : SchemeBaseChange S) {T U : SchemeBaseChange S} (f : T ⟶ U) [IsAffineHom (CategoryTheory.Over.Hom.left f)] : IsAffineHom (CategoryTheory.Over.Hom.left (X.baseChangeMap f))

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcLeftDerivedPullback.PreservesBoundedCoherent {S : Scheme} {V W : SchemeBaseChange S} {f : V ⟶ W} (pull : DqcLeftDerivedPullback f) : Prop

A Dqc derived pullback preserves the intrinsic bounded-coherent locus.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcLeftDerivedPullback.boundedFunctor {S : Scheme} {V W : SchemeBaseChange S} {f : V ⟶ W} (pull : DqcLeftDerivedPullback f) (h : pull.PreservesBoundedCoherent) : CategoryTheory.Functor (Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left W)) (Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left V))

Restrict a Dqc derived pullback to intrinsic bounded-coherent complexes.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcLeftDerivedPullback.boundedFunctorCompInclusion {S : Scheme} {V W : SchemeBaseChange S} {f : V ⟶ W} (pull : DqcLeftDerivedPullback f) (h : pull.PreservesBoundedCoherent) : (pull.boundedFunctor h).comp (Dqc.SchemeBoundedCoherentDqcCategory.ι (CategoryTheory.Over.left V)) ≅ (Dqc.SchemeBoundedCoherentDqcCategory.ι (CategoryTheory.Over.left W)).comp pull.functor

Forgetting bounded-coherent witnesses recovers the Dqc pullback.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcLeftDerivedPullback.boundedFunctor_obj_obj {S : Scheme} {V W : SchemeBaseChange S} {f : V ⟶ W} (pull : DqcLeftDerivedPullback f) (h : pull.PreservesBoundedCoherent) (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left W)) : ((pull.boundedFunctor h).obj E).obj = pull.functor.obj E.obj

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.pullbackAlong {S : Scheme} {X T U : SchemeBaseChange S} (D : X.KFlatBaseChangeData U) (f : T ⟶ U) (hAcyclic : KFlatPullbackAcyclic D.tensorResolution (X.baseChangeMap f)) (hQuasicoherent : KFlatResolvedPullbackPreservesQuasicoherentCohomology D.tensorResolution (X.baseChangeMap f)) : DqcLeftDerivedPullback (X.baseChangeMap f)

Construct pullback along X ×_S T ⟶ X ×_S U from the K-flat resolution on X ×_S U carried by the target base-change data.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.pullbackAlong_ambient_essSurj_of_isOpenImmersion {S : Scheme} {X T U : SchemeBaseChange S} (D : X.KFlatBaseChangeData U) (f : T ⟶ U) (hAcyclic : KFlatPullbackAcyclic D.tensorResolution (X.baseChangeMap f)) (hQuasicoherent : KFlatResolvedPullbackPreservesQuasicoherentCohomology D.tensorResolution (X.baseChangeMap f)) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : (D.pullbackAlong f hAcyclic hQuasicoherent).ambient.functor.EssSurj

For an open immersion of bases, the honest ambient left-derived functor underlying the K-flat pullback is essentially surjective. Open immersions are stable under the product base change X ×_S -, and the preceding geometric construction applies to that induced open immersion.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PullbackPreservesQuasicoherentComponent {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) : Prop

The exact component-level statement that pullback along f preserves the constructed quasicoherent base-change component.

Equations

• DT.PullbackPreservesQuasicoherentComponent DU P pull = (DU.quasicoherentComponent P ≤ (DT.quasicoherentComponent P).inverseImage pull.functor)

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PullbackMapsPerfectEnvelope {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) : Prop

The smaller generator-level condition that pullback sends the source perfect envelope into the target quasicoherent component.

Equations

• DT.PullbackMapsPerfectEnvelope DU P pull = ((DU.perfectEnvelope P).map pull.functor ≤ DT.quasicoherentComponent P)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.pullback_preservesQuasicoherentComponent_of_perfectEnvelope {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) [pull.functor.CommShift ℤ] [pull.functor.IsTriangulated] (hCoproducts : pull.functor.PreservesSmallCoproducts) (hEnvelope : DT.PullbackMapsPerfectEnvelope DU P pull) : DT.PullbackPreservesQuasicoherentComponent DU P pull

A coproduct-preserving triangulated pullback preserves the whole quasicoherent component once it maps the perfect envelope into the target component.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullback {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (h : DT.PullbackPreservesQuasicoherentComponent DU P pull) : CategoryTheory.Functor (DU.QuasicoherentCategory P) (DT.QuasicoherentCategory P)

Pullback between the constructed quasicoherent base-change categories.

Equations

• DT.quasicoherentPullback DU P pull h = CategoryTheory.ObjectProperty.liftOfLE pull.functor h

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackOfPerfectEnvelope {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) [pull.functor.CommShift ℤ] [pull.functor.IsTriangulated] (hCoproducts : pull.functor.PreservesSmallCoproducts) (hEnvelope : DT.PullbackMapsPerfectEnvelope DU P pull) : CategoryTheory.Functor (DU.QuasicoherentCategory P) (DT.QuasicoherentCategory P)

Pullback between quasicoherent base-change components, constructed from the smaller perfect-envelope preservation condition.

Equations

• DT.quasicoherentPullbackOfPerfectEnvelope DU P pull hCoproducts hEnvelope = DT.quasicoherentPullback DU P pull ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackCompInclusion {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (h : DT.PullbackPreservesQuasicoherentComponent DU P pull) : (DT.quasicoherentPullback DU P pull h).comp (DT.quasicoherentComponent P).ι ≅ (DU.quasicoherentComponent P).ι.comp pull.functor

Forgetting component witnesses recovers the ambient Dqc pullback.

Equations

• DT.quasicoherentPullbackCompInclusion DU P pull h = (DT.quasicoherentComponent P).liftCompιIso ((DU.quasicoherentComponent P).ι.comp pull.functor) ⋯

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.pullback_preservesBoundedComponent {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hDqc : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hBounded : pull.PreservesBoundedCoherent) : DU.boundedComponent P ≤ (DT.boundedComponent P).inverseImage (pull.boundedFunctor hBounded)

Preservation of the bounded component follows from preservation of (Dqc) together with preservation of bounded coherent cohomology by the same derived pullback.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullback {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hDqc : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hBounded : pull.PreservesBoundedCoherent) : CategoryTheory.Functor (DU.BoundedCategory P) (DT.BoundedCategory P)

Pullback between the constructed bounded base-change categories.

Equations

• DT.boundedPullback DU P pull hDqc hBounded = CategoryTheory.ObjectProperty.liftOfLE (pull.boundedFunctor hBounded) ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackOfPerfectEnvelope {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) [pull.functor.CommShift ℤ] [pull.functor.IsTriangulated] (hCoproducts : pull.functor.PreservesSmallCoproducts) (hEnvelope : DT.PullbackMapsPerfectEnvelope DU P pull) (hBounded : pull.PreservesBoundedCoherent) : CategoryTheory.Functor (DU.BoundedCategory P) (DT.BoundedCategory P)

Bounded pullback constructed from perfect-envelope preservation and preservation of intrinsic bounded-coherent objects.

Equations

• DT.boundedPullbackOfPerfectEnvelope DU P pull hCoproducts hEnvelope hBounded = DT.boundedPullback DU P pull ⋯ hBounded

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackCompInclusion {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hDqc : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hBounded : pull.PreservesBoundedCoherent) : (DT.boundedPullback DU P pull hDqc hBounded).comp (DT.boundedComponent P).ι ≅ (DU.boundedComponent P).ι.comp (pull.boundedFunctor hBounded)

Forgetting component witnesses recovers pullback on the intrinsic bounded-coherent loci.

Equations

• DT.boundedPullbackCompInclusion DU P pull hDqc hBounded = (DT.boundedComponent P).liftCompιIso ((DU.boundedComponent P).ι.comp (pull.boundedFunctor hBounded)) ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.kFlatQuasicoherentPullback {S : Scheme} {X T U : SchemeBaseChange S} (DT : X.KFlatBaseChangeData T) (DU : X.KFlatBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (f : T ⟶ U) (hAcyclic : KFlatPullbackAcyclic DU.tensorResolution (X.baseChangeMap f)) (hQuasicoherent : KFlatResolvedPullbackPreservesQuasicoherentCohomology DU.tensorResolution (X.baseChangeMap f)) (hComponent : DT.toDerivedBaseChangeData.PullbackPreservesQuasicoherentComponent DU.toDerivedBaseChangeData P (DU.pullbackAlong f hAcyclic hQuasicoherent)) : CategoryTheory.Functor (DU.QuasicoherentCategory P) (DT.QuasicoherentCategory P)

The fully K-flat form of pullback on (Dqc): both the ambient derived functor and its restriction to the constructed component are obtained from the resolutions.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.kFlatBoundedPullback {S : Scheme} {X T U : SchemeBaseChange S} (DT : X.KFlatBaseChangeData T) (DU : X.KFlatBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (f : T ⟶ U) (hAcyclic : KFlatPullbackAcyclic DU.tensorResolution (X.baseChangeMap f)) (hQuasicoherent : KFlatResolvedPullbackPreservesQuasicoherentCohomology DU.tensorResolution (X.baseChangeMap f)) (hComponent : DT.toDerivedBaseChangeData.PullbackPreservesQuasicoherentComponent DU.toDerivedBaseChangeData P (DU.pullbackAlong f hAcyclic hQuasicoherent)) (hBounded : (DU.pullbackAlong f hAcyclic hQuasicoherent).PreservesBoundedCoherent) : CategoryTheory.Functor (DU.BoundedCategory P) (DT.BoundedCategory P)

The fully K-flat form of pullback on D: the bounded restriction is constructed from the same K-flat derived pullback used on (Dqc).

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackOfDetection {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hDetect : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))), DU.quasicoherentComponent P E ↔ DT.quasicoherentComponent P (pull.functor.obj E)) : CategoryTheory.Functor (DU.QuasicoherentCategory P) (DT.QuasicoherentCategory P)

Pullback on (Dqc) when membership in the source component is detected after ambient pullback. This is the form in which essential surjectivity descends from the ambient category.

Equations

• DT.quasicoherentPullbackOfDetection DU P pull hDetect = CategoryTheory.ObjectProperty.preimageLift pull.functor hDetect

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackOfDetection_essSurj {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hDetect : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))), DU.quasicoherentComponent P E ↔ DT.quasicoherentComponent P (pull.functor.obj E)) [pull.functor.EssSurj] : (DT.quasicoherentPullbackOfDetection DU P pull hDetect).EssSurj

Lemma 3.18's essential-surjectivity argument for the quasicoherent component: ambient essential surjectivity and detection of component membership imply essential surjectivity of the restricted pullback.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackOfDetection {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hBounded : pull.PreservesBoundedCoherent) (hDetect : ∀ (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), DU.boundedComponent P E ↔ DT.boundedComponent P ((pull.boundedFunctor hBounded).obj E)) : CategoryTheory.Functor (DU.BoundedCategory P) (DT.BoundedCategory P)

Pullback on D when bounded-component membership is detected after ambient bounded pullback.

Equations

• DT.boundedPullbackOfDetection DU P pull hBounded hDetect = CategoryTheory.ObjectProperty.preimageLift (pull.boundedFunctor hBounded) hDetect

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackOfDetection_essSurj {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hBounded : pull.PreservesBoundedCoherent) (hDetect : ∀ (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), DU.boundedComponent P E ↔ DT.boundedComponent P ((pull.boundedFunctor hBounded).obj E)) [(pull.boundedFunctor hBounded).EssSurj] : (DT.boundedPullbackOfDetection DU P pull hBounded hDetect).EssSurj

Lemma 3.18's essential-surjectivity argument for the bounded component.

Lemma 3.18: base change restricts an equivalence to the components

Essential surjectivity of the restricted pullback is above. Full faithfulness needs nothing about base change at all -- it restricts along a full-subcategory inclusion for free -- so once the ambient pullback is an equivalence, detection of component membership makes the restriction one too. The hypothesis is deliberately on the ambient functor: nothing here proves that any base-change pullback is an equivalence.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackOfDetection_faithful {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hDetect : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))), DU.quasicoherentComponent P E ↔ DT.quasicoherentComponent P (pull.functor.obj E)) [pull.functor.Faithful] : (DT.quasicoherentPullbackOfDetection DU P pull hDetect).Faithful

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackOfDetection_full {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hDetect : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))), DU.quasicoherentComponent P E ↔ DT.quasicoherentComponent P (pull.functor.obj E)) [pull.functor.Full] : (DT.quasicoherentPullbackOfDetection DU P pull hDetect).Full

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackOfDetectionEquivalence {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hDetect : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))), DU.quasicoherentComponent P E ↔ DT.quasicoherentComponent P (pull.functor.obj E)) [pull.functor.IsEquivalence] : DU.QuasicoherentCategory P ≌ DT.QuasicoherentCategory P

Lemma 3.18 for the quasicoherent base-change component: an ambient Dqc pullback that is an equivalence restricts to an equivalence (Dqc)_U ≌ (Dqc)_T along the detection of component membership.

Equations

• DT.quasicoherentPullbackOfDetectionEquivalence DU P pull hDetect = CategoryTheory.ObjectProperty.preimageLiftEquivalence pull.functor hDetect

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackOfDetection_faithful {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hBounded : pull.PreservesBoundedCoherent) (hDetect : ∀ (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), DU.boundedComponent P E ↔ DT.boundedComponent P ((pull.boundedFunctor hBounded).obj E)) [(pull.boundedFunctor hBounded).Faithful] : (DT.boundedPullbackOfDetection DU P pull hBounded hDetect).Faithful

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackOfDetection_full {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hBounded : pull.PreservesBoundedCoherent) (hDetect : ∀ (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), DU.boundedComponent P E ↔ DT.boundedComponent P ((pull.boundedFunctor hBounded).obj E)) [(pull.boundedFunctor hBounded).Full] : (DT.boundedPullbackOfDetection DU P pull hBounded hDetect).Full

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackOfDetectionEquivalence {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hBounded : pull.PreservesBoundedCoherent) (hDetect : ∀ (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), DU.boundedComponent P E ↔ DT.boundedComponent P ((pull.boundedFunctor hBounded).obj E)) [(pull.boundedFunctor hBounded).IsEquivalence] : DU.BoundedCategory P ≌ DT.BoundedCategory P

Lemma 3.18 for the bounded base-change component D_U ≌ D_T.

Equations

• DT.boundedPullbackOfDetectionEquivalence DU P pull hBounded hDetect = CategoryTheory.ObjectProperty.preimageLiftEquivalence (pull.boundedFunctor hBounded) hDetect