Module

QuasicoherentPushforward.lean

Nyll.SchemeTheory.Modules.QuasicoherentPushforward

3 declarations indexed from sourceView source ↗

Module documentation

Quasicoherent direct images for open and affine morphisms

The affine-target theorem is transported from the actual Spec theorem through isoSpec. The arbitrary-target theorem uses the actual open-restriction comparison on each affine target open, then the native affine-cover criterion.

Imports12

Nyll.SchemeTheory.Modules.PushforwardLocalization
Nyll.SchemeTheory.Modules.PushforwardRestrict
Nyll.SchemeTheory.Modules.QuasicoherentLocal
Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Imported by3

theorem

isQuasicoherent_pushforward_of_qcqs_toAffine

L38 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward_of_qcqs_toAffine

Documentation

The direct image of a quasicoherent module from a quasi-compact, quasi-separated source to an affine target is quasicoherent.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isQuasicoherent_pushforward_of_qcqs_toAffine
    {X Y : Scheme.{u}} [IsAffine Y] (j : X ⟶ Y)
    [CompactSpace X] [QuasiSeparatedSpace X] (M : X.Modules) [M.IsQuasicoherent] :
    ((pushforward j).obj M).IsQuasicoherent

theorem

isQuasicoherent_pushforward_of_quasiCompact_openImmersion

L60 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward_of_quasiCompact_openImmersion

Documentation

The actual direct image of a quasicoherent module under a quasi-compact open immersion is quasicoherent over an arbitrary target scheme.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isQuasicoherent_pushforward_of_quasiCompact_openImmersion
    {X Y : Scheme.{u}} (j : X ⟶ Y) [IsOpenImmersion j] [QuasiCompact j]
    (M : X.Modules) [M.IsQuasicoherent] :
    ((pushforward j).obj M).IsQuasicoherent

theorem

isQuasicoherent_pushforward_of_isAffineHom

L91 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pushforward_of_isAffineHom

Documentation

The actual direct image of a quasicoherent module along an affine morphism is quasicoherent, over an arbitrary target scheme.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isQuasicoherent_pushforward_of_isAffineHom
    {X Y : Scheme.{u}} (g : X ⟶ Y) [IsAffineHom g]
    (M : X.Modules) [M.IsQuasicoherent] :
    ((pushforward g).obj M).IsQuasicoherent

Module documentation

Quasicoherent direct images for open and affine morphisms

Declarations

isQuasicoherent_pushforward_of_qcqs_toAffine

isQuasicoherent_pushforward_of_quasiCompact_openImmersion

isQuasicoherent_pushforward_of_isAffineHom