Coherent subobjects on an affine basic open

The coherent tilde subobject associated to a finite submodule is pulled back along the actual immersion D(r) ↪ Spec R. Its affine global sections, transported across basicOpenIsoSpecAway r, agree with the canonical localized submodule. This is a one-chart, underived statement; it does not glue subobjects over a union of opens.

noncomputable def AlgebraicGeometry.Coh.basicOpenGlobalSectionsIso {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 e := basicOpenIsoSpecAway r; have β := pullbackEquivalence e; have j := Scheme.Opens.ι (PrimeSpectrum.basicOpen r); have G := pullback j; have EA := affineEquivalence; have J := (ModuleCat.isFG A).ι; have Hloc := ModuleCat.localizedModuleFunctor (Submonoid.powers r); J.obj (EA.functor.obj (β.inverse.obj (G.obj E))) ≅ Hloc.obj M.obj

Transport global sections of the pullback of E on the actual basic open to Mathlib's canonical localization of its chosen finite-module presentation. The comparison factors through basicOpenIsoSpecAway r; it is not definitional.

Equations

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

noncomputable def AlgebraicGeometry.Coh.basicOpenCoherentSubobject {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 the coherent tilde inclusion for N ≤ M back to the actual basic open, then take affine global sections through basicOpenIsoSpecAway r. The target is transported to Mathlib's canonical localized-module carrier.

Equations

• AlgebraicGeometry.Coh.basicOpenCoherentSubobject r M E cR N hN = ↑(AlgebraicGeometry.Coh.basicOpenCoherentSubobjectData✝ r M E cR N hN)

theorem AlgebraicGeometry.Coh.basicOpenCoherentSubobject_eq_localizedSpectrum {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) : basicOpenCoherentSubobject r M E cR N hN = localizedSpectrumCoherentSubobject r M E cR N hN

The actual basic-open construction agrees with the localized-spectrum construction after transporting through basicOpenIsoSpecAway r.

theorem AlgebraicGeometry.Coh.basicOpenCoherentSubobject_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 (basicOpenCoherentSubobject r M E cR N hN) = Submodule.localized' (Localization.Away r) (Submonoid.powers r) (M.obj.localizedModuleMkLinearMap (Submonoid.powers r)) N

On the actual affine basic open D(r), the transported coherent subobject has underlying module exactly N.localized' inside canonical localization.