Coherent subobjects after localization on an affine spectrum

For a finitely generated submodule of the affine global sections of a coherent sheaf, the corresponding coherent tilde monomorphism pulls back to the subobject given by localizing that submodule. The comparison is on Spec (Localization.Away r). The canonical Localization.Away r-module is Mathlib's localizedModuleFunctor carrier, not definitionally the sections of the pulled-back sheaf; the natural isomorphism below performs that transport explicitly.

This file asserts nothing about the actual basic open D(r), unions of opens, derived Hom, or Theorem 5.7(2).

noncomputable def AlgebraicGeometry.Coh.localizedSpectrumGlobalSectionsNatIso {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) : let A := Localization.Away r; have k := Spec.map (CommRingCat.ofHom (algebraMap (↑R) A)); have FR := FGModuleCat.affineTilde; have F := pullback k; have EA := affineEquivalence; have J := (ModuleCat.isFG A).ι; have H := ModuleCat.localizedModuleFunctor (Submonoid.powers r); ((FR.comp F).comp EA.functor).comp J ≅ (ModuleCat.isFG ↑R).ι.comp H

Affine global sections of coherent pullback to the localized spectrum agree naturally with canonical localization of the original finite module. The factors are affineTildePullbackIso, the affine-equivalence counit, and ModuleCat.extendScalarsLocalizationNatIso; none is treated as definitional.

Equations

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

noncomputable def AlgebraicGeometry.Coh.localizedSpectrumGlobalSectionsIso {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (M : FGModuleCat ↑R) (E : Coh (Spec R)) (cR : E ≅ FGModuleCat.affineTilde.obj M) : let A := Localization.Away r; have k := Spec.map (CommRingCat.ofHom (algebraMap (↑R) A)); have F := pullback k; have EA := affineEquivalence; have J := (ModuleCat.isFG A).ι; have H := ModuleCat.localizedModuleFunctor (Submonoid.powers r); J.obj (EA.functor.obj (F.obj E)) ≅ H.obj M.obj

Transport affine global sections of the pullback of E to the canonical localization of M. For M = Γ(E), take cR to be the affine-equivalence unit. The isomorphism cR is retained explicitly to avoid conflating the two module actions on global sections.

Equations

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

noncomputable def AlgebraicGeometry.Coh.coherentTildeSubobject {R : CommRingCat} [IsNoetherianRing ↑R] (M : FGModuleCat ↑R) (E : Coh (Spec R)) (cR : E ≅ FGModuleCat.affineTilde.obj M) (N : Submodule ↑R ↑M.obj) (hN : N.FG) : CategoryTheory.Subobject E

The coherent tilde monomorphism associated to a finite submodule of the module presenting E. In the canonical case M = Γ(E), cR is the unit of the affine coherent equivalence.

Equations

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

noncomputable def AlgebraicGeometry.Coh.localizedSpectrumSubobject {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (M : FGModuleCat ↑R) (N : Submodule ↑R ↑M.obj) (hN : N.FG) : CategoryTheory.Subobject ((ModuleCat.localizedModuleFunctor (Submonoid.powers r)).obj M.obj)

The subobject of the canonical localized module obtained by pulling back the coherent tilde inclusion of a finite submodule and transporting global sections along localizedSpectrumGlobalSectionsNatIso.

Equations

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

theorem AlgebraicGeometry.Coh.localizedSpectrumSubobject_subobjectModule {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (M : FGModuleCat ↑R) (N : Submodule ↑R ↑M.obj) (hN : N.FG) : ((ModuleCat.localizedModuleFunctor (Submonoid.powers r)).obj M.obj).subobjectModule (localizedSpectrumSubobject r M N hN) = Submodule.localized' (Localization.Away r) (Submonoid.powers r) (M.obj.localizedModuleMkLinearMap (Submonoid.powers r)) N

The transported pullback of the coherent tilde subobject has precisely the localized finite submodule as its underlying submodule. The target module is the canonical localized-module carrier, with transport through κ explicit in localizedSpectrumSubobject.

noncomputable def AlgebraicGeometry.Coh.localizedSpectrumCoherentSubobject {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (M : FGModuleCat ↑R) (E : Coh (Spec R)) (cR : E ≅ FGModuleCat.affineTilde.obj M) (N : Submodule ↑R ↑M.obj) (hN : N.FG) : CategoryTheory.Subobject ((ModuleCat.localizedModuleFunctor (Submonoid.powers r)).obj M.obj)

Pull back the coherent tilde inclusion into E, take affine global sections, and transport its target along the explicit localized-spectrum comparison. This is a subobject of the canonical localized module, not an identification of the two carrier types.

Equations

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

theorem AlgebraicGeometry.Coh.localizedSpectrumCoherentSubobject_subobjectModule {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (M : FGModuleCat ↑R) (E : Coh (Spec R)) (cR : E ≅ FGModuleCat.affineTilde.obj M) (N : Submodule ↑R ↑M.obj) (hN : N.FG) : ((ModuleCat.localizedModuleFunctor (Submonoid.powers r)).obj M.obj).subobjectModule (localizedSpectrumCoherentSubobject r M E cR N hN) = Submodule.localized' (Localization.Away r) (Submonoid.powers r) (M.obj.localizedModuleMkLinearMap (Submonoid.powers r)) N

On the localized spectrum, the subobject obtained from the coherent inclusion into E is exactly N.localized' after transporting the target along localizedSpectrumGlobalSectionsIso. This is not a statement on the actual basic open D(r).

theorem AlgebraicGeometry.Coh.localizedSpectrumCoherentSubobject_globalSections {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (E : Coh (Spec R)) : let M := affineEquivalence.functor.obj E; ∀ (N : Submodule ↑R ↑M.obj) (hN : N.FG), ((ModuleCat.localizedModuleFunctor (Submonoid.powers r)).obj M.obj).subobjectModule (localizedSpectrumCoherentSubobject r M E (affineEquivalence.unitIso.app E) N hN) = Submodule.localized' (Localization.Away r) (Submonoid.powers r) (M.obj.localizedModuleMkLinearMap (Submonoid.powers r)) N

Canonical M = Γ(E) specialization of the localized-spectrum coherent subobject comparison. The affine-equivalence unit supplies cR; no equality of the two global-sections module actions is assumed.