NYLL
Module

OModulePresheaf_forall_pushforward_of_isIntegral.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_forall_pushforward_of_isIntegral
19 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf forall pushforward of is Integral

Imports2
Imported by2

Declarations

theorem

support_vanishingIdeal'

L43 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.support_vanishingIdeal'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem support_vanishingIdeal' (Z : Closeds V) :
    (Scheme.IdealSheafData.vanishingIdeal Z).support = Z
theorem

isNoetherian_of_isProper

L47 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isNoetherian_of_isProper
Source context 16 commands

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

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

isCoherent_ker

L59 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isCoherent_ker
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem isCoherent_ker [IsLocallyNoetherian V] (hF : F.IsCoherent) : (ker φ).IsCoherent
theorem

isCoherent_im

L66 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isCoherent_im
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem isCoherent_im (hF : F.IsCoherent) : (im φ).IsCoherent
theorem

isCoherent_coker

L71 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isCoherent_coker
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem isCoherent_coker (hG : G.IsCoherent) : (coker φ).IsCoherent
theorem

isQuasicoherent_coker

L76 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isQuasicoherent_coker
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem isQuasicoherent_coker (hG : G.IsQuasicoherent) (hF : F.IsQuasicoherent) :
    (coker φ).IsQuasicoherent
theorem

isQuasicoherent_ker

L91 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isQuasicoherent_ker
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem isQuasicoherent_ker (hF : F.IsQuasicoherent) (hG : G.IsQuasicoherent) :
    (ker φ).IsQuasicoherent
theorem

isQuasicoherent_im

L107 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isQuasicoherent_im
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem isQuasicoherent_im (hF : F.IsQuasicoherent) (hG : G.IsQuasicoherent) :
    (im φ).IsQuasicoherent
theorem

isCoherent_prod

L120 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isCoherent_prod
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem isCoherent_prod {F G : OModulePresheaf π} (hF : F.IsCoherent) (hG : G.IsCoherent) :
    (F.prod G).IsCoherent
theorem

isQuasicoherent_prod

L124 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isQuasicoherent_prod
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem isQuasicoherent_prod {F G : OModulePresheaf π} (hF : F.IsQuasicoherent) (hG :
  G.IsQuasicoherent) :
    (F.prod G).IsQuasicoherent
theorem

isCoherent_pow

L142 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isCoherent_pow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem isCoherent_pow {F : OModulePresheaf π} (n : ℕ) (hF : F.IsCoherent) : (F.pow n).IsCoherent
theorem

isQuasicoherent_pow

L145 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isQuasicoherent_pow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem isQuasicoherent_pow {F : OModulePresheaf π} (n : ℕ) (hF : F.IsQuasicoherent) :
    (F.pow n).IsQuasicoherent
theorem

isQuasicoherent_restrOpen

L160 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isQuasicoherent_restrOpen
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem isQuasicoherent_restrOpen {F : OModulePresheaf π} (W₀ : V.Opens)
    (haff : ∀ U : V.affineOpens, IsAffineOpen (U.1 ⊓ W₀)) (hF : F.IsQuasicoherent) :
    (F.restrOpen W₀).IsQuasicoherent
theorem

isCoherent_pushforwardUnit

L189 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isCoherent_pushforwardUnit
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section PushUnit
variable {Z : Scheme.{u}} (i : Z ⟶ V) [IsClosedImmersion i]
Lean source · statement
theorem isCoherent_pushforwardUnit : (pushforwardUnit π i).IsCoherent
theorem

isQuasicoherent_unit

L197 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isQuasicoherent_unit
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section PushUnit
variable {Z : Scheme.{u}} (i : Z ⟶ V) [IsClosedImmersion i]
Lean source · statement
theorem isQuasicoherent_unit (π : V ⟶ Spec (.of R)) : (unit π).IsQuasicoherent
theorem

isQuasicoherent_pushforwardUnit

L209 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.isQuasicoherent_pushforwardUnit
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
section PushUnit
variable {Z : Scheme.{u}} (i : Z ⟶ V) [IsClosedImmersion i]
Lean source · statement
theorem isQuasicoherent_pushforwardUnit : (pushforwardUnit π i).IsQuasicoherent
def

affSESPowSucc

L246 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.affSESPowSucc
Documentation

The affine short exact sequence inserting a zero last coordinate into a finite power and projecting to that coordinate.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
def affSESPowSucc (F : OModulePresheaf π) (m : ℕ) : AffSES (F.pow m) (F.pow (m + 1)) F
theorem

pow_of_ext

L294 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral.AlgebraicGeometry.OModulePresheaf.PivotQAux.pow_of_ext
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotQAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem pow_of_ext (Q : OModulePresheaf π → Prop)
    (h0 : ∀ G : OModulePresheaf π, (∀ U : V.affineOpens, Subsingleton (G.obj U.1)) → Q G)
    (hext : ∀ (G₁ G₂ G₃ : OModulePresheaf π), Nonempty (AffSES G₁ G₂ G₃) →
      G₁.IsCoherent → G₁.IsQuasicoherent → G₂.IsCoherent → G₂.IsQuasicoherent →
      G₃.IsCoherent → G₃.IsQuasicoherent → Q G₁ → Q G₃ → Q G₂)
    {F : OModulePresheaf π} (hFc : F.IsCoherent) (hFq : F.IsQuasicoherent) (hF : Q F) (n : ℕ) :
    Q (F.pow n)
theorem

forall_pushforward_of_isIntegral

L313 ↗
AlgebraicGeometry.OModulePresheaf.forall_pushforward_of_isIntegral
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_forall_pushforward_of_isIntegral
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.OModulePresheaf in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.forall_pushforward_of_isIntegral
    {R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
      [IsProper π]
    (Z₀ : Closeds V) (hZ₀ : (Z₀ : Set V).Nonempty)
    (hint : IsIntegral (Scheme.IdealSheafData.vanishingIdeal Z₀).subscheme)
    (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₁))
    (hO : Q (OModulePresheaf.pushforwardUnit π (Scheme.IdealSheafData.vanishingIdeal
      Z₀).subschemeι))
    (ih : ∀ Y' < Z₀, ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y' →
      Q G)
    (H : OModulePresheaf ((Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι ≫ π))
    (hc : (OModulePresheaf.pushforward π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι
      H).IsCoherent)
    (hq : (OModulePresheaf.pushforward π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι
      H).IsQuasicoherent)
    (_hs : (OModulePresheaf.pushforward π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι
      H).SupportedIn Z₀) :
    Q (OModulePresheaf.pushforward π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι H)

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