NYLL
Module

OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.lean

Nyll.SchemeTheory.Cohomology.Cech.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
17 declarations indexed from sourceView source ↗

Module documentation

Finiteness of pushforward Cech cohomology by induction on the integral support.

Imports7
Imported by2

Declarations

theorem

support_vanishingIdeal'

L52 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.support_vanishingIdeal'
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
Lean source · statement
theorem support_vanishingIdeal' {V : Scheme.{u}} (Z : Closeds V) :
    (Scheme.IdealSheafData.vanishingIdeal Z).support = Z
theorem

isCoherent_ker

L80 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isCoherent_ker
Source context 24 commands

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

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

isCoherent_coker

L87 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isCoherent_coker
Source context 24 commands

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

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

isQuasicoherent_coker

L92 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isQuasicoherent_coker
Source context 24 commands

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

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

isQuasicoherent_ker

L107 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isQuasicoherent_ker
Source context 24 commands

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

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

isCoherent_prod

L125 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isCoherent_prod
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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

L129 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isQuasicoherent_prod
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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

L147 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isCoherent_pow
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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

L150 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isQuasicoherent_pow
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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

L165 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isQuasicoherent_restrOpen
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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

eq_zero_of_res_basicOpen_eq_zero

L190 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.eq_zero_of_res_basicOpen_eq_zero
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem eq_zero_of_res_basicOpen_eq_zero {F : OModulePresheaf π} (hF : F.IsQuasicoherent)
    (U : V.affineOpens) {ι : Type*} [Finite ι] (h : ι → Γ(V, U.1))
    (hcov : U.1 ≤ ⨆ j, V.basicOpen (h j)) (x : F.obj U.1)
    (hx : ∀ j, F.res (V.basicOpen_le (h j)) x = 0) : x = 0
theorem

isNoetherian_of_isProper

L210 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isNoetherian_of_isProper
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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_pushforwardUnit

L222 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isCoherent_pushforwardUnit
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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

L230 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isQuasicoherent_unit
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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

L242 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.isQuasicoherent_pushforwardUnit
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
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
theorem

cechFinite_pow

L298 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih.AlgebraicGeometry.OModulePresheaf.PivotAux.cechFinite_pow
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace OModulePresheaf_cechFinite_pushforward_of_isIntegral_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace PivotAux
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem cechFinite_pow [IsNoetherianRing R] [IsSeparated π] (K : V.OrderedAffineCover)
    {F : OModulePresheaf π} (n : ℕ) (hF : F.CechFinite K) : (F.pow n).CechFinite K
theorem

cechFinite_pushforward_of_isIntegral_of_ih

L363 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_pushforward_of_isIntegral_of_ih
Source context 10 commands

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

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

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