Affine coherent localization

This file transfers fixed-target arrows, zero-composite three-term diagrams, and finite-window complex-object descent to coherent sheaves on affine noetherian schemes. These concern ordinary coherent pullback, not derived arrows, bounded components, or an arbitrary t-heart.

noncomputable def AlgebraicGeometry.Coh.finiteExtendScalars {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : CategoryTheory.Functor (FGModuleCat R) (FGModuleCat A)

Extension of scalars restricted to finite modules. This is defined for any ring map; flatness is only needed when subsequently passing to derived categories.

Equations

• AlgebraicGeometry.Coh.finiteExtendScalars = (ModuleCat.isFG A).lift ((ModuleCat.isFG R).ι.comp (ModuleCat.extendScalars (algebraMap R A))) ⋯

noncomputable def AlgebraicGeometry.Coh.affineTildePullbackIso {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] [IsNoetherianRing A] : FGModuleCat.affineTilde.comp (pullback (Spec.map AlgebraicGeometry.Coh.ringMap✝)) ≅ finiteExtendScalars.comp FGModuleCat.affineTilde

Affine sheafification commutes with coherent pullback after finite-module extension of scalars. This is an isomorphism of ordinary functors.

Equations

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

theorem AlgebraicGeometry.Coh.fixedTargetArrowExtension_pullbackSpecMap_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] (S : Submonoid R) [IsLocalization S A] (E : Coh (Spec (CommRingCat.of R))) : CategoryTheory.Subobject.FixedTargetArrowExtension (pullback (Spec.map (CommRingCat.ofHom (algebraMap R A)))) E

Fixed-target arrow extension for coherent sheaves on an affine noetherian localization. The target sheaf remains fixed; only the arrow's domain is replaced by an isomorphic pullback. This is an underived statement about Coh.pullback.

theorem AlgebraicGeometry.Coh.exists_fixedTerminalThreeTerm_pullbackSpecMap_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] (S : Submonoid R) [IsLocalization S A] (E : Coh (Spec (CommRingCat.of R))) (N₀ N₁ : Coh (Spec (CommRingCat.of A))) (d : N₀ ⟶ N₁) (β : N₁ ⟶ (pullback (Spec.map (CommRingCat.ofHom (algebraMap R A)))).obj E) (hz : CategoryTheory.CategoryStruct.comp d β = 0) : ∃ (L₀ : Coh (Spec (CommRingCat.of R))) (L₁ : Coh (Spec (CommRingCat.of R))) (d₀ : L₀ ⟶ L₁) (f : L₁ ⟶ E) (e₀ : N₀ ≅ (pullback (Spec.map (CommRingCat.ofHom (algebraMap R A)))).obj L₀) (e₁ : N₁ ≅ (pullback (Spec.map (CommRingCat.ofHom (algebraMap R A)))).obj L₁), CategoryTheory.CategoryStruct.comp d₀ f = 0 ∧ CategoryTheory.CategoryStruct.comp d e₁.hom = CategoryTheory.CategoryStruct.comp e₀.hom ((pullback (Spec.map (CommRingCat.ofHom (algebraMap R A)))).map d₀) ∧ β = CategoryTheory.CategoryStruct.comp e₁.hom ((pullback (Spec.map (CommRingCat.ofHom (algebraMap R A)))).map f)

A zero-composite three-term diagram of coherent sheaves over an affine noetherian localization descends with its terminal coherent sheaf E fixed. Both arrows agree with ordinary coherent pullback through the displayed isomorphisms. This is underived.

theorem AlgebraicGeometry.Coh.exists_finite_window_complex_model_pullbackSpecMap_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] (S : Submonoid R) [IsLocalization S A] (lo hi : ℤ) (K : CochainComplex (Coh (Spec (CommRingCat.of A))) ℤ) [K.IsStrictlyGE lo] [K.IsStrictlyLE hi] : ∃ (L : CochainComplex (Coh (Spec (CommRingCat.of R))) ℤ), L.IsStrictlyGE lo ∧ L.IsStrictlyLE hi ∧ Nonempty (K ≅ ((pullback (Spec.map (CommRingCat.ofHom (algebraMap R A)))).mapHomologicalComplex (ComplexShape.up ℤ)).obj L)

A strictly finite-window complex of coherent sheaves on an affine localization has a strictly finite-window coherent model on the base affine scheme. The isomorphism is one of ordinary complexes under termwise coherent pullback, not a derived or component-level descent statement.