NYLL
Module

OModulePresheaf_cechFinite_preimage_of_ih.lean

Nyll.SchemeTheory.Cohomology.Cech.OModulePresheaf_cechFinite_preimage_of_ih
4 declarations indexed from sourceView source ↗

Module documentation

Čech finiteness under closed-subscheme preimage by induction

Imports5
Imported by2

Declarations

theorem

isCoherent_pushforward

L46 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_preimage_of_ih.AlgebraicGeometry.OModulePresheaf.Descend.isCoherent_pushforward
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_preimage_of_ih
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 Descend
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (i : Z ⟶ V)
  [IsClosedImmersion i]
variable (F : OModulePresheaf (i ≫ π))
Lean source · statement
theorem isCoherent_pushforward (hFc : F.IsCoherent) : (pushforward π i F).IsCoherent
theorem

isQuasicoherent_pushforward

L61 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_preimage_of_ih.AlgebraicGeometry.OModulePresheaf.Descend.isQuasicoherent_pushforward
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_preimage_of_ih
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 Descend
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (i : Z ⟶ V)
  [IsClosedImmersion i]
variable (F : OModulePresheaf (i ≫ π))
Lean source · statement
theorem isQuasicoherent_pushforward (hFq : F.IsQuasicoherent) : (pushforward π i
    F).IsQuasicoherent
theorem

supportedIn_pushforward_image

L93 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_preimage_of_ih.AlgebraicGeometry.OModulePresheaf.Descend.supportedIn_pushforward_image
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_preimage_of_ih
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 Descend
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (i : Z ⟶ V)
  [IsClosedImmersion i]
variable (F : OModulePresheaf (i ≫ π))
Lean source · statement
theorem supportedIn_pushforward_image {Y' : Closeds Z} (hFs : F.SupportedIn Y') :
    (pushforward π i F).SupportedIn ⟨i.base '' Y', i.isClosedEmbedding.isClosedMap _ Y'.2⟩
theorem

cechFinite_preimage_of_ih

L103 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_preimage_of_ih
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_preimage_of_ih
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open AlgebraicGeometry.OModulePresheaf.Descend in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_preimage_of_ih
    {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (K : V.OrderedAffineCover)
    {Z₀ : TopologicalSpace.Closeds V}
    (ih : ∀ Y' < Z₀, ∀ G : OModulePresheaf π, G.IsCoherent → G.IsQuasicoherent → G.SupportedIn Y'
      → G.CechFinite K)
    (F : OModulePresheaf ((Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι ≫ π))
    (hFc : F.IsCoherent) (hFq : F.IsQuasicoherent)
    (Y' : TopologicalSpace.Closeds (Scheme.IdealSheafData.vanishingIdeal Z₀).subscheme) (hY' : Y'
      < ⊤)
    (hFs : F.SupportedIn Y') :
    F.CechFinite (K.preimage (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι)

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