NYLL
Module

OModulePresheaf_isCoherent_idealPowQuot.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_isCoherent_idealPowQuot
2 declarations indexed from sourceView source ↗

Module documentation

Coherence of quotients of a coherent module presheaf by ideal powers.

Imports7
Imported by3

Declarations

theorem

isCoherent_idealPowQuot

L51 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.isCoherent_idealPowQuot
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_idealPowQuot
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G4T
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section Closure
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
Lean source · statement
theorem isCoherent_idealPowQuot [IsLocallyNoetherian V] (I : V.IdealSheafData)
    (F : OModulePresheaf π) (k : ℕ) (hFc : OModulePresheaf.IsCoherent F) :
    OModulePresheaf.IsCoherent (idealPowQuot π I F k)
theorem

isCoherent_idealPowQuot

L84 ↗
AlgebraicGeometry.OModulePresheaf.isCoherent_idealPowQuot
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_idealPowQuot
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
universe u
open _root_.AlgebraicCurves.Cohomology.Sheaves.Proofs in
open _root_.AlgebraicGeometry OModulePresheaf_isCoherent_idealPowQuot.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.isCoherent_idealPowQuot {R : Type u} [CommRing R]
    {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsLocallyNoetherian V] (I : V.IdealSheafData) (F :
    OModulePresheaf π) (k : ℕ) (hFc : F.IsCoherent) : (OModulePresheaf.idealPowQuot π I F
    k).IsCoherent

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.