NYLL
Module

OModulePresheaf_forall_of_forall_idealAnnihilates.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_forall_of_forall_idealAnnihilates
9 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf forall of forall ideal Annihilates

Imports9
Imported by2

Declarations

theorem

isLocallyNoetherian

L45 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_of_forall_idealAnnihilates.P2mFiltQ.isLocallyNoetherian
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_of_forall_idealAnnihilates
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mFiltQ
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
section Topology
include π in
Lean source · statement
theorem isLocallyNoetherian [IsNoetherianRing R] [IsProper π] : IsLocallyNoetherian V
theorem

compactSpace

L49 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_of_forall_idealAnnihilates.P2mFiltQ.compactSpace
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_of_forall_idealAnnihilates
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mFiltQ
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
section Topology
include π in
Lean source · statement
theorem compactSpace [IsProper π] : CompactSpace V
theorem

isCoherent_zero

L54 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_of_forall_idealAnnihilates.P2mFiltQ.isCoherent_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_of_forall_idealAnnihilates
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mFiltQ
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
Lean source · statement
theorem isCoherent_zero : (zero π).IsCoherent
theorem

isQuasicoherent_zero

L58 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_of_forall_idealAnnihilates.P2mFiltQ.isQuasicoherent_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_of_forall_idealAnnihilates
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mFiltQ
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
Lean source · statement
theorem isQuasicoherent_zero : (zero π).IsQuasicoherent
theorem

isCoherent_idealPow

L61 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_of_forall_idealAnnihilates.P2mFiltQ.isCoherent_idealPow
Source context 8 commands

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

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

subsingleton_basicOpen_of_subsingleton

L80 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_of_forall_idealAnnihilates.P2mFiltQ.subsingleton_basicOpen_of_subsingleton
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_of_forall_idealAnnihilates
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mFiltQ
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
section Uniform
Lean source · statement
theorem subsingleton_basicOpen_of_subsingleton (G : OModulePresheaf π) (hGq : G.IsQuasicoherent)
    (W : V.affineOpens) [Subsingleton (G.obj W.1)] (g : Γ(V, W.1)) :
    Subsingleton (G.obj (V.basicOpen g))
theorem

exists_forall_subsingleton_idealPow

L93 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_of_forall_idealAnnihilates.P2mFiltQ.exists_forall_subsingleton_idealPow
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_of_forall_idealAnnihilates
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mFiltQ
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
section Uniform
variable [IsNoetherianRing R] [IsProper π]
Lean source · statement
theorem exists_forall_subsingleton_idealPow (Y : Closeds V) (F : OModulePresheaf π) (hFc :
  F.IsCoherent)
    (hFq : F.IsQuasicoherent) (hFs : F.SupportedIn Y) :
    ∃ N : ℕ, ∀ U : V.affineOpens,
      Subsingleton ((idealPow π (Scheme.IdealSheafData.vanishingIdeal Y) F N).obj U.1)
theorem

main

L158 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_of_forall_idealAnnihilates.P2mFiltQ.main
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_of_forall_idealAnnihilates
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mFiltQ
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
section Main
variable [IsNoetherianRing R] [IsProper π]
variable (Y : Closeds V) (Q : OModulePresheaf π → Prop)
  (h0 : ∀ G : OModulePresheaf π, (∀ U : V.affineOpens, Subsingleton (G.obj U.1)) → Q G)
  (hext : ∀ (G₁ G₂ G₃ : OModulePresheaf π), Nonempty (OModulePresheaf.AffSES G₁ G₂ G₃) →
    G₁.IsCoherent → G₁.IsQuasicoherent → G₂.IsCoherent → G₂.IsQuasicoherent →
    G₃.IsCoherent → G₃.IsQuasicoherent →
    (Q G₁ → Q G₃ → Q G₂) ∧ (Q G₁ → Q G₂ → Q G₃) ∧ (Q G₂ → Q G₃ → Q G₁))
  (hann : ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y →
    OModulePresheaf.IdealAnnihilates π (Scheme.IdealSheafData.vanishingIdeal Y) G → Q G)
include h0 hext hann in
Lean source · statement
theorem main : ∀ F : OModulePresheaf π, F.IsCoherent → F.IsQuasicoherent → F.SupportedIn Y → Q F
theorem

forall_of_forall_idealAnnihilates

L197 ↗
AlgebraicGeometry.OModulePresheaf.forall_of_forall_idealAnnihilates
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_of_forall_idealAnnihilates
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.forall_of_forall_idealAnnihilates
    {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
      [IsProper π]
    (Y : Closeds V) (Q : OModulePresheaf π → Prop)
    (h0 : ∀ G : OModulePresheaf π, (∀ U : V.affineOpens, Subsingleton (G.obj U.1)) → Q G)
    (hext : ∀ (G₁ G₂ G₃ : OModulePresheaf π), Nonempty (OModulePresheaf.AffSES G₁ G₂ G₃) →
      G₁.IsCoherent → G₁.IsQuasicoherent → G₂.IsCoherent → G₂.IsQuasicoherent →
      G₃.IsCoherent → G₃.IsQuasicoherent →
      (Q G₁ → Q G₃ → Q G₂) ∧ (Q G₁ → Q G₂ → Q G₃) ∧ (Q G₂ → Q G₃ → Q G₁))
    (hann : ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y →
      OModulePresheaf.IdealAnnihilates π (Scheme.IdealSheafData.vanishingIdeal Y) G → Q G) :
    ∀ F : OModulePresheaf π, F.IsCoherent → F.IsQuasicoherent → F.SupportedIn Y → Q F

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