Module

OModulePresheaf_forall_coherent_of_forall_integral.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_forall_coherent_of_forall_integral

4 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf forall coherent of forall integral

Imports5

Imported by5

theorem

isNoetherian

L40 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_coherent_of_forall_integral.P2mDevissageDriver.isNoetherian

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_coherent_of_forall_integral
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace P2mDevissageDriver
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
  [IsProper π]
include π in

Lean source · statement

theorem isNoetherian : IsNoetherian V

theorem

step

L60 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_coherent_of_forall_integral.P2mDevissageDriver.step

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_coherent_of_forall_integral
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace P2mDevissageDriver
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
  [IsProper π]
variable (Q : Closeds V → OModulePresheaf π → Prop)
  (h0 : ∀ (Y : Closeds V) (G : OModulePresheaf π), (∀ U : V.affineOpens, Subsingleton (G.obj U.1))
    → Q Y G)
  (hmono : ∀ (Y Y' : Closeds V) (G : OModulePresheaf π), Y' ≤ Y → Q Y' G → Q Y G)
  (hext : ∀ (Y : Closeds V) (G₁ G₂ G₃ : OModulePresheaf π), Nonempty (AffSES G₁ G₂ G₃) →
    G₁.IsCoherent → G₁.IsQuasicoherent → G₂.IsCoherent → G₂.IsQuasicoherent →
    G₃.IsCoherent → G₃.IsQuasicoherent →
    (Q Y G₁ → Q Y G₃ → Q Y G₂) ∧ (Q Y G₁ → Q Y G₂ → Q Y G₃) ∧ (Q Y G₂ → Q Y G₃ → Q Y G₁))
  (hInt : ∀ Z₀ : Closeds V, (Z₀ : Set V).Nonempty →
    IsIntegral (Scheme.IdealSheafData.vanishingIdeal Z₀).subscheme →
    (∀ Y' < Z₀, ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y' → Q Y'
      G) →
    Q Z₀ (pushforwardUnit π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι))
include h0 hmono hext hInt in

Lean source · statement

theorem step (Y : Closeds V)
    (IH : ∀ Y' < Y, ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y' →
      Q Y' G) :
    ∀ F : OModulePresheaf π, F.IsCoherent → F.IsQuasicoherent → F.SupportedIn Y → Q Y F

theorem

main

L88 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_coherent_of_forall_integral.P2mDevissageDriver.main

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_coherent_of_forall_integral
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace P2mDevissageDriver
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
  [IsProper π]
variable (Q : Closeds V → OModulePresheaf π → Prop)
  (h0 : ∀ (Y : Closeds V) (G : OModulePresheaf π), (∀ U : V.affineOpens, Subsingleton (G.obj U.1))
    → Q Y G)
  (hmono : ∀ (Y Y' : Closeds V) (G : OModulePresheaf π), Y' ≤ Y → Q Y' G → Q Y G)
  (hext : ∀ (Y : Closeds V) (G₁ G₂ G₃ : OModulePresheaf π), Nonempty (AffSES G₁ G₂ G₃) →
    G₁.IsCoherent → G₁.IsQuasicoherent → G₂.IsCoherent → G₂.IsQuasicoherent →
    G₃.IsCoherent → G₃.IsQuasicoherent →
    (Q Y G₁ → Q Y G₃ → Q Y G₂) ∧ (Q Y G₁ → Q Y G₂ → Q Y G₃) ∧ (Q Y G₂ → Q Y G₃ → Q Y G₁))
  (hInt : ∀ Z₀ : Closeds V, (Z₀ : Set V).Nonempty →
    IsIntegral (Scheme.IdealSheafData.vanishingIdeal Z₀).subscheme →
    (∀ Y' < Z₀, ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y' → Q Y'
      G) →
    Q Z₀ (pushforwardUnit π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι))
include h0 hmono hext hInt in

Lean source · statement

theorem main : ∀ (Y : Closeds V) (F : OModulePresheaf π), F.IsCoherent → F.IsQuasicoherent →
  F.SupportedIn Y → Q Y F

theorem

forall_coherent_of_forall_integral

L97 ↗

AlgebraicGeometry.OModulePresheaf.forall_coherent_of_forall_integral

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_forall_coherent_of_forall_integral
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.forall_coherent_of_forall_integral
    {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
      [IsProper π]
    (Q : Closeds V → OModulePresheaf π → Prop)
    (h0 : ∀ (Y : Closeds V) (G : OModulePresheaf π), (∀ U : V.affineOpens, Subsingleton (G.obj
      U.1)) → Q Y G)
    (hmono : ∀ (Y Y' : Closeds V) (G : OModulePresheaf π), Y' ≤ Y → Q Y' G → Q Y G)
    (hext : ∀ (Y : Closeds V) (G₁ G₂ G₃ : OModulePresheaf π), Nonempty (OModulePresheaf.AffSES G₁
      G₂ G₃) →
      G₁.IsCoherent → G₁.IsQuasicoherent → G₂.IsCoherent → G₂.IsQuasicoherent →
      G₃.IsCoherent → G₃.IsQuasicoherent →
      (Q Y G₁ → Q Y G₃ → Q Y G₂) ∧ (Q Y G₁ → Q Y G₂ → Q Y G₃) ∧ (Q Y G₂ → Q Y G₃ → Q Y G₁))
    (hInt : ∀ Z₀ : Closeds V, (Z₀ : Set V).Nonempty →
      IsIntegral (Scheme.IdealSheafData.vanishingIdeal Z₀).subscheme →
      (∀ Y' < Z₀, ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y' → Q
        Y' G) →
      Q Z₀ (OModulePresheaf.pushforwardUnit π (Scheme.IdealSheafData.vanishingIdeal
        Z₀).subschemeι)) :
    ∀ (Y : Closeds V) (F : OModulePresheaf π), F.IsCoherent → F.IsQuasicoherent → F.SupportedIn Y →
      Q Y F

Module documentation

OModule Presheaf forall coherent of forall integral

Declarations

isNoetherian

step

main

forall_coherent_of_forall_integral