Documentation

DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Affine.BasicOpenRestriction

Restricting a chosen coherent subobject between basic opens #

For a finite submodule N ≤ M, the coherent tilde inclusion on D(r) restricts to the same inclusion constructed directly on D(r * s). After affine global sections and explicit transport from Shrink to the raw localized-module carrier, its submodule is the span of the image under the canonical map M[1/r] → M[1/(r*s)]. This is a one-chart, underived statement for the chosen finite N; it neither classifies arbitrary subobjects nor glues a union.

source
noncomputable def AlgebraicGeometry.Coh.basicOpenChosenTildeSubobject {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 ((pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r))).obj E)

The actual coherent tilde inclusion for a chosen finite N ≤ M, pulled back from Spec R to the basic open D(r).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def AlgebraicGeometry.Coh.restrictBasicOpenSubobject {R : CommRingCat} [IsNoetherianRing ↑R] (a x : ↑R) (h : PrimeSpectrum.basicOpen x ≤ PrimeSpectrum.basicOpen a) (E : Coh (Spec R)) (S : CategoryTheory.Subobject ((pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen a))).obj E)) :
    CategoryTheory.Subobject ((pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen x))).obj E)

    Restrict a coherent subobject on D(a) along D(x) ⊆ D(a), using the pullback-composition isomorphism to place it on the canonical D(x) pullback.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AlgebraicGeometry.Coh.basicOpenSubobjectRawModule {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (M : FGModuleCat ↑R) (E : Coh (Spec R)) (cR : E ≅ FGModuleCat.affineTilde.obj M) (S : CategoryTheory.Subobject ((pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r))).obj E)) :
      Submodule (Localization.Away r) (LocalizedModule.Away r ↑M.obj)

      Transport a coherent subobject on the actual D(r) through the affine global-sections comparison and then explicitly to the raw M[1/r] carrier.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem AlgebraicGeometry.Coh.basicOpenChosenTildeSubobject_restrict_rawModule {R : CommRingCat} [IsNoetherianRing ↑R] (r s : ↑R) (M : FGModuleCat ↑R) (E : Coh (Spec R)) (cR : E ≅ FGModuleCat.affineTilde.obj M) (N : Submodule ↑R ↑M.obj) (hN : N.FG) :
        have h := ⋯; basicOpenSubobjectRawModule (r * s) M E cR (restrictBasicOpenSubobject r (r * s) h E (basicOpenChosenTildeSubobject r M E cR N hN)) = Submodule.span (Localization.Away (r * s)) (⇑(LocalizedModule.awayToAwayRightLinearMap r s) '' ↑(basicOpenSubobjectRawModule r M E cR (basicOpenChosenTildeSubobject r M E cR N hN)))

        The chosen finite tilde subobject, restricted from D(r) to D(r*s), has raw affine-global-sections submodule equal to the span of the image of its D(r) submodule under the canonical nested-localization map.