Module

OModulePresheaf_exists_idealPowSub_eq_bot.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_exists_idealPowSub_eq_bot

4 declarations indexed from sourceView source ↗

Module documentation

A sufficiently high ideal power annihilates a coherent module presheaf supported on its vanishing locus.

Imports4

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

Imported by3

theorem

support_vanishingIdeal

L44 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_idealPowSub_eq_bot.AlgebraicGeometry.OModulePresheaf.G4T.support_vanishingIdeal

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_idealPowSub_eq_bot
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

Lean source · statement

theorem support_vanishingIdeal {V : Scheme.{u}} (Z : Closeds V) :
    (Scheme.IdealSheafData.vanishingIdeal Z).support = Z

theorem

basicOpen_disjoint_of_mem_vanishingIdeal

L52 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_idealPowSub_eq_bot.AlgebraicGeometry.OModulePresheaf.G4T.basicOpen_disjoint_of_mem_vanishingIdeal

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_idealPowSub_eq_bot
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 Terminates
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem basicOpen_disjoint_of_mem_vanishingIdeal (Y : Closeds V)
    (U : V.affineOpens) (f : Γ(V, U.1))
    (hf : f ∈ (Scheme.IdealSheafData.vanishingIdeal Y).ideal U) :
    ((V.basicOpen f : V.Opens) : Set V) ∩ Y = ∅

theorem

exists_idealPowSub_eq_bot

L70 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_idealPowSub_eq_bot.AlgebraicGeometry.OModulePresheaf.G4T.exists_idealPowSub_eq_bot

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_idealPowSub_eq_bot
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 Terminates
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem exists_idealPowSub_eq_bot [IsLocallyNoetherian V] (Y : Closeds V)
    (F : OModulePresheaf π) (hFc : OModulePresheaf.IsCoherent F)
    (hFq : OModulePresheaf.IsQuasicoherent F) (hFs : OModulePresheaf.SupportedIn F Y)
    (U : V.affineOpens) :
    ∃ N, idealPowSub π (Scheme.IdealSheafData.vanishingIdeal Y) F N U.1 = ⊥

theorem

exists_idealPowSub_eq_bot

L113 ↗

AlgebraicGeometry.OModulePresheaf.exists_idealPowSub_eq_bot

Source context 9 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.exists_idealPowSub_eq_bot {R : Type u} [CommRing
    R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsLocallyNoetherian V] (Y :
    TopologicalSpace.Closeds V) (F : OModulePresheaf π) (hFc : F.IsCoherent) (hFq :
    F.IsQuasicoherent) (hFs : F.SupportedIn Y) (U : V.affineOpens) : ∃ N : ℕ,
    OModulePresheaf.idealPowSub π (Scheme.IdealSheafData.vanishingIdeal Y) F N U.1 = ⊥

Module documentation

Declarations

support_vanishingIdeal

basicOpen_disjoint_of_mem_vanishingIdeal

exists_idealPowSub_eq_bot

exists_idealPowSub_eq_bot