Module

OModulePresheaf_supportedIn_idealPowQuot.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_supportedIn_idealPowQuot

2 declarations indexed from sourceView source ↗

Module documentation

Support of a module-presheaf quotient by an ideal power.

Imports4

Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.RingTheory.Localization.Away.Basic
Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafIdealFiltration

Imported by3

theorem

supportedIn_idealPowQuot

L48 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_supportedIn_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.supportedIn_idealPowQuot

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_supportedIn_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 supportedIn_idealPowQuot (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ)
    {Y : Closeds V} (hFs : OModulePresheaf.SupportedIn F Y) :
    OModulePresheaf.SupportedIn (idealPowQuot π I F k) Y

theorem

supportedIn_idealPowQuot

L69 ↗

AlgebraicGeometry.OModulePresheaf.supportedIn_idealPowQuot

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_supportedIn_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_supportedIn_idealPowQuot.AlgebraicGeometry in

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.supportedIn_idealPowQuot {R : Type u} [CommRing
    R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (I : V.IdealSheafData) (F : OModulePresheaf π) (k :
    ℕ) {Y : TopologicalSpace.Closeds V} (hFs : F.SupportedIn Y) : (OModulePresheaf.idealPowQuot π
    I F k).SupportedIn Y

Module documentation

Declarations

supportedIn_idealPowQuot

supportedIn_idealPowQuot