Derived pullback along an affine localization

For a localization R → A, restriction of scalars followed by extension of scalars is naturally isomorphic to the identity on A-modules. Flatness of localizations therefore lets this counit descend to derived categories and exhibits derived extension of scalars as essentially surjective.

This is the algebraic affine-localization input for the essential-surjectivity part of the base-change construction. The module and quasi-coherent functors are compared here with the general exact affine pullback, including the pullback--restriction adjunction on unbounded and bounded derived categories.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationExtendRestrictCounitApp_isIso {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] (N : ModuleCat A) : CategoryTheory.IsIso ((ModuleCat.ExtendRestrictScalarsAdj.counit (algebraMap R A)).app N)

For a localization R → A, the extension--restriction counit is an isomorphism on every A-module.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationExtendRestrictCounitIso {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (ModuleCat.restrictScalars (algebraMap R A)).comp (ModuleCat.extendScalars (algebraMap R A)) ≅ CategoryTheory.Functor.id (ModuleCat A)

The extension--restriction counit for a localization, bundled as a natural isomorphism of module functors.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationExtendRestrictCounitIso M = CategoryTheory.asIso (ModuleCat.ExtendRestrictScalarsAdj.counit (algebraMap R A))

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationExtendScalars_additive {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : (ModuleCat.extendScalars (algebraMap R A)).Additive

Additivity data for extension of scalars, with universes fixed for the localization-derived construction.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationAlgebraMap_flat {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (algebraMap R A).Flat

The algebra map of a localization is flat.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationExtendScalars_preservesFiniteLimits {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.extendScalars (algebraMap R A))

Extension of scalars along a localization preserves finite limits.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedPullback {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : CategoryTheory.Functor (DerivedCategory (ModuleCat R)) (DerivedCategory (ModuleCat A))

Exact derived extension of scalars along a localization.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedPullback M = (ModuleCat.extendScalars (algebraMap R A)).mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedPullbackComparison {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineLocalizationDerivedPullback M ≅ affineExtendScalarsDerived (CommRingCat.ofHom (algebraMap R A)) ⋯

The localization-specific derived pullback is the general exact derived extension-of-scalars functor specialized to the flat localization map.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedPullbackComparison M = CategoryTheory.Iso.refl (AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedPullback M)

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedRestriction {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : CategoryTheory.Functor (DerivedCategory (ModuleCat A)) (DerivedCategory (ModuleCat R))

Exact derived restriction of scalars. It supplies an explicit preimage for essential surjectivity of localization pullback.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedRestriction = (ModuleCat.restrictScalars (algebraMap R A)).mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedCounitIso {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineLocalizationDerivedRestriction.comp (affineLocalizationDerivedPullback M) ≅ CategoryTheory.Functor.id (DerivedCategory (ModuleCat A))

On derived module categories, restriction followed by localization pullback is naturally isomorphic to the identity.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedPullback_essSurj {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineLocalizationDerivedPullback M).EssSurj

Derived extension of scalars along a localization is essentially surjective.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedPullback_bounded {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] (E : DerivedCategory (ModuleCat R)) (hE : DerivedCategory.TStructure.t.bounded E) : DerivedCategory.TStructure.t.bounded ((affineLocalizationDerivedPullback M).obj E)

Derived localization pullback preserves cohomologically bounded objects.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationDerivedRestriction_bounded {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (E : DerivedCategory (ModuleCat A)) (hE : DerivedCategory.TStructure.t.bounded E) : DerivedCategory.TStructure.t.bounded (affineLocalizationDerivedRestriction.obj E)

Derived restriction of scalars preserves cohomologically bounded objects.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationBoundedDerivedPullback {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : CategoryTheory.Functor (DerivedCategory.Bounded (ModuleCat R)) (DerivedCategory.Bounded (ModuleCat A))

Exact derived localization pullback restricted to cohomologically bounded derived categories.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationBoundedDerivedRestriction {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : CategoryTheory.Functor (DerivedCategory.Bounded (ModuleCat A)) (DerivedCategory.Bounded (ModuleCat R))

Exact derived restriction of scalars restricted to cohomologically bounded derived categories.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationBoundedDerivedPullbackCompInclusion {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineLocalizationBoundedDerivedPullback M).comp DerivedCategory.Bounded.ι ≅ DerivedCategory.Bounded.ι.comp (affineLocalizationDerivedPullback M)

Forgetting boundedness recovers derived localization pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationBoundedDerivedRestrictionCompInclusion {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : affineLocalizationBoundedDerivedRestriction.comp DerivedCategory.Bounded.ι ≅ DerivedCategory.Bounded.ι.comp affineLocalizationDerivedRestriction

Forgetting boundedness recovers derived restriction of scalars.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationBoundedDerivedCounitIso {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineLocalizationBoundedDerivedRestriction.comp (affineLocalizationBoundedDerivedPullback M) ≅ CategoryTheory.Functor.id (DerivedCategory.Bounded (ModuleCat A))

On bounded derived module categories, restriction followed by localization pullback is naturally isomorphic to the identity.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.affineLocalizationBoundedDerivedPullback_essSurj {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineLocalizationBoundedDerivedPullback M).EssSurj

Derived extension of scalars along a localization is essentially surjective on cohomologically bounded derived categories.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullback {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : CategoryTheory.Functor (AffineQuasicoherentBoundedDerivedCategory (CommRingCat.of R)) (AffineQuasicoherentBoundedDerivedCategory (CommRingCat.of A))

Transport bounded localization pullback to the genuine bounded derived categories of quasi-coherent sheaves on affine spectra.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationRestriction {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : CategoryTheory.Functor (AffineQuasicoherentBoundedDerivedCategory (CommRingCat.of A)) (AffineQuasicoherentBoundedDerivedCategory (CommRingCat.of R))

Transport bounded restriction of scalars to the genuine bounded derived categories of affine quasi-coherent sheaves.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationCounitIso {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineQuasicoherentBoundedLocalizationRestriction.comp (affineQuasicoherentBoundedLocalizationPullback M) ≅ CategoryTheory.Functor.id (AffineQuasicoherentBoundedDerivedCategory (CommRingCat.of A))

On bounded affine quasi-coherent derived categories, transported restriction followed by localization pullback is naturally isomorphic to the identity.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullback_essSurj {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentBoundedLocalizationPullback M).EssSurj

Localization pullback is essentially surjective on bounded affine quasi-coherent derived categories.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullbackToDqc {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : CategoryTheory.Functor (AffineQuasicoherentBoundedDerivedCategory (CommRingCat.of R)) (SchemeBoundedQuasicoherentDerivedCategory (Spec (CommRingCat.of A)))

Bounded affine localization pullback followed by realization into the intrinsic bounded target Dqc category.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullbackToDqc_essSurj {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentBoundedLocalizationPullbackToDqc M).EssSurj

Bounded localization pullback reaches every object of the intrinsic bounded target Dqc category.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullbackToDqc_essImage {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentBoundedLocalizationPullbackToDqc M).essImage = (affineQuasicoherentBoundedDerivedToDqc (CommRingCat.of A)).essImage

Bounded localization pullback and bounded affine realization have the same essential image; both now reach the entire intrinsic bounded target Dqc category.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationPullback {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory (CommRingCat.of R)) (AffineQuasicoherentDerivedCategory (CommRingCat.of A))

Transport localization pullback from derived module categories to the genuine derived categories of quasi-coherent sheaves on affine spectra.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationRestriction {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory (CommRingCat.of A)) (AffineQuasicoherentDerivedCategory (CommRingCat.of R))

Transport restriction of scalars to affine quasi-coherent derived categories.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationPullbackComparison {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineQuasicoherentDerivedPullback (CommRingCat.ofHom (algebraMap R A)) ⋯ ≅ affineQuasicoherentLocalizationPullback M

The general geometric affine pullback specializes to the previously constructed transported localization pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationRestrictionComparison {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : affineQuasicoherentDerivedPushforward (CommRingCat.ofHom (algebraMap R A)) ≅ affineQuasicoherentLocalizationRestriction

For the affine localization morphism, geometric derived pushforward is the transported restriction-of-scalars functor.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationPullbackRestrictionAdjunction {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineQuasicoherentLocalizationPullback M ⊣ affineQuasicoherentLocalizationRestriction

The geometric affine pullback--pushforward adjunction specializes to the transported localization pullback and restriction functors.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationCounitIso {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineQuasicoherentLocalizationRestriction.comp (affineQuasicoherentLocalizationPullback M) ≅ CategoryTheory.Functor.id (AffineQuasicoherentDerivedCategory (CommRingCat.of A))

On affine quasi-coherent derived categories, transported restriction followed by localization pullback is naturally isomorphic to the identity.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationGeometricCounitIso {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentDerivedPushforward (CommRingCat.ofHom (algebraMap R A))).comp (affineQuasicoherentLocalizationPullback M) ≅ CategoryTheory.Functor.id (AffineQuasicoherentDerivedCategory (CommRingCat.of A))

Geometric affine pushforward followed by localization pullback is the identity on the target affine quasi-coherent derived category.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullbackCompInclusion {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentBoundedLocalizationPullback M).comp DerivedCategory.Bounded.ι ≅ DerivedCategory.Bounded.ι.comp (affineQuasicoherentLocalizationPullback M)

Forgetting boundedness recovers transported affine localization pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationRestrictionCompInclusion {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : affineQuasicoherentBoundedLocalizationRestriction.comp DerivedCategory.Bounded.ι ≅ DerivedCategory.Bounded.ι.comp affineQuasicoherentLocalizationRestriction

Forgetting boundedness recovers transported affine restriction of scalars.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullbackComparison {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineQuasicoherentBoundedDerivedPullback (CommRingCat.ofHom (algebraMap R A)) ⋯ ≅ affineQuasicoherentBoundedLocalizationPullback M

The bounded general geometric affine pullback specializes to the bounded transported localization pullback.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPullback_essSurj_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentBoundedDerivedPullback (CommRingCat.ofHom (algebraMap R A)) ⋯).EssSurj

The canonical exact bounded affine pullback is essentially surjective when the ring map is a localization.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPullbackToDqc_essSurj_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentBoundedDerivedPullbackToDqc (CommRingCat.ofHom (algebraMap R A)) ⋯).EssSurj

The canonical exact bounded affine pullback along a localization reaches every object of the intrinsic bounded target Dqc category.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPullbackToDqc_essImage_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentBoundedDerivedPullbackToDqc (CommRingCat.ofHom (algebraMap R A)) ⋯).essImage = (affineQuasicoherentBoundedDerivedToDqc (CommRingCat.of A)).essImage

The bounded affine-localization specialization of the essential-image conclusion; both sides are the entire intrinsic bounded target Dqc category.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullbackToDqcComparison {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineQuasicoherentBoundedDerivedPullbackToDqc (CommRingCat.ofHom (algebraMap R A)) ⋯ ≅ affineQuasicoherentBoundedLocalizationPullbackToDqc M

Realizing the general bounded affine pullback along a localization agrees with the earlier transported localization realization.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationRestrictionComparison {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : affineQuasicoherentBoundedDerivedPushforward (CommRingCat.ofHom (algebraMap R A)) ≅ affineQuasicoherentBoundedLocalizationRestriction

For the affine localization morphism, bounded geometric derived pushforward is the transported bounded restriction-of-scalars functor.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationPullbackRestrictionAdjunction {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineQuasicoherentBoundedLocalizationPullback M ⊣ affineQuasicoherentBoundedLocalizationRestriction

The bounded geometric affine pullback--pushforward adjunction specializes to the bounded localization pullback and restriction functors.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedLocalizationGeometricCounitIso {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentBoundedDerivedPushforward (CommRingCat.ofHom (algebraMap R A))).comp (affineQuasicoherentBoundedLocalizationPullback M) ≅ CategoryTheory.Functor.id (AffineQuasicoherentBoundedDerivedCategory (CommRingCat.of A))

Bounded geometric affine pushforward followed by bounded localization pullback is naturally isomorphic to the identity.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationPullback_essSurj {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentLocalizationPullback M).EssSurj

Localization pullback is essentially surjective on the genuine affine quasi-coherent derived categories.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullback_essSurj_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentDerivedPullback (CommRingCat.ofHom (algebraMap R A)) ⋯).EssSurj

The canonical exact affine pullback is essentially surjective when the ring map is a localization.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullbackToDqc_essImage_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentDerivedPullbackToDqc (CommRingCat.ofHom (algebraMap R A)) ⋯).essImage = (affineQuasicoherentDerivedToDqc (CommRingCat.of A)).essImage

The affine-localization specialization of the essential-image conclusion: canonical exact pullback reaches every intrinsic target object currently covered by affine realization.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationPullbackToDqc {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory (CommRingCat.of R)) (SchemeQuasicoherentDerivedCategory (Spec (CommRingCat.of A)))

Affine localization pullback followed by the concrete realization into the target Dqc category.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationPullbackToDqcComparison {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : affineQuasicoherentDerivedPullbackToDqc (CommRingCat.ofHom (algebraMap R A)) ⋯ ≅ affineQuasicoherentLocalizationPullbackToDqc M

Realizing the general affine pullback along a localization agrees with the earlier transported localization realization.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationPullbackToDqc_essSurj_of_identification {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] (I : AffineQuasicoherentDqcIdentification (CommRingCat.of A)) : (affineQuasicoherentLocalizationPullbackToDqc M).EssSurj

If the unbounded affine Dqc identification is available for the target ring, then localization pullback reaches every object of the unbounded intrinsic target Dqc category.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullbackToDqc_essSurj_of_isLocalization_of_identification {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] (I : AffineQuasicoherentDqcIdentification (CommRingCat.of A)) : (affineQuasicoherentDerivedPullbackToDqc (CommRingCat.ofHom (algebraMap R A)) ⋯).EssSurj

Under the target unbounded affine identification, the canonical exact affine pullback along a localization reaches every object of the unbounded intrinsic target Dqc category.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentLocalizationPullbackToDqc_essImage {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] : (affineQuasicoherentLocalizationPullbackToDqc M).essImage = (affineQuasicoherentDerivedToDqc (CommRingCat.of A)).essImage

Localization pullback reaches exactly all target Dqc objects covered by the currently available affine realization. Upgrading this equality to essential surjectivity onto the full unbounded Dqc category is precisely the missing affine-realization input.