Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Families.AffineCoherentLocalizationComparison

Exact affine coherent localization comparison #

On noetherian affine schemes, localization is flat, so coherent pullback and finite-module extension of scalars are exact. This file derives the ordinary affine sheafification/pullback natural isomorphism and records its naturality. It does not assert localization of derived Hom groups, bounded-component compatibility, or descent in a chosen heart.

source
noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.finiteAffineTildeDerived (B : CommRingCat) [IsNoetherianRing ↑B] :
CategoryTheory.Functor (DerivedCategory (FGModuleCat ↑B)) (DerivedCategory (Coh (Spec B)))

Exact derived affine sheafification on finitely generated modules over a noetherian ring.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.coherentLocalizationDerivedPullback {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] (S : Submonoid R) [IsLocalization S A] :
    CategoryTheory.Functor (DerivedCategory (Coh (Spec (CommRingCat.of R)))) (DerivedCategory (Coh (Spec (CommRingCat.of A))))

    Exact derived coherent pullback along an affine localization. The target ring is noetherian because it is a localization of the noetherian source.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.finiteExtendScalarsDerived {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] (S : Submonoid R) [IsLocalization S A] :
      CategoryTheory.Functor (DerivedCategory (FGModuleCat R)) (DerivedCategory (FGModuleCat A))

      Exact derived extension of scalars on finite modules along an affine localization. Finite terms remain finite under base change.

      Equations
      Instances For
        source
        noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.affineCoherentLocalizationDerivedComparison {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] (S : Submonoid R) [IsLocalization S A] :
        (finiteAffineTildeDerived (CommRingCat.of R)).comp (coherentLocalizationDerivedPullback S) ≅ (finiteExtendScalarsDerived S).comp (finiteAffineTildeDerived (CommRingCat.of A))

        Derived affine sheafification identifies finite-module localization with coherent derived pullback. The isomorphism is natural in the derived finite module complex.

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