Affine derived pullback from K-projective complexes

This file applies the generic K-projective derived-functor API to extension of scalars along an arbitrary morphism of commutative rings. No flatness hypothesis is imposed.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineExtendScalars_additive {R A : CommRingCat} (f : R ⟶ A) : (ModuleCat.extendScalars (CommRingCat.Hom.hom f)).Additive

Extension of scalars is additive.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectivePullback {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.Functor (CategoryTheory.KProjectiveHomotopyCategory (ModuleCat ↑R)) (DerivedCategory (ModuleCat ↑A))

Arbitrary extension of scalars on affine K-projective representatives.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectivePullback f = CategoryTheory.kProjectiveDerivedFunctor (ModuleCat.extendScalars (CommRingCat.Hom.hom f))

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectiveDerivedPullback {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.Functor (CategoryTheory.KProjectiveDerivedCategory (ModuleCat ↑R)) (DerivedCategory (ModuleCat ↑A))

Arbitrary affine derived pullback on the full K-projective derived locus.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectiveDerivedPullback f = CategoryTheory.kProjectiveLocusDerivedFunctor (ModuleCat.extendScalars (CommRingCat.Hom.hom f))

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectiveDerivedPullbackComparison {R A : CommRingCat} (f : R ⟶ A) : (CategoryTheory.kProjectiveQhEquivalence (ModuleCat ↑R)).functor.comp (affineKProjectiveDerivedPullback f) ≅ affineKProjectivePullback f

The derived-locus construction agrees with extension of scalars on actual K-projective representatives.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectiveDerivedPullbackComparison f = CategoryTheory.kProjectiveLocusDerivedComparison (ModuleCat.extendScalars (CommRingCat.Hom.hom f))

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectiveSchemeModulePullbackComparison {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.kProjectiveLocusDerivedFunctor ((tilde.functor R).comp (Scheme.Modules.pullback (Spec.map f))) ≅ (affineKProjectiveDerivedPullback f).comp (tilde.functor A).mapDerivedCategory

On the affine K-projective derived locus, actual pullback of the sheafified representatives agrees after localization with scalar extension followed by the derived functor of the target affine tilde functor. The target is the derived category of all scheme-module sheaves on Spec A, not only the quasi-coherent subcategory.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectivePullbackObjIso {R A : CommRingCat} (f : R ⟶ A) (K : CochainComplex (ModuleCat ↑R) ℤ) (d : ℤ) [K.IsStrictlyLE d] [∀ (n : ℤ), CategoryTheory.Projective (K.X n)] : (affineKProjectivePullback f).obj (CategoryTheory.KProjectiveHomotopyCategory.ofBoundedAboveProjectives K d) ≅ DerivedCategory.Q.obj (((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K)

A bounded-above complex of projective R-modules computes arbitrary affine derived pullback by degreewise extension of scalars.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineKProjectivePullbackObjIso f K d = CategoryTheory.kProjectiveDerivedFunctorObjIso (ModuleCat.extendScalars (CommRingCat.Hom.hom f)) K d

theorem AlgebraicGeometry.DerivedCategory.Dqc.quasiIso_extendScalars_map_of_isKProjective {R A : CommRingCat} (f : R ⟶ A) {K L : CochainComplex (ModuleCat ↑R) ℤ} [K.IsKProjective] [L.IsKProjective] {g : K ⟶ L} (hg : HomologicalComplex.quasiIso (ModuleCat ↑R) (ComplexShape.up ℤ) g) : HomologicalComplex.quasiIso (ModuleCat ↑A) (ComplexShape.up ℤ) (((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).mapHomologicalComplex (ComplexShape.up ℤ)).map g)

Extension of scalars along an arbitrary morphism of commutative rings carries a quasi-isomorphism between K-projective complexes to a quasi-isomorphism.

The ring map carries no flatness hypothesis: a quasi-isomorphism between K-projective complexes is a homotopy equivalence, and extension of scalars is additive.

theorem AlgebraicGeometry.DerivedCategory.Dqc.quasiIso_extendScalars_map_of_projective {R A : CommRingCat} (f : R ⟶ A) {K L : CochainComplex (ModuleCat ↑R) ℤ} (dK dL : ℤ) [K.IsStrictlyLE dK] [L.IsStrictlyLE dL] [∀ (n : ℤ), CategoryTheory.Projective (K.X n)] [∀ (n : ℤ), CategoryTheory.Projective (L.X n)] {g : K ⟶ L} (hg : HomologicalComplex.quasiIso (ModuleCat ↑R) (ComplexShape.up ℤ) g) : HomologicalComplex.quasiIso (ModuleCat ↑A) (ComplexShape.up ℤ) (((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).mapHomologicalComplex (ComplexShape.up ℤ)).map g)

The inhabited form of quasiIso_extendScalars_map_of_isKProjective.

Bounded-above complexes of projective modules are K-projective and exist in abundance over any ring, so this is the statement an affine consumer of arbitrary derived pullback can actually apply.