Module

QuasicoherentCoprod.lean

Nyll.SchemeTheory.Modules.QuasicoherentCoprod

4 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence of actual binary coproducts

On each affine chart the tilde adjunction carries the coproduct of the two section modules to the actual sheaf coproduct. Restriction preserves this coproduct, so the affine criterion gives global quasicoherence.

Imports6

Nyll.SchemeTheory.Modules.QuasicoherentLocal
Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts

Imported by2

def

tildeSectionsIso

L30 ↗

AlgebraicGeometry.Scheme.Modules.tildeSectionsIso

Source context 4 commands

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

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

Lean source · statement

def tildeSectionsIso {R : CommRingCat.{u}}
    (M : (Spec R).Modules) [M.IsQuasicoherent] :
    (tilde.functor R).obj ((moduleSpecΓFunctor (R := R)).obj M) ≅ M

theorem

isQuasicoherent_coprod_toSpec

L40 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_coprod_toSpec

Documentation

Actual binary coproducts of quasicoherent modules are quasicoherent on an affine scheme.

Source context 4 commands

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

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

Lean source · statement

theorem isQuasicoherent_coprod_toSpec {R : CommRingCat.{u}}
    (M N : (Spec R).Modules) [M.IsQuasicoherent] [N.IsQuasicoherent] :
    (M ⨿ N).IsQuasicoherent

theorem

isQuasicoherent_coprod

L56 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_coprod

Documentation

The actual binary coproduct of quasicoherent scheme modules is quasicoherent.

Source context 4 commands

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

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

Lean source · statement

theorem isQuasicoherent_coprod {X : Scheme.{u}}
    (M N : X.Modules) [M.IsQuasicoherent] [N.IsQuasicoherent] :
    (M ⨿ N).IsQuasicoherent

theorem

isQuasicoherent_coprod_native

L77 ↗

SheafOfModules.isQuasicoherent_coprod_native

Documentation

The actual native binary coproduct of quasicoherent sheaves on a scheme is quasicoherent.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace SheafOfModules

Lean source · statement

theorem isQuasicoherent_coprod_native {X : AlgebraicGeometry.Scheme.{u}}
    (M N : SheafOfModules.{u} X.ringCatSheaf) [M.IsQuasicoherent] [N.IsQuasicoherent] :
    (M ⨿ N).IsQuasicoherent

Module documentation

Quasicoherence of actual binary coproducts

Declarations

tildeSectionsIso

isQuasicoherent_coprod_toSpec

isQuasicoherent_coprod

isQuasicoherent_coprod_native