Module

OModulePresheaf_isQuasicoherent_ofModules_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_ofModules_of_locallyTrivial

1 declaration indexed from sourceView source ↗

Module documentation

Quasicoherence of the section presheaf of a locally trivial scheme module.

Quasicoherence of the presheaf associated to a locally trivial module.

Imports4

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafOfModules
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.AffineScheme
Nyll.SchemeTheory.Modules.LocallyTrivialSectionsLocalization

Imported by28

theorem

isQuasicoherent_ofModules_of_locallyTrivial

L34 ↗

AlgebraicGeometry.OModulePresheaf.isQuasicoherent_ofModules_of_locallyTrivial

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_ofModules_of_locallyTrivial
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.isQuasicoherent_ofModules_of_locallyTrivial
    {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
    (htriv : ∀ x : V, ∃ (U : V.Opens), x ∈ U ∧
      Nonempty ((Scheme.Modules.pullback U.ι).obj M ≅ SheafOfModules.unit
        U.toScheme.ringCatSheaf)) :
    (OModulePresheaf.ofModules π M).IsQuasicoherent

Module documentation

Declarations

isQuasicoherent_ofModules_of_locallyTrivial