NYLL
Module

OModulePresheaf_isQuasicoherent_idealPowQuot.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_idealPowQuot
3 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence of quotients of a quasicoherent module presheaf by ideal powers.

Imports4
Imported by3

Declarations

theorem

isQuasicoherent_idealPow

L47 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.isQuasicoherent_idealPow
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_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 isQuasicoherent_idealPow (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ)
    (hFq : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.IsQuasicoherent (idealPow π I F k)
theorem

isQuasicoherent_idealPowQuot

L106 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.isQuasicoherent_idealPowQuot
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_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 isQuasicoherent_idealPowQuot (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ)
    (hFq : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.IsQuasicoherent (idealPowQuot π I F k)
theorem

isQuasicoherent_idealPowQuot

L173 ↗
AlgebraicGeometry.OModulePresheaf.isQuasicoherent_idealPowQuot
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_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_isQuasicoherent_idealPowQuot.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.isQuasicoherent_idealPowQuot {R : Type u}
    [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (I : V.IdealSheafData) (F :
    OModulePresheaf π) (k : ℕ) (hFq : F.IsQuasicoherent) : (OModulePresheaf.idealPowQuot π I F
    k).IsQuasicoherent

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