Module

OModulePresheaf_isCoherent_ofModules_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isCoherent_ofModules_of_locallyTrivial

1 declaration indexed from sourceView source ↗

Module documentation

Coherence of the module presheaf associated to a locally trivial module sheaf.

Imports5

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafOfModules
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.RingTheory.Finiteness.Defs
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_finite_sections_of_locallyTrivial

Imported by15

theorem

isCoherent_ofModules_of_locallyTrivial

L33 ↗

AlgebraicGeometry.OModulePresheaf.isCoherent_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_isCoherent_ofModules_of_locallyTrivial
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.isCoherent_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).IsCoherent

Module documentation

Declarations

isCoherent_ofModules_of_locallyTrivial