AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_idealPow.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_idealPow
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)