Module

OModulePresheaf_hasDevissageStep.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_hasDevissageStep

44 declarations indexed from sourceView source ↗

Module documentation

Devissage of coherent quasicoherent module presheaves supported on a closed subset.

Imports5

Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.RingTheory.Localization.Away.Basic
Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafConstructions
Nyll.SchemeTheory.Divisors.Scheme_isIntegral_subscheme_vanishingIdeal

Imported by3

def

annIdealSubAff

L49 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annIdealSubAff

Documentation

The sections over an affine open annihilated by its ideal of I.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

def annIdealSubAff (I : V.IdealSheafData) (F : OModulePresheaf π)
    (W : V.affineOpens) : Submodule Γ(V, W.1) (F.obj W.1)

def

annIdealSub

L57 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annIdealSub

Documentation

The submodule of sections whose restrictions to affine opens are annihilated by I.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

def annIdealSub (I : V.IdealSheafData) (F : OModulePresheaf π) (U : V.Opens) :
    Submodule R (F.obj U)

theorem

mem_annIdealSub

L63 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.mem_annIdealSub

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem mem_annIdealSub (I : V.IdealSheafData) (F : OModulePresheaf π) (U : V.Opens)
    (x : F.obj U) :
    x ∈ annIdealSub π I F U
      ↔ ∀ (W : V.affineOpens) (hW : W.1 ≤ U), ∀ a ∈ I.ideal W, a • F.res hW x = 0

theorem

annIdealSub_res

L71 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annIdealSub_res

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem annIdealSub_res (I : V.IdealSheafData) (F : OModulePresheaf π)
    {U U' : V.Opens} (h : U ≤ U') (x : F.obj U')
    (hx : x ∈ annIdealSub π I F U') :
    F.res h x ∈ annIdealSub π I F U

theorem

annIdealSub_Γsmul

L80 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annIdealSub_Γsmul

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem annIdealSub_Γsmul (I : V.IdealSheafData) (F : OModulePresheaf π)
    (U : V.Opens) (c : Γ(V, U)) (x : F.obj U)
    (hx : x ∈ annIdealSub π I F U) :
    c • x ∈ annIdealSub π I F U

def

annIdealPMod

L89 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annIdealPMod

Documentation

The subpresheaf of sections annihilated by I after restriction to affine opens.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · full declaration

def annIdealPMod (I : V.IdealSheafData) (F : OModulePresheaf π) : OModulePresheaf π where
  obj U := annIdealSub π I F U
  addCommGroup U := inferInstance
  module U := inferInstance
  moduleSections U :=
    letI := (Scheme.TwoAffineOpenCover.algebraOfHom π U).toModule; haveI := F.isScalarTower U
    { smul := fun c x => ⟨c • x.1, annIdealSub_Γsmul π I F U c x.1 x.2⟩
      one_smul := fun x => Subtype.ext (one_smul _ x.1)
      mul_smul := fun a b x => Subtype.ext (mul_smul a b x.1)
      smul_zero := fun a => Subtype.ext (smul_zero a)
      smul_add := fun a x y => Subtype.ext (smul_add a x.1 y.1)
      add_smul := fun a b x => Subtype.ext (add_smul a b x.1)
      zero_smul := fun x => Subtype.ext (zero_smul _ x.1) }
  isScalarTower U := by
    let := (Scheme.TwoAffineOpenCover.algebraOfHom π U).toModule; have := F.isScalarTower U
    let : Module Γ(V, U) (annIdealSub π I F U) :=
      { smul := fun c x => ⟨c • x.1, annIdealSub_Γsmul π I F U c x.1 x.2⟩
        one_smul := fun x => Subtype.ext (one_smul _ x.1)
        mul_smul := fun a b x => Subtype.ext (mul_smul a b x.1)
        smul_zero := fun a => Subtype.ext (smul_zero a)
        smul_add := fun a x y => Subtype.ext (smul_add a x.1 y.1)
        add_smul := fun a b x => Subtype.ext (add_smul a b x.1)
        zero_smul := fun x => Subtype.ext (zero_smul _ x.1) }
    exact ⟨fun r a x => Subtype.ext (smul_assoc r a x.1)⟩
  res {U U'} h := LinearMap.codRestrict (annIdealSub π I F U)
    ((F.res h).comp (annIdealSub π I F U').subtype)
    (fun x => annIdealSub_res π I F h x.1 x.2)
  res_smul {U U'} h a x := Subtype.ext (F.res_smul h a x.1)
  res_refl U := LinearMap.ext fun x => Subtype.ext (LinearMap.congr_fun (F.res_refl U) x.1)
  res_comp h h' := LinearMap.ext fun x => Subtype.ext (LinearMap.congr_fun (F.res_comp h h') x.1)

theorem

annIdealSub_affine

L120 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annIdealSub_affine

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem annIdealSub_affine (I : V.IdealSheafData) (F : OModulePresheaf π)
    (U : V.affineOpens) (x : F.obj U.1) :
    x ∈ annIdealSub π I F U.1 ↔ ∀ a ∈ I.ideal U, a • x = 0

theorem

vanishingIdeal_ideal_eq_top

L134 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.vanishingIdeal_ideal_eq_top

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem vanishingIdeal_ideal_eq_top (Z : Closeds V) (U : V.affineOpens)
    (hU : ((U : V.Opens) : Set V) ∩ Z = ∅) :
    (Scheme.IdealSheafData.vanishingIdeal Z).ideal U = ⊤

theorem

annIdealPMod_suppIn

L142 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annIdealPMod_suppIn

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem annIdealPMod_suppIn (Z : Closeds V) (F : OModulePresheaf π) :
    OModulePresheaf.SupportedIn
      (annIdealPMod π (Scheme.IdealSheafData.vanishingIdeal Z) F) Z

theorem

annIdealPMod_isQCF

L152 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annIdealPMod_isQCF

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnIdealPMod
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))

Lean source · statement

theorem annIdealPMod_isQCF [IsLocallyNoetherian V]
    (I : V.IdealSheafData) (F : OModulePresheaf π) (hFq : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.IsQuasicoherent (annIdealPMod π I F)

abbrev

subschemeInc

L190 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.subschemeInc

Documentation

The closed immersion of the subscheme defined by the vanishing ideal of Z.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)

Lean source · statement

abbrev subschemeInc

abbrev

G₂

L196 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂

Documentation

The subpresheaf of F annihilated by the vanishing ideal of Z.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

abbrev G₂ : OModulePresheaf π

theorem

G₂_ann

L198 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_ann

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem G₂_ann (U : V.affineOpens) (x : (G₂ π Z F).obj U.1)
    (a : Γ(V, U.1)) (ha : a ∈ (IZ).ideal U) : a • x.1 = 0

theorem

G₂_cf_id

L202 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_cf_id

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem G₂_cf_id (U : V.affineOpens) (f c : Γ(V, U.1))
    (hfc : (1 : Γ(V, U.1)) - c * f ∈ (IZ).ideal U)
    (x : (G₂ π Z F).obj U.1) (k : ℕ) : (c * f) ^ k • x.1 = x.1

theorem

G₂_res_bij_basicOpen

L212 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_res_bij_basicOpen

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem G₂_res_bij_basicOpen [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) (U : V.affineOpens) (f : Γ(V, U.1))
    (hf : ((U : V.Opens) : Set V) ∩ Z ⊆ V.basicOpen f) :
    Function.Bijective
      ((G₂ π Z F).res (U := (V.affineBasicOpen f).1) (V.basicOpen_le f))

theorem

G₂_res_bij_basicOpen'

L285 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_res_bij_basicOpen'

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem G₂_res_bij_basicOpen' [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) (U : V.affineOpens) (f : Γ(V, U.1))
    (hf : ((U : V.Opens) : Set V) ∩ Z ⊆ V.basicOpen f) {W : V.Opens}
    (hW : W = V.basicOpen f) (hWle : W ≤ U.1) :
    Function.Bijective ((G₂ π Z F).res (U := W) hWle)

theorem

G₂_res_bij

L292 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_res_bij

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem G₂_res_bij [IsSeparated π] [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) {U U' : V.affineOpens} (hle : U'.1 ≤ U.1)
    (hdisj : (((U : V.Opens) : Set V) \ U'.1) ∩ Z = ∅) :
    Function.Bijective ((G₂ π Z F).res (U := U'.1) (U' := U.1) hle)

def

G₂_modZ

L354 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_modZ

Documentation

The action on annihilator sections descended to the section ring of the closed subscheme.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

def G₂_modZ (U : V.affineOpens) :
    Module Γ((IZ).subscheme, iZ ⁻¹ᵁ U.1) ((G₂ π Z F).obj U.1)

theorem

G₂_modZ_smul

L368 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_modZ_smul

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

theorem G₂_modZ_smul (U : V.affineOpens) (c : Γ(V, U.1))
    (x : (G₂ π Z F).obj U.1) :
    letI := G₂_modZ π Z F U
    ((IZ).subschemeι.app U.1).hom c • x = c • x := Subtype.ext <| by
  set c' := ((IZ).subschemeι_app_surjective U (((IZ).subschemeι.app U.1).hom c)).choose
  have hker : c' - c ∈ (IZ).ideal U := by
    rw [← (IZ).ker_subschemeι_app U, RingHom.mem_ker, map_sub,
      ((IZ).subschemeι_app_surjective U _).choose_spec, sub_self]
  change c' • x.1 = c • x.1
  have := G₂_ann π Z F U x (c' - c) hker
  rwa [sub_smul, sub_eq_zero] at this

def

annPullIdx

L381 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPullIdx

Documentation

The affine opens of V whose inverse images under the closed immersion lie in W.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

def annPullIdx (W : (IZ).subscheme.Opens) : Type u

def

G₂_modZW

L388 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_modZW

Documentation

The action of sections over W obtained by restricting to the inverse image of the indexed affine open.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

def G₂_modZW (W : (IZ).subscheme.Opens) (U : annPullIdx Z W) :
    Module Γ((IZ).subscheme, W) ((G₂ π Z F).obj U.1.1)

def

annPullSub

L397 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPullSub

Documentation

The submodule of annihilator-section families compatible with restriction between indexed affine opens.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

def annPullSub (W : (IZ).subscheme.Opens) :
    Submodule R (∀ U : annPullIdx Z W, (G₂ π Z F).obj U.1.1) where
  carrier := {x | ∀ (U U' : annPullIdx Z W) (h : U.1.1 ≤ U'.1.1),
    (G₂ π Z F).res h (x U') = x U}
  add_mem' := fun {x y} hx hy U U' h => by
    change (G₂ π Z F).res h (x U' + y U') = x U + y U
    rw [map_add, hx U U' h, hy U U' h]
  zero_mem' := fun U U' h => by
    change (G₂ π Z F).res h 0 = 0; exact map_zero _
  smul_mem' := fun c x hx U U' h => by
    change (G₂ π Z F).res h (c • x U') = c • x U
    rw [map_smul, hx U U' h]

theorem

G₂_modZW_smul

L410 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.G₂_modZW_smul

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

theorem G₂_modZW_smul (W : (IZ).subscheme.Opens)
    (U : annPullIdx Z W) (c : Γ((IZ).subscheme, W)) (ℓ : Γ(V, U.1.1))
    (hℓ : ((IZ).subschemeι.app U.1.1).hom ℓ
      = ((IZ).subscheme.presheaf.map (homOfLE U.2).op).hom c)
    (x : (G₂ π Z F).obj U.1.1) :
    letI := G₂_modZW π Z F W U
    c • x = ℓ • x := by
  let := G₂_modZ π Z F U.1
  change ((IZ).subscheme.presheaf.map (homOfLE U.2).op).hom c • x = ℓ • x
  rw [← hℓ]; exact G₂_modZ_smul π Z F U.1 ℓ x

theorem

annPullSub_Γsmul

L421 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPullSub_Γsmul

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

theorem annPullSub_Γsmul (W : (IZ).subscheme.Opens) (c : Γ((IZ).subscheme, W))
    (x : ∀ U : annPullIdx Z W, (G₂ π Z F).obj U.1.1)
    (hx : x ∈ annPullSub π Z F W) :
    letI := fun U => G₂_modZW π Z F W U
    (fun U => c • x U) ∈ annPullSub π Z F W := fun U U' h => by
  let := fun V₀ => G₂_modZW π Z F W V₀
  obtain ⟨ℓ', hℓ'⟩ := (IZ).subschemeι_app_surjective U'.1
    (((IZ).subscheme.presheaf.map (homOfLE U'.2).op).hom c)
  have hnat : ((IZ).subschemeι.app U.1.1).hom ((V.presheaf.map (homOfLE h).op).hom ℓ')
      = ((IZ).subscheme.presheaf.map (homOfLE U.2).op).hom c := by
    rw [← CommRingCat.comp_apply, (IZ).subschemeι.naturality, CommRingCat.comp_apply, hℓ',
      ← CommRingCat.comp_apply, ← Functor.map_comp]
    rfl
  change (G₂ π Z F).res h (c • x U') = c • x U
  rw [G₂_modZW_smul π Z F W U' c ℓ' hℓ' (x U'),
    (G₂ π Z F).res_smul h ℓ' (x U'), hx U U' h,
    G₂_modZW_smul π Z F W U c _ hnat (x U)]

def

annPullΓmod

L440 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPullΓmod

Documentation

The section-ring module structure on compatible families of annihilator sections.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

def annPullΓmod (W : (IZ).subscheme.Opens) :
    Module Γ((IZ).subscheme, W) (annPullSub π Z F W)

def

annPullPMod

L455 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPullPMod

Documentation

The presheaf on the closed subscheme formed from compatible families of annihilator sections.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

def annPullPMod : OModulePresheaf (iZ ≫ π) where
  obj W := annPullSub π Z F W
  addCommGroup W := inferInstance
  module W := inferInstance
  moduleSections W := annPullΓmod π Z F W
  isScalarTower W := by
    let := (Scheme.TwoAffineOpenCover.algebraOfHom (iZ ≫ π) W).toModule
    let := annPullΓmod π Z F W
    refine ⟨fun r c x => Subtype.ext (funext fun U => ?_)⟩
    let := G₂_modZW π Z F W U
    let := (Scheme.TwoAffineOpenCover.algebraOfHom π U.1.1).toModule
    have := (G₂ π Z F).isScalarTower U.1.1
    change (r • c) • x.1 U = r • (c • x.1 U)
    obtain ⟨ℓ, hℓ⟩ := (IZ).subschemeι_app_surjective U.1
      (((IZ).subscheme.presheaf.map (homOfLE U.2).op).hom c)
    have hrℓ : ((IZ).subschemeι.app U.1.1).hom (r • ℓ)
        = ((IZ).subscheme.presheaf.map (homOfLE U.2).op).hom (r • c) := by
      let := Scheme.TwoAffineOpenCover.algebraOfHom π U.1.1
      let := Scheme.TwoAffineOpenCover.algebraOfHom (iZ ≫ π) W
      let := Scheme.TwoAffineOpenCover.algebraOfHom (iZ ≫ π) (iZ ⁻¹ᵁ U.1.1)
      rw [Algebra.smul_def, Algebra.smul_def, map_mul, map_mul, hℓ]
      refine congrArg (· * _) (Eq.trans ?_
        (?_ : _ = algebraMap R Γ((IZ).subscheme, iZ ⁻¹ᵁ U.1.1) r).symm)
      · rw [Scheme.Hom.app_eq_appLE]
        exact OModulePresheaf.appLE_algebraMap (iZ) U.1.1 r
      · exact (Scheme.TwoAffineOpenCover.restrictAlgHom (iZ ≫ π) U.2).commutes r
    rw [G₂_modZW_smul π Z F W U (r • c) (r • ℓ) hrℓ (x.1 U),
      G₂_modZW_smul π Z F W U c ℓ hℓ (x.1 U), smul_assoc]
  res {W W'} h :=
    { toFun := fun x => ⟨fun U => x.1 ⟨U.1, U.2.trans h⟩,
        fun U U' hle => x.2 ⟨U.1, U.2.trans h⟩ ⟨U'.1, U'.2.trans h⟩ hle⟩
      map_add' := fun x y => rfl
      map_smul' := fun c x => rfl }
  res_smul {W W'} h c x := Subtype.ext (funext fun U => by
    let := G₂_modZW π Z F W' ⟨U.1, U.2.trans h⟩
    let := G₂_modZW π Z F W U
    change (c • x.1 ⟨U.1, U.2.trans h⟩ : (G₂ π Z F).obj U.1.1)
      = ((IZ).subscheme.presheaf.map (homOfLE h).op).hom c • x.1 ⟨U.1, U.2.trans h⟩
    obtain ⟨ℓ, hℓ⟩ := (IZ).subschemeι_app_surjective U.1
      (((IZ).subscheme.presheaf.map (homOfLE (U.2.trans h)).op).hom c)
    rw [G₂_modZW_smul π Z F W' ⟨U.1, U.2.trans h⟩ c ℓ hℓ,
      G₂_modZW_smul π Z F W U _ ℓ
        (hℓ.trans (by rw [← CommRingCat.comp_apply, ← Functor.map_comp]; rfl))])
  res_refl W := LinearMap.ext fun x => Subtype.ext (funext fun U => by
    change x.1 ⟨U.1, _⟩ = x.1 U; congr 1)
  res_comp h h' := LinearMap.ext fun x => Subtype.ext (funext fun U => by
    change x.1 ⟨U.1, _⟩ = x.1 ⟨U.1, _⟩; congr 1)

def

annPull_eval

L504 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPull_eval

Documentation

Evaluation of a compatible family at the indexed affine open U.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

def annPull_eval (U : V.affineOpens) :
    (annPullPMod π Z F).obj (iZ ⁻¹ᵁ U.1) →ₗ[R] (G₂ π Z F).obj U.1 where
  toFun x := x.1 ⟨U, le_rfl⟩
  map_add' _x _y := rfl
  map_smul' _c _x := rfl

theorem

preimage_le_hdisj

L510 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.preimage_le_hdisj

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem preimage_le_hdisj {U U' : V.Opens} (h : iZ ⁻¹ᵁ U' ≤ iZ ⁻¹ᵁ U) :
    ((U' : Set V) \ U) ∩ Z = ∅

theorem

annPull_eval_bij

L518 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPull_eval_bij

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AnnPull
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "iZ" => subschemeInc Z
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem annPull_eval_bij [IsSeparated π] [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) (U : V.affineOpens) :
    Function.Bijective (annPull_eval π Z F U)

def

quotAnnΓmod

L556 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.quotAnnΓmod

Documentation

The section-ring module structure on the quotient by the annihilator submodule.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

def quotAnnΓmod (U : V.Opens) :
    Module Γ(V, U) (F.obj U ⧸ annIdealSub π IZ F U)

theorem

quotAnnΓmod_mk

L578 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.quotAnnΓmod_mk

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

theorem quotAnnΓmod_mk (U : V.Opens) (a : Γ(V, U)) (y : F.obj U) :
    letI := quotAnnΓmod π Z F U
    a • (annIdealSub π IZ F U).mkQ y
      = (annIdealSub π IZ F U).mkQ (a • y) :=
  rfl

def

quotAnnPMod

L585 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.quotAnnPMod

Documentation

The quotient presheaf of F by the subpresheaf annihilated by the vanishing ideal of Z.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

def quotAnnPMod : OModulePresheaf π where
  obj U := F.obj U ⧸ annIdealSub π IZ F U
  addCommGroup U := inferInstance
  module U := inferInstance
  moduleSections U := quotAnnΓmod π Z F U
  isScalarTower U := by
    let := (Scheme.TwoAffineOpenCover.algebraOfHom π U).toModule; let := quotAnnΓmod π Z F U
    have := F.isScalarTower U
    refine ⟨fun r a x => ?_⟩
    obtain ⟨y, rfl⟩ := (annIdealSub π IZ F U).mkQ_surjective x
    rw [quotAnnΓmod_mk, quotAnnΓmod_mk, ← map_smul, smul_assoc]
  res h := Submodule.mapQ _ _ (F.res h) (fun x hx => annIdealSub_res π IZ F h x hx)
  res_smul {U U'} h a x := by
    let := quotAnnΓmod π Z F U'
    let := quotAnnΓmod π Z F U
    obtain ⟨y, rfl⟩ := (annIdealSub π IZ F U').mkQ_surjective x
    rw [quotAnnΓmod_mk]
    change (annIdealSub π IZ F U).mkQ (F.res h (a • y)) = _
    rw [F.res_smul h a y, ← quotAnnΓmod_mk]
    rfl
  res_refl U := by
    refine LinearMap.ext fun x => Quotient.inductionOn' x fun y => ?_
    exact congrArg (Submodule.Quotient.mk) (LinearMap.congr_fun (F.res_refl U) y)
  res_comp h h' := by
    refine LinearMap.ext fun x => Quotient.inductionOn' x fun y => ?_
    exact congrArg (Submodule.Quotient.mk) (LinearMap.congr_fun (F.res_comp h h') y)

def

devSES

L616 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.devSES

Documentation

The affine short exact sequence from the pushed-forward annihilator presheaf to F and its quotient.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · full declaration

def devSES [IsSeparated π] [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.AffSES
      (OModulePresheaf.pushforward π (subschemeInc Z) (annPullPMod π Z F))
      F (quotAnnPMod π Z F) where
  inc :=
    { app := fun U => (annIdealSub π IZ F U.1).subtype
        ∘ₗ annPull_eval π Z F U
      app_smul := fun U a x => by
        have key := G₂_modZW_smul π Z F (subschemeInc Z ⁻¹ᵁ U.1) ⟨U, le_rfl⟩
          (((IZ).subschemeι.appLE U.1 _ le_rfl).hom a) a
          (by rw [← Scheme.Hom.app_eq_appLE,
                show (homOfLE (le_rfl : _ ≤ subschemeInc Z ⁻¹ᵁ U.1)).op = 𝟙 _ from rfl,
                (IZ).subscheme.presheaf.map_id]; rfl)
          (x.1 ⟨U, le_rfl⟩)
        exact congrArg Subtype.val key
      naturality := fun {U U'} h => LinearMap.ext fun x =>
        (congrArg Subtype.val (x.2 ⟨U, (Opens.map (subschemeInc Z).base).monotone h⟩
          ⟨U', le_rfl⟩ h)).symm }
  proj :=
    { app := fun U => (annIdealSub π IZ F U.1).mkQ
      app_smul := fun U a x => (quotAnnΓmod_mk π Z F U.1 a x).symm
      naturality := fun {U U'} h => rfl }
  injective := fun U => Subtype.val_injective.comp (annPull_eval_bij π Z F hFq U).1
  surjective := fun U => Submodule.mkQ_surjective _
  exact := fun U => le_antisymm
    (LinearMap.range_le_ker_iff.mpr (LinearMap.ext fun x =>
      (Submodule.Quotient.mk_eq_zero _).mpr (x.1 ⟨U, le_rfl⟩).2))
    (fun y hy => by
      obtain ⟨x, hx⟩ := (annPull_eval_bij π Z F hFq U).2
        ⟨y, (Submodule.Quotient.mk_eq_zero _).mp hy⟩
      exact ⟨x, congrArg Subtype.val hx⟩)

theorem

annPull_eval_Γsmul

L649 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPull_eval_Γsmul

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem annPull_eval_Γsmul [IsSeparated π] [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) (U : V.affineOpens) (a : Γ(V, U.1))
    (x : (OModulePresheaf.pushforward π (subschemeInc Z)
      (annPullPMod π Z F)).obj U.1) :
    annPull_eval π Z F U (a • x) = a • annPull_eval π Z F U x

theorem

annPull_eval_nat

L656 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.annPull_eval_nat

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem annPull_eval_nat {U U' : V.affineOpens} (h : U.1 ≤ U'.1)
    (x : (OModulePresheaf.pushforward π (subschemeInc Z)
      (annPullPMod π Z F)).obj U'.1) :
    annPull_eval π Z F U
        ((OModulePresheaf.pushforward π (subschemeInc Z)
          (annPullPMod π Z F)).res h x)
      = (annIdealPMod π IZ F).res h (annPull_eval π Z F U' x)

theorem

closedPushAnnPull_isCoherent

L665 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.closedPushAnnPull_isCoherent

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem closedPushAnnPull_isCoherent [IsSeparated π] [IsLocallyNoetherian V]
    (hFc : OModulePresheaf.IsCoherent F) (hFq : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.IsCoherent (OModulePresheaf.pushforward π (subschemeInc Z)
      (annPullPMod π Z F))

theorem

closedPushAnnPull_isQCF

L675 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.closedPushAnnPull_isQCF

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem closedPushAnnPull_isQCF [IsSeparated π] [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.IsQuasicoherent (OModulePresheaf.pushforward π (subschemeInc Z)
      (annPullPMod π Z F))

theorem

closedPushAnnPull_suppIn

L696 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.closedPushAnnPull_suppIn

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem closedPushAnnPull_suppIn [IsSeparated π] [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.SupportedIn (OModulePresheaf.pushforward π (subschemeInc Z)
      (annPullPMod π Z F)) Z

theorem

quotAnnPMod_isCoherent

L703 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.quotAnnPMod_isCoherent

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem quotAnnPMod_isCoherent [IsLocallyNoetherian V]
    (hFc : OModulePresheaf.IsCoherent F) :
    OModulePresheaf.IsCoherent (quotAnnPMod π Z F)

theorem

quotAnnPMod_isQCF

L716 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.quotAnnPMod_isQCF

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem quotAnnPMod_isQCF [IsLocallyNoetherian V]
    (hFq : OModulePresheaf.IsQuasicoherent F) :
    OModulePresheaf.IsQuasicoherent (quotAnnPMod π Z F)

theorem

quotAnnPMod_subsingleton

L749 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.quotAnnPMod_subsingleton

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section QuotG3
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable (Z : Closeds V) (F : OModulePresheaf π)
local notation "IZ" => Scheme.IdealSheafData.vanishingIdeal Z

Lean source · statement

theorem quotAnnPMod_subsingleton (U : V.affineOpens)
    (hAnn : ∀ a ∈ (Scheme.IdealSheafData.vanishingIdeal Z).ideal U, ∀ x : F.obj U.1, a • x = 0) :
    Subsingleton ((quotAnnPMod π Z F).obj U.1)

theorem

devStep'_exists

L761 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.devStep'_exists

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u

Lean source · statement

theorem devStep'_exists {R : Type u} [CommRing R] [IsNoetherianRing R]
    {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] [IsNoetherian V]
    (F : OModulePresheaf π) (hFc : OModulePresheaf.IsCoherent F)
    (hFq : OModulePresheaf.IsQuasicoherent F) (Y : Closeds V)
    (hYne : (Y : Set V).Nonempty) (_hFs : OModulePresheaf.SupportedIn F Y)
    (hAnn : ∀ U : V.affineOpens, ∀ a ∈ (Scheme.IdealSheafData.vanishingIdeal Y).ideal U,
      ∀ x : F.obj U.1, a • x = 0) :
    Nonempty (OModulePresheaf.DevissageStep F Y)

theorem

hasDevissageStep

L827 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep.AlgebraicGeometry.OModulePresheaf.G5B.hasDevissageStep

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace G5B
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u

Lean source · statement

theorem hasDevissageStep : OModulePresheaf.HasDevissageStep.{u}

theorem

hasDevissageStep

L837 ↗

AlgebraicGeometry.OModulePresheaf.hasDevissageStep

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_hasDevissageStep
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.hasDevissageStep :
    AlgebraicGeometry.OModulePresheaf.HasDevissageStep.{u}

Module documentation

Declarations