NYLL
Module

OModulePresheaf_cechFinite_of_forall_integral.lean

Nyll.SchemeTheory.Cohomology.Cech.OModulePresheaf_cechFinite_of_forall_integral
3 declarations indexed from sourceView source ↗

Module documentation

Cech finiteness from the corresponding assertion on integral closed subschemes of the support.

Imports13
Imported by2

Declarations

theorem

isNoetherian_of_isProper

L52 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_integral.AlgebraicGeometry.OModulePresheaf.Driver.isNoetherian_of_isProper
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_integral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Driver
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
Lean source · statement
theorem isNoetherian_of_isProper [IsNoetherianRing R] (π : V ⟶ Spec (.of R)) [IsProper π] :
    IsNoetherian V
theorem

cechFinite_of_supportedIn_empty

L60 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_integral.AlgebraicGeometry.OModulePresheaf.Driver.cechFinite_of_supportedIn_empty
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_integral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Driver
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
Lean source · statement
theorem cechFinite_of_supportedIn_empty (π : V ⟶ Spec (.of R)) [IsSeparated π] (K :
    V.OrderedAffineCover)
    (F : OModulePresheaf π) {Y : Closeds V} (hY : (Y : Set V) = ∅) (hFs : F.SupportedIn Y) :
      F.CechFinite K
theorem

cechFinite_of_forall_integral

L76 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_of_forall_integral
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_forall_integral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open AlgebraicGeometry.OModulePresheaf.Driver in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_of_forall_integral
    {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
      [IsProper π]
    (K : V.OrderedAffineCover)
    (hInt : ∀ Z₀ : TopologicalSpace.Closeds V, (Z₀ : Set V).Nonempty →
      IsIntegral (Scheme.IdealSheafData.vanishingIdeal Z₀).subscheme →
      (∀ Y' < Z₀, ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y' →
        G.CechFinite K) →
      (OModulePresheaf.pushforwardUnit π (Scheme.IdealSheafData.vanishingIdeal
        Z₀).subschemeι).CechFinite K) :
    ∀ (Y : TopologicalSpace.Closeds V) (F : OModulePresheaf π),
      F.IsCoherent → F.IsQuasicoherent → F.SupportedIn Y → 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.