NYLL
Module

OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
7 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence of the relative cohomology presheaf in the Chow construction.

Imports3
Imported by3

Declarations

theorem

res_res'

L52 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow.AlgebraicGeometry.OModulePresheaf.Leray.res_res'
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Local
variable {R : Type u} [CommRing R]
Lean source · statement
theorem res_res' {V : Scheme.{u}} {O₁ O₂ O₃ : V.Opens} (h12 : O₁ ≤ O₂) (h23 : O₂ ≤ O₃) (x : Γ(V,
    O₃)) :
    (V.presheaf.map (homOfLE h12).op).hom ((V.presheaf.map (homOfLE h23).op).hom x)
      = (V.presheaf.map (homOfLE (h12.trans h23)).op).hom x
theorem

res_refl'

L58 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow.AlgebraicGeometry.OModulePresheaf.Leray.res_refl'
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Local
variable {R : Type u} [CommRing R]
Lean source · statement
theorem res_refl' {V : Scheme.{u}} {O : V.Opens} (h : O ≤ O) (x : Γ(V, O)) :
    (V.presheaf.map (homOfLE h).op).hom x = x
theorem

algebraOfHom_compat

L63 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow.AlgebraicGeometry.OModulePresheaf.Leray.algebraOfHom_compat
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Local
variable {R : Type u} [CommRing R]
Lean source · full declaration
theorem algebraOfHom_compat {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (W : V.Opens) :
    ∀ c, letI := Scheme.TwoAffineOpenCover.algebraOfHom π W
      algebraMap R Γ(V, W) c = (V.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op).hom
        (π.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom c)) :=
  fun _ => rfl
theorem

specMap_algebraMap_eq_fromSpec_comp

L69 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow.AlgebraicGeometry.OModulePresheaf.Leray.specMap_algebraMap_eq_fromSpec_comp
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Local
variable {R : Type u} [CommRing R]
Lean source · full declaration
theorem specMap_algebraMap_eq_fromSpec_comp {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
    {U : X.Opens} (hU : IsAffineOpen U) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom f U
    Spec.map (CommRingCat.ofHom (algebraMap R Γ(X, U))) = hU.fromSpec ≫ f := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom f U
  have halg : CommRingCat.ofHom (algebraMap R Γ(X, U))
      = (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appLE ⊤ U (le_top : U ≤ f ⁻¹ᵁ ⊤) := rfl
  rw [halg, Spec.map_comp, ← Scheme.isoSpec_Spec_inv, ← IsAffineOpen.fromSpec_top,
    IsAffineOpen.SpecMap_appLE_fromSpec f (isAffineOpen_top (Spec (CommRingCat.of R))) hU
      (le_top : U ≤ f ⁻¹ᵁ ⊤)]
theorem

isNoeth_of_proper

L80 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow.AlgebraicGeometry.OModulePresheaf.Leray.isNoeth_of_proper
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section Local
variable {R : Type u} [CommRing R]
Lean source · statement
theorem isNoeth_of_proper [IsNoetherianRing R] {V : Scheme.{u}}
    (π : V ⟶ Spec (CommRingCat.of R)) [IsProper π] : IsNoetherian V
theorem

isQuasicoherent_relHPresheaf_chow'

L95 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow.AlgebraicGeometry.OModulePresheaf.Leray.isQuasicoherent_relHPresheaf_chow'
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section RelHPresheafChow
variable {R : Type u} [CommRing R] {Z : Scheme.{u}}
variable (πZ : Z ⟶ Spec (CommRingCat.of R)) (D : ChowDatumProj πZ)
Lean source · statement
theorem isQuasicoherent_relHPresheaf_chow' [IsSeparated πZ] (b : ℕ) :
    (relHPresheaf D.p πZ (ProjSpace.stdCoverPullback D.ιN) b).IsQuasicoherent
theorem

isQuasicoherent_relHPresheaf_chow

L236 ↗
AlgebraicGeometry.OModulePresheaf.Leray.isQuasicoherent_relHPresheaf_chow
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.CategoryTheory.Limits
attribute [local instance] MvPolynomial.gradedAlgebra in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.Leray.isQuasicoherent_relHPresheaf_chow {R : Type
    u} [CommRing R]
    {Z : Scheme.{u}} (πZ : Z ⟶ Spec (.of R)) [IsSeparated πZ] (D : ChowDatumProj πZ) (b : ℕ) :
    (OModulePresheaf.Leray.relHPresheaf D.p πZ (ProjSpace.stdCoverPullback D.ιN)
      b).IsQuasicoherent

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