NYLL
Module

OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot.lean

Nyll.SchemeTheory.Cohomology.Cech.OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot
7 declarations indexed from sourceView source ↗

Module documentation

Cech finiteness by devissage through powers of the vanishing ideal of a supporting closed subset.

Imports7
Imported by2

Declarations

theorem

cechFinite_of_affSES_mid'

L51 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.cechFinite_of_affSES_mid'
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_of_forall_cechFinite_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 Wrappers
variable {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
  [IsSeparated π]
  {F₁ F₂ F₃ : OModulePresheaf π}
Lean source · statement
theorem cechFinite_of_affSES_mid' (K : V.OrderedAffineCover) (S : AffSES F₁ F₂ F₃) (h₁ :
    F₁.CechFinite K)
    (h₃ : F₃.CechFinite K) : F₂.CechFinite K
theorem

cechFinite_of_affSES_right'

L54 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.cechFinite_of_affSES_right'
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_of_forall_cechFinite_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 Wrappers
variable {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
  [IsSeparated π]
  {F₁ F₂ F₃ : OModulePresheaf π}
Lean source · statement
theorem cechFinite_of_affSES_right' (K : V.OrderedAffineCover) (S : AffSES F₁ F₂ F₃) (h₁ :
    F₁.CechFinite K)
    (h₂ : F₂.CechFinite K) : F₃.CechFinite K
theorem

cechFinite_zero

L63 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.cechFinite_zero
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_of_forall_cechFinite_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 ZeroBase
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
Lean source · statement
theorem cechFinite_zero (K : V.OrderedAffineCover) :
    OModulePresheaf.CechFinite (K := K) (OModulePresheaf.zero π)
theorem

cechFinite_idealPow_of_forall_subsingleton

L71 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.cechFinite_idealPow_of_forall_subsingleton
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_of_forall_cechFinite_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 ZeroBase
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
Lean source · statement
theorem cechFinite_idealPow_of_forall_subsingleton [IsSeparated π]
    (K : V.OrderedAffineCover) (I : V.IdealSheafData) (F : OModulePresheaf π) (N : ℕ)
    (hN : ∀ (q : ℕ) (s : K.Idx q),
      idealPowSub π I F N (K.inter s) = ⊥) :
    OModulePresheaf.CechFinite (K := K) (idealPow π I F N)
theorem

exists_cechFinite_idealPow

L87 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.exists_cechFinite_idealPow
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_of_forall_cechFinite_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 ZeroBase
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
Lean source · statement
theorem exists_cechFinite_idealPow [IsSeparated π] [IsLocallyNoetherian V]
    (K : V.OrderedAffineCover) (Y : Closeds V) (F : OModulePresheaf π)
    (hFc : OModulePresheaf.IsCoherent F) (hFq : OModulePresheaf.IsQuasicoherent F)
    (hFs : OModulePresheaf.SupportedIn F Y) :
    ∃ N, OModulePresheaf.CechFinite (K := K)
      (idealPow π (Scheme.IdealSheafData.vanishingIdeal Y) F N)
theorem

cechFinite_of_forall_cechFinite_idealPowQuot

L106 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot.AlgebraicGeometry.OModulePresheaf.G4T.cechFinite_of_forall_cechFinite_idealPowQuot
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_of_forall_cechFinite_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 ZeroBase
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
Lean source · statement
theorem cechFinite_of_forall_cechFinite_idealPowQuot [IsNoetherianRing R] [IsSeparated π]
    [IsLocallyNoetherian V] (K : V.OrderedAffineCover) (Y : Closeds V) (F : OModulePresheaf π)
    (hFc : OModulePresheaf.IsCoherent F) (hFq : OModulePresheaf.IsQuasicoherent F)
    (hFs : OModulePresheaf.SupportedIn F Y)
    (hStep : ∀ k, OModulePresheaf.CechFinite (K := K)
      (idealPowQuot π (Scheme.IdealSheafData.vanishingIdeal Y) F k)) :
    OModulePresheaf.CechFinite (K := K) F
theorem

cechFinite_of_forall_cechFinite_idealPowQuot

L141 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_of_forall_cechFinite_idealPowQuot
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
universe u
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.AlgebraicGeometry
  OModulePresheaf_cechFinite_of_forall_cechFinite_idealPowQuot.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_of_forall_cechFinite_idealPowQuot {R :
    Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated
    π] [IsLocallyNoetherian V] (K : V.OrderedAffineCover) (Y : TopologicalSpace.Closeds V) (F :
    OModulePresheaf π) (hFc : F.IsCoherent) (hFq : F.IsQuasicoherent) (hFs : F.SupportedIn Y)
    (hStep : ∀ k, (OModulePresheaf.idealPowQuot π (Scheme.IdealSheafData.vanishingIdeal Y) F
    k).CechFinite K) : F.CechFinite K

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