Proves localization of pushforward sections for a quasicoherent module along a quasi-compact open immersion into an affine scheme. This gives quasicoherence of the direct image.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulesdef sourceRing (X : Scheme.{u}) : CommRingCat.{u}Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulesdef sourceCoefficient {R : CommRingCat.{u}} {X : Scheme.{u}}
(j : X ⟶ Spec R) : R →+* sourceRing XSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulesdef sourceBasicOpen {R : CommRingCat.{u}} {X : Scheme.{u}}
(σ : R →+* sourceRing X) (r : R) : X.OpensSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulesdef sourceModuleOver {R : CommRingCat.{u}} {X : Scheme.{u}}
(M : X.Modules) (σ : R →+* sourceRing X) : X.Opensᵒᵖ ⥤ ModuleCat.{u} RSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulestheorem sourceModuleOver_localizes {R : CommRingCat.{u}} {X : Scheme.{u}}
(M : X.Modules) [M.IsQuasicoherent] [CompactSpace X] [QuasiSeparatedSpace X]
(σ : R →+* sourceRing X) (r : R) (W : X.Opens) (hW : W = sourceBasicOpen σ r) :
IsLocalizedModule (Submonoid.powers r) ((sourceModuleOver M σ).map W.leTop.op).homSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Moduleslemma sourceBasicOpen_eq_preimage {R : CommRingCat.{u}} {X : Scheme.{u}}
(j : X ⟶ Spec R) (r : R) :
j.sectionComparisonOpen (PrimeSpectrum.basicOpen r) = sourceBasicOpen (sourceCoefficient j) rThe already computed source presheaf is a sheaf by its actual comparison with the pushforward.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulesdef sourceSheafOnTarget {R : CommRingCat.{u}} {X : Scheme.{u}}
(j : X ⟶ Spec R) (M : X.Modules) : TopCat.Sheaf (ModuleCat.{u} R) (Spec R) where
obj := sourceModuleOnTarget j M
property := TopCat.Presheaf.isSheaf_of_iso (pushforwardModulePresheafIso j M)
(modulesSpecToSheaf.obj ((pushforward j).obj M)).propertySurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulesdef sourceSheafIso {R : CommRingCat.{u}} {X : Scheme.{u}}
(j : X ⟶ Spec R) (M : X.Modules) :
modulesSpecToSheaf.obj ((pushforward j).obj M) ≅ sourceSheafOnTarget j MSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulestheorem sourceSheaf_isLocalizing {R : CommRingCat.{u}} {X : Scheme.{u}}
(j : X ⟶ Spec R) (M : X.Modules) [M.IsQuasicoherent]
[CompactSpace X] [QuasiSeparatedSpace X] : IsLocalizing (sourceSheafOnTarget j M)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulestheorem isLocalizing_pushforward_of_qcqs {R : CommRingCat.{u}} {X : Scheme.{u}}
(j : X ⟶ Spec R) (M : X.Modules) [M.IsQuasicoherent]
[CompactSpace X] [QuasiSeparatedSpace X] :
IsLocalizing (modulesSpecToSheaf.obj ((pushforward j).obj M))Quasicoherent modules on a quasi-compact open subscheme of an affine scheme have genuinely localizing pushforward sections over the base ring.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulestheorem isLocalizing_pushforward_of_quasiCompact_openImmersion_toSpec
{R : CommRingCat.{u}} {X : Scheme.{u}} (j : X ⟶ Spec R)
[IsOpenImmersion j] [QuasiCompact j] (M : X.Modules) [M.IsQuasicoherent] :
IsLocalizing (modulesSpecToSheaf.obj ((pushforward j).obj M))Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulestheorem isQuasicoherent_of_isLocalizing {R : CommRingCat.{u}}
(N : (Spec R).Modules) (hN : IsLocalizing (modulesSpecToSheaf.obj N)) :
N.IsQuasicoherentThe actual direct image of a quasicoherent module from a quasi-compact, quasi-separated scheme to Spec R is quasicoherent.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulestheorem isQuasicoherent_pushforward_of_qcqs_toSpec
{R : CommRingCat.{u}} {X : Scheme.{u}} (g : X ⟶ Spec R)
[CompactSpace X] [QuasiSeparatedSpace X] (M : X.Modules) [M.IsQuasicoherent] :
((pushforward g).obj M).IsQuasicoherentThe actual direct image of a quasicoherent module along a quasi-compact open immersion into an affine scheme is quasicoherent.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modulestheorem isQuasicoherent_pushforward_of_quasiCompact_openImmersion_toSpec
{R : CommRingCat.{u}} {X : Scheme.{u}} (j : X ⟶ Spec R)
[IsOpenImmersion j] [QuasiCompact j] (M : X.Modules) [M.IsQuasicoherent] :
((pushforward j).obj M).IsQuasicoherent