NYLL
Module

OModulePresheafConstructions.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafConstructions
51 declarations indexed from sourceView source ↗

Module documentation

Basic constructions on module presheaves, including kernels, cokernels, products and restrictions.

Imports5
Imported by33

Declarations

def

preimage

L36 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.preimage
Documentation

The ordered affine cover pulled back along a closed immersion.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace Scheme.OrderedAffineCover
Lean source · full declaration
def preimage {Z : Scheme.{u}} (i : Z ⟶ V) [IsClosedImmersion i] (K : V.OrderedAffineCover) :
    Z.OrderedAffineCover where
  ι := K.ι
  U j := i ⁻¹ᵁ K.U j
  isAffineOpen j := (K.isAffineOpen j).preimage i
  iSup_eq_top := Scheme.Hom.iSup_preimage_eq_top i K.iSup_eq_top
theorem

preimage_U

L43 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.preimage_U
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace Scheme.OrderedAffineCover
Lean source · statement
theorem preimage_U {Z : Scheme.{u}} (i : Z ⟶ V) [IsClosedImmersion i] (K :
  V.OrderedAffineCover) (j : K.ι) :
    (K.preimage i).U j = i ⁻¹ᵁ K.U j
def

prod

L54 ↗
AlgebraicGeometry.OModulePresheaf.prod
Documentation

The pointwise product of two module presheaves.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · full declaration
def prod (F G : OModulePresheaf π) : OModulePresheaf π where
  obj U := F.obj U × G.obj U
  module U := inferInstance
  moduleSections U := Prod.instModule
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    exact ⟨fun r a x => Prod.ext (smul_assoc r a x.1) (smul_assoc r a x.2)⟩
  res h := (F.res h).prodMap (G.res h)
  res_smul h a x := Prod.ext (F.res_smul h a x.1) (G.res_smul h a x.2)
  res_refl U := LinearMap.ext fun x =>
    Prod.ext (LinearMap.congr_fun (F.res_refl U) x.1) (LinearMap.congr_fun (G.res_refl U) x.2)
  res_comp h h' := LinearMap.ext fun x =>
    Prod.ext (LinearMap.congr_fun (F.res_comp h h') x.1) (LinearMap.congr_fun (G.res_comp h h') x.2)
def

fstHom

L69 ↗
AlgebraicGeometry.OModulePresheaf.fstHom
Documentation

The projection from the product module presheaf to its first factor.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · statement
def fstHom (F G : OModulePresheaf π) : Hom (F.prod G) F
def

sndHom

L73 ↗
AlgebraicGeometry.OModulePresheaf.sndHom
Documentation

The projection from the product module presheaf to its second factor.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · statement
def sndHom (F G : OModulePresheaf π) : Hom (F.prod G) G
theorem

prod_obj

L76 ↗
AlgebraicGeometry.OModulePresheaf.prod_obj
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem prod_obj (F G : OModulePresheaf π) (U : V.Opens) : (F.prod G).obj U = (F.obj U ×
  G.obj U)
theorem

fstHom_app

L78 ↗
AlgebraicGeometry.OModulePresheaf.fstHom_app
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem fstHom_app (F G : OModulePresheaf π) (U : V.Opens) (x : (F.prod G).obj U) :
  (F.fstHom G).app U x = x.1
theorem

sndHom_app

L80 ↗
AlgebraicGeometry.OModulePresheaf.sndHom_app
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem sndHom_app (F G : OModulePresheaf π) (U : V.Opens) (x : (F.prod G).obj U) :
  (F.sndHom G).app U x = x.2
def

pow

L84 ↗
AlgebraicGeometry.OModulePresheaf.pow
Documentation

The pointwise finite power of a module presheaf indexed by Fin n.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · full declaration
def pow (F : OModulePresheaf π) (n : ℕ) : OModulePresheaf π where
  obj U := Fin n → F.obj U
  module U := inferInstance
  moduleSections U := Pi.module _ _ _
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    exact ⟨fun r a x => funext fun j => smul_assoc r a (x j)⟩
  res h := LinearMap.compLeft (F.res h) (Fin n)
  res_smul h a x := funext fun j => F.res_smul h a (x j)
  res_refl U := LinearMap.ext fun x => funext fun j => LinearMap.congr_fun (F.res_refl U) (x j)
  res_comp h h' := LinearMap.ext fun x => funext fun j => LinearMap.congr_fun (F.res_comp h h') (x
    j)
theorem

pow_obj

L97 ↗
AlgebraicGeometry.OModulePresheaf.pow_obj
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem pow_obj (F : OModulePresheaf π) (n : ℕ) (U : V.Opens) : (F.pow n).obj U = (Fin n →
  F.obj U)
theorem

pow_res_apply

L99 ↗
AlgebraicGeometry.OModulePresheaf.pow_res_apply
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · statement
theorem pow_res_apply (F : OModulePresheaf π) (n : ℕ) {U U' : V.Opens} (h : U ≤ U') (x : (F.pow
    n).obj U') (j : Fin n) :
    (F.pow n).res h x j = F.res h (x j)
def

zero

L105 ↗
AlgebraicGeometry.OModulePresheaf.zero
Documentation

The zero module presheaf, with singleton sections on every open.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
Lean source · full declaration
def zero : OModulePresheaf π where
  obj _ := PUnit.{u + 1}
  module _ := inferInstance
  moduleSections _ := inferInstance
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    exact ⟨fun _ _ _ => Subsingleton.elim _ _⟩
  res _ := 0
  res_smul _ _ _ := Subsingleton.elim _ _
  res_refl _ := Subsingleton.elim _ _
  res_comp _ _ := Subsingleton.elim _ _
instance

(anonymous instance)

L117 ↗
Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
Lean source · statement
instance (U : V.Opens) : Subsingleton ((zero π).obj U)
def

restrOpen

L121 ↗
AlgebraicGeometry.OModulePresheaf.restrOpen
Documentation

Restrict the sections of F to intersections with the fixed open W₀.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
Lean source · full declaration
def restrOpen (F : OModulePresheaf π) (W₀ : V.Opens) : OModulePresheaf π where
  obj U := F.obj (U ⊓ W₀)
  module U := inferInstance
  moduleSections U := Module.compHom _ (V.presheaf.map (homOfLE (inf_le_left : U ⊓ W₀ ≤ U)).op).hom
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    let := Scheme.TwoAffineOpenCover.algebraOfHom π (U ⊓ W₀)
    let : Module Γ(V, U) (F.obj (U ⊓ W₀)) :=
      Module.compHom _ (V.presheaf.map (homOfLE (inf_le_left : U ⊓ W₀ ≤ U)).op).hom
    refine ⟨fun r a x => ?_⟩
    change (V.presheaf.map (homOfLE (inf_le_left : U ⊓ W₀ ≤ U)).op).hom (r • a) • x
      = r • ((V.presheaf.map (homOfLE (inf_le_left : U ⊓ W₀ ≤ U)).op).hom a • x)
    rw [Algebra.smul_def, map_mul, mul_smul,
      show (V.presheaf.map (homOfLE (inf_le_left : U ⊓ W₀ ≤ U)).op).hom (algebraMap R Γ(V, U) r)
        = algebraMap R Γ(V, U ⊓ W₀) r from (Scheme.TwoAffineOpenCover.restrictAlgHom π
          inf_le_left).commutes r,
      algebraMap_smul]
  res h := F.res (inf_le_inf_right W₀ h)
  res_smul {U U'} h a x := by
    change F.res _ ((V.presheaf.map (homOfLE (inf_le_left : U' ⊓ W₀ ≤ U')).op).hom a • x)
      = (V.presheaf.map (homOfLE (inf_le_left : U ⊓ W₀ ≤ U)).op).hom
          ((V.presheaf.map (homOfLE h).op).hom a) • F.res (inf_le_inf_right W₀ h) x
    rw [F.res_smul, ← CommRingCat.comp_apply, ← CommRingCat.comp_apply (g := V.presheaf.map _),
      ← V.presheaf.map_comp, ← V.presheaf.map_comp]
    rfl
  res_refl U := F.res_refl (U ⊓ W₀)
  res_comp h h' := F.res_comp (inf_le_inf_right W₀ h) (inf_le_inf_right W₀ h')
theorem

restrOpen_obj

L149 ↗
AlgebraicGeometry.OModulePresheaf.restrOpen_obj
Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
Lean source · statement
theorem restrOpen_obj (F : OModulePresheaf π) (W₀ U : V.Opens) : (F.restrOpen W₀).obj U =
  F.obj (U ⊓ W₀)
theorem

restrOpen_res

L151 ↗
AlgebraicGeometry.OModulePresheaf.restrOpen_res
Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
Lean source · statement
theorem restrOpen_res (F : OModulePresheaf π) (W₀ : V.Opens) {U U' : V.Opens} (h : U ≤ U') :
    (F.restrOpen W₀).res h = F.res (inf_le_inf_right W₀ h)
def

submoduleSections

L159 ↗
AlgebraicGeometry.OModulePresheaf.submoduleSections
Documentation

The module structure on a submodule stable under multiplication by local sections.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
def submoduleSections (U : V.Opens) {M : OModulePresheaf π} (p : Submodule R (M.obj U))
    (hp : ∀ (a : Γ(V, U)) (x : M.obj U), x ∈ p → a • x ∈ p) : Module Γ(V, U) p
theorem

range_smul_mem

L165 ↗
AlgebraicGeometry.OModulePresheaf.range_smul_mem
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem range_smul_mem (U : V.Opens) (a : Γ(V, U)) (x : G.obj U) (hx : x ∈ LinearMap.range (φ.app
    U)) :
    a • x ∈ LinearMap.range (φ.app U)
theorem

ker_smul_mem

L170 ↗
AlgebraicGeometry.OModulePresheaf.ker_smul_mem
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem ker_smul_mem (U : V.Opens) (a : Γ(V, U)) (x : F.obj U) (hx : x ∈ LinearMap.ker (φ.app U)) :
    a • x ∈ LinearMap.ker (φ.app U)
def

ker

L175 ↗
AlgebraicGeometry.OModulePresheaf.ker
Documentation

The pointwise kernel module presheaf of the morphism φ.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · full declaration
def ker : OModulePresheaf π where
  obj U := LinearMap.ker (φ.app U)
  module U := inferInstance
  moduleSections U := submoduleSections U _ (ker_smul_mem φ U)
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    let := submoduleSections U _ (ker_smul_mem φ U)
    exact ⟨fun r a x => Subtype.ext (smul_assoc r a x.1)⟩
  res h := (F.res h).restrict fun x hx => LinearMap.mem_ker.mpr <|
    (φ.naturality_apply h x).trans ((congrArg (G.res h) (LinearMap.mem_ker.mp hx)).trans (map_zero
      _))
  res_smul 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)
def

im

L191 ↗
AlgebraicGeometry.OModulePresheaf.im
Documentation

The pointwise image module presheaf of the morphism φ.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · full declaration
def im : OModulePresheaf π where
  obj U := LinearMap.range (φ.app U)
  module U := inferInstance
  moduleSections U := submoduleSections U _ (range_smul_mem φ U)
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    let := submoduleSections U _ (range_smul_mem φ U)
    exact ⟨fun r a x => Subtype.ext (smul_assoc r a x.1)⟩
  res h := (G.res h).restrict fun x ⟨s, hs⟩ => ⟨F.res h s, hs ▸ φ.naturality_apply h s⟩
  res_smul h a x := Subtype.ext (G.res_smul h a x.1)
  res_refl U := LinearMap.ext fun x => Subtype.ext (LinearMap.congr_fun (G.res_refl U) x.1)
  res_comp h h' := LinearMap.ext fun x => Subtype.ext (LinearMap.congr_fun (G.res_comp h h') x.1)
def

cokerModuleSections

L205 ↗
AlgebraicGeometry.OModulePresheaf.cokerModuleSections
Documentation

The local-sections module structure on the pointwise quotient by the image of φ.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
def cokerModuleSections (U : V.Opens) : Module Γ(V, U) (G.obj U ⧸ LinearMap.range
  (φ.app U))
def

coker

L214 ↗
AlgebraicGeometry.OModulePresheaf.coker
Documentation

The pointwise cokernel module presheaf of the morphism φ.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · full declaration
def coker : OModulePresheaf π where
  obj U := G.obj U ⧸ LinearMap.range (φ.app U)
  module U := inferInstance
  moduleSections U := cokerModuleSections φ U
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    let := cokerModuleSections φ U
    exact ⟨fun r a => Quotient.ind' fun x => congrArg Submodule.Quotient.mk (smul_assoc r a x)⟩
  res {U U'} h := Submodule.mapQ _ _ (G.res h) fun x ⟨s, hs⟩ => ⟨F.res h s, hs ▸
    φ.naturality_apply h s⟩
  res_smul {U U'} h a z := z.inductionOn' fun x => congrArg Submodule.Quotient.mk (G.res_smul h a x)
  res_refl U := LinearMap.ext fun z => z.inductionOn' fun x =>
    congrArg Submodule.Quotient.mk (LinearMap.congr_fun (G.res_refl U) x)
  res_comp {U U' U''} h h' := LinearMap.ext fun z => z.inductionOn' fun x =>
    congrArg Submodule.Quotient.mk (LinearMap.congr_fun (G.res_comp h h') x)
theorem

ker_obj

L230 ↗
AlgebraicGeometry.OModulePresheaf.ker_obj
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem ker_obj (U : V.Opens) : (ker φ).obj U = LinearMap.ker (φ.app U)
theorem

im_obj

L231 ↗
AlgebraicGeometry.OModulePresheaf.im_obj
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem im_obj (U : V.Opens) : (im φ).obj U = LinearMap.range (φ.app U)
theorem

coker_obj

L232 ↗
AlgebraicGeometry.OModulePresheaf.coker_obj
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem coker_obj (U : V.Opens) : (coker φ).obj U = (G.obj U ⧸ LinearMap.range (φ.app U))
theorem

ker_res_coe

L234 ↗
AlgebraicGeometry.OModulePresheaf.ker_res_coe
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem ker_res_coe {U U' : V.Opens} (h : U ≤ U') (x : (ker φ).obj U') : ((ker φ).res h x).1 =
    F.res h x.1
theorem

im_res_coe

L236 ↗
AlgebraicGeometry.OModulePresheaf.im_res_coe
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem im_res_coe {U U' : V.Opens} (h : U ≤ U') (x : (im φ).obj U') : ((im φ).res h x).1 = G.res
    h x.1
theorem

coker_res_mk

L238 ↗
AlgebraicGeometry.OModulePresheaf.coker_res_mk
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem coker_res_mk {U U' : V.Opens} (h : U ≤ U') (x : G.obj U') :
    (coker φ).res h (Submodule.Quotient.mk x) = Submodule.Quotient.mk (G.res h x)
theorem

ker_smul_coe

L240 ↗
AlgebraicGeometry.OModulePresheaf.ker_smul_coe
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem ker_smul_coe (U : V.Opens) (a : Γ(V, U)) (x : (ker φ).obj U) : (a • x).1 = a • x.1
theorem

im_smul_coe

L241 ↗
AlgebraicGeometry.OModulePresheaf.im_smul_coe
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem im_smul_coe (U : V.Opens) (a : Γ(V, U)) (x : (im φ).obj U) : (a • x).1 = a • x.1
theorem

coker_smul_mk

L242 ↗
AlgebraicGeometry.OModulePresheaf.coker_smul_mk
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · full declaration
theorem coker_smul_mk (U : V.Opens) (a : Γ(V, U)) (x : G.obj U) :
    (a • (show (coker φ).obj U from Submodule.Quotient.mk x)) = (show (coker φ).obj U from
      Submodule.Quotient.mk (a • x)) := rfl
def

kerImSES

L247 ↗
AlgebraicGeometry.OModulePresheaf.kerImSES
Documentation

The short exact sequence from the kernel of φ through F to the image of φ.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · full declaration
def kerImSES : SES (ker φ) F (im φ) where
  inc :=
    { app := fun U => (LinearMap.ker (φ.app U)).subtype,
      app_smul := fun _ _ _ => rfl,
      naturality := fun _ => rfl }
  proj := { app := fun U => (φ.app U).rangeRestrict
            app_smul := fun U a x => Subtype.ext (φ.app_smul U a x)
            naturality := fun h => LinearMap.ext fun x => Subtype.ext (φ.naturality_apply h x) }
  injective _ := Subtype.val_injective
  surjective U := LinearMap.surjective_rangeRestrict (φ.app U)
  exact U := (Submodule.range_subtype _).trans (LinearMap.ker_rangeRestrict (φ.app U)).symm
def

imCokerSES

L260 ↗
AlgebraicGeometry.OModulePresheaf.imCokerSES
Documentation

The short exact sequence from the image of φ through G to the cokernel of φ.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · full declaration
def imCokerSES : SES (im φ) G (coker φ) where
  inc :=
    { app := fun U => (LinearMap.range (φ.app U)).subtype,
      app_smul := fun _ _ _ => rfl,
      naturality := fun _ => rfl }
  proj :=
    { app := fun U => (LinearMap.range (φ.app U)).mkQ,
      app_smul := fun _ _ _ => rfl,
      naturality := fun _ => rfl }
  injective _ := Subtype.val_injective
  surjective _ := Submodule.Quotient.mk_surjective _
  exact _ := (Submodule.range_subtype _).trans (Submodule.ker_mkQ _).symm
theorem

kerImSES_inc_app

L273 ↗
AlgebraicGeometry.OModulePresheaf.kerImSES_inc_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem kerImSES_inc_app (U : V.Opens) (x : (ker φ).obj U) : (kerImSES φ).inc.app U x = x.1
theorem

kerImSES_proj_app

L274 ↗
AlgebraicGeometry.OModulePresheaf.kerImSES_proj_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem kerImSES_proj_app (U : V.Opens) (x : F.obj U) : ((kerImSES φ).proj.app U x).1 = φ.app U x
theorem

imCokerSES_inc_app

L276 ↗
AlgebraicGeometry.OModulePresheaf.imCokerSES_inc_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · statement
theorem imCokerSES_inc_app (U : V.Opens) (x : (im φ).obj U) : (imCokerSES φ).inc.app U x = x.1
theorem

imCokerSES_proj_app

L278 ↗
AlgebraicGeometry.OModulePresheaf.imCokerSES_proj_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section KerImCoker
variable {F G : OModulePresheaf π} (φ : Hom F G)
Lean source · full declaration
theorem imCokerSES_proj_app (U : V.Opens) (x : G.obj U) : (imCokerSES φ).proj.app U x = (show
    (coker φ).obj U from Submodule.Quotient.mk x) := rfl
theorem

appLE_algebraMap

L287 ↗
AlgebraicGeometry.OModulePresheaf.appLE_algebraMap
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section Pushforward
variable {Z : Scheme.{u}} (i : Z ⟶ V)
Lean source · full declaration
theorem appLE_algebraMap (U : V.Opens) (r : R) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom π U
    letI := Scheme.TwoAffineOpenCover.algebraOfHom (i ≫ π) (i ⁻¹ᵁ U)
    (i.appLE U (i ⁻¹ᵁ U) le_rfl).hom (algebraMap R Γ(V, U) r) = algebraMap R Γ(Z, i ⁻¹ᵁ U) r := by
  change (i.appLE U (i ⁻¹ᵁ U) le_rfl).hom ((π.appLE ⊤ U le_top).hom _) = ((i ≫ π).appLE ⊤ (i ⁻¹ᵁ
    U) le_top).hom _
  rw [← CommRingCat.comp_apply]
  erw [Scheme.Hom.appLE_comp_appLE]
def

pushforward

L298 ↗
AlgebraicGeometry.OModulePresheaf.pushforward
Documentation

Push a module presheaf forward by evaluating its sections on inverse images of opens.

Source context 11 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section Pushforward
variable {Z : Scheme.{u}} (i : Z ⟶ V)
variable (π) in
Lean source · full declaration
def pushforward (H : OModulePresheaf (i ≫ π)) : OModulePresheaf π where
  obj U := H.obj (i ⁻¹ᵁ U)
  module U := inferInstance
  moduleSections U := Module.compHom _ (i.appLE U (i ⁻¹ᵁ U) le_rfl).hom
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    let := Scheme.TwoAffineOpenCover.algebraOfHom (i ≫ π) (i ⁻¹ᵁ U)
    let : Module Γ(V, U) (H.obj (i ⁻¹ᵁ U)) := Module.compHom _ (i.appLE U (i ⁻¹ᵁ U) le_rfl).hom
    refine ⟨fun r a x => ?_⟩
    change (i.appLE U (i ⁻¹ᵁ U) le_rfl).hom (r • a) • x = r • ((i.appLE U (i ⁻¹ᵁ U) le_rfl).hom a
      • x)
    rw [Algebra.smul_def, map_mul, mul_smul, appLE_algebraMap, algebraMap_smul]
  res h := H.res ((Opens.map i.base).monotone h)
  res_smul {U U'} h a x := by
    change H.res _ ((i.appLE U' (i ⁻¹ᵁ U') le_rfl).hom a • x)
      = (i.appLE U (i ⁻¹ᵁ U) le_rfl).hom ((V.presheaf.map (homOfLE h).op).hom a) • H.res
        ((Opens.map i.base).monotone h) x
    rw [H.res_smul, ← CommRingCat.comp_apply, ← CommRingCat.comp_apply (f := V.presheaf.map _),
      Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]
  res_refl U := H.res_refl (i ⁻¹ᵁ U)
  res_comp h h' := H.res_comp ((Opens.map i.base).monotone h) ((Opens.map i.base).monotone h')
theorem

pushforward_obj

L320 ↗
AlgebraicGeometry.OModulePresheaf.pushforward_obj
Source context 11 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section Pushforward
variable {Z : Scheme.{u}} (i : Z ⟶ V)
variable (π) in
Lean source · statement
theorem pushforward_obj (H : OModulePresheaf (i ≫ π)) (U : V.Opens) : (pushforward π i
  H).obj U = H.obj (i ⁻¹ᵁ U)
theorem

pushforward_res

L322 ↗
AlgebraicGeometry.OModulePresheaf.pushforward_res
Source context 11 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section Pushforward
variable {Z : Scheme.{u}} (i : Z ⟶ V)
variable (π) in
Lean source · statement
theorem pushforward_res (H : OModulePresheaf (i ≫ π)) {U U' : V.Opens} (h : U ≤ U') :
    (pushforward π i H).res h = H.res ((Opens.map i.base).monotone h)
theorem

pushforward_smul

L324 ↗
AlgebraicGeometry.OModulePresheaf.pushforward_smul
Source context 11 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section Pushforward
variable {Z : Scheme.{u}} (i : Z ⟶ V)
variable (π) in
Lean source · full declaration
theorem pushforward_smul (H : OModulePresheaf (i ≫ π)) (U : V.Opens) (a : Γ(V, U)) (x : H.obj (i
    ⁻¹ᵁ U)) :
    (a • (show (pushforward π i H).obj U from x)) = (show (pushforward π i H).obj U from (i.appLE
      U (i ⁻¹ᵁ U) le_rfl).hom a • x) := rfl
abbrev

pushforwardUnit

L331 ↗
AlgebraicGeometry.OModulePresheaf.pushforwardUnit
Documentation

The pushforward of the unit module presheaf along i.

Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section Pushforward
variable {Z : Scheme.{u}} (i : Z ⟶ V)
variable (π) in
variable (π) in
Lean source · statement
abbrev pushforwardUnit : OModulePresheaf π
def

zeroFrom

L340 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.zeroFrom
Documentation

The affine morphism from the zero presheaf to F.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section AffHoms
variable (F : OModulePresheaf π)
Lean source · full declaration
def AffHom.zeroFrom : AffHom (zero π) F where
  app _ := 0
  app_smul _ _ _ := by simp
  naturality _ := by ext; simp
def

zeroTo

L346 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.zeroTo
Documentation

The affine morphism from F to the zero presheaf.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section AffHoms
variable (F : OModulePresheaf π)
Lean source · full declaration
def AffHom.zeroTo : AffHom F (zero π) where
  app _ := 0
  app_smul _ _ _ := Subsingleton.elim _ _
  naturality _ := LinearMap.ext fun _ => Subsingleton.elim _ _
def

zeroLeft

L352 ↗
AlgebraicGeometry.OModulePresheaf.AffSES.zeroLeft
Documentation

The affine short exact sequence with zero kernel and identity projection on F.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section AffHoms
variable (F : OModulePresheaf π)
Lean source · full declaration
def AffSES.zeroLeft : AffSES (zero π) F F where
  inc := AffHom.zeroFrom F
  proj := AffHom.id F
  injective _ := fun _ _ _ => Subsingleton.elim _ _
  surjective _ := Function.surjective_id
  exact _ := by
    change LinearMap.range (0 : _ →ₗ[R] _) = LinearMap.ker LinearMap.id
    rw [LinearMap.range_zero, LinearMap.ker_id]
def

powOne

L362 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.powOne
Documentation

Evaluation at the unique coordinate of the first power of F.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section AffHoms
variable (F : OModulePresheaf π)
Lean source · full declaration
def AffHom.powOne : AffHom (F.pow 1) F where
  app U := LinearMap.proj (R := R) (φ := fun _ : Fin 1 => F.obj U.1) 0
  app_smul _ _ _ := rfl
  naturality _ := rfl
def

powOne

L368 ↗
AlgebraicGeometry.OModulePresheaf.AffSES.powOne
Documentation

The affine short exact sequence identifying the first power of F with F.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
section AffHoms
variable (F : OModulePresheaf π)
Lean source · full declaration
def AffSES.powOne : AffSES (F.pow 1) F (zero π) where
  inc := AffHom.powOne F
  proj := AffHom.zeroTo F
  injective _ := fun f g h => funext fun j => Fin.fin_one_eq_zero j ▸ h
  surjective _ := fun x => ⟨0, Subsingleton.elim _ _⟩
  exact U := by
    apply le_antisymm
    · exact fun x _ => LinearMap.mem_ker.mpr (Subsingleton.elim _ _)
    · exact fun x _ => ⟨fun _ => x, rfl⟩
structure

DevissageStep

L384 ↗
AlgebraicGeometry.OModulePresheaf.DevissageStep
Documentation

An integral support piece, its pushed-forward module presheaf, and an exact sequence with smaller supported quotient.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
Lean source · full declaration
structure DevissageStep (F : OModulePresheaf π) (Y : Closeds V) where
  /-- The closed integral support piece selected inside Y. -/
  Z₀ : Closeds V
  /-- The subscheme defined by the vanishing ideal of Z₀ is integral. -/
  isIntegral : IsIntegral (Scheme.IdealSheafData.vanishingIdeal Z₀).subscheme
  /-- The selected support piece is contained in Y. -/
  Z₀_le : Z₀ ≤ Y
  /-- The selected support piece is nonempty. -/
  Z₀_nonempty : (Z₀ : Set V).Nonempty
  /-- The module presheaf on the selected integral subscheme. -/
  H : OModulePresheaf ((Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι ≫ π)
  /-- The pushforward of H is coherent. -/
  isCoherent_pushforward : (pushforward π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι
    H).IsCoherent
  /-- The pushforward of H is quasicoherent. -/
  isQuasicoherent_pushforward : (pushforward π (Scheme.IdealSheafData.vanishingIdeal
    Z₀).subschemeι H).IsQuasicoherent
  /-- The pushforward of H is supported inside Z₀. -/
  supportedIn_pushforward : (pushforward π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι
    H).SupportedIn Z₀
  /-- The quotient module presheaf in the dévissage sequence. -/
  G₃ : OModulePresheaf π
  /-- The affine short exact sequence from the pushforward of H through F to G₃. -/
  ses : AffSES (pushforward π (Scheme.IdealSheafData.vanishingIdeal Z₀).subschemeι H) F G₃
  /-- A strictly smaller closed set supporting the quotient. -/
  Z₁ : Closeds V
  /-- The closed support of the quotient is strictly smaller than Y. -/
  Z₁_lt : Z₁ < Y
  /-- The quotient module presheaf is coherent. -/
  isCoherent_G₃ : G₃.IsCoherent
  /-- The quotient module presheaf is quasicoherent. -/
  isQuasicoherent_G₃ : G₃.IsQuasicoherent
  /-- The quotient module presheaf is supported inside Z₁. -/
  supportedIn_G₃ : G₃.SupportedIn Z₁
def

HasDevissageStep

L423 ↗
AlgebraicGeometry.OModulePresheaf.HasDevissageStep
Documentation

The existence of a dévissage step for each coherent quasicoherent presheaf annihilated by its nonempty support ideal.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
variable (π) in
Lean source · statement
def HasDevissageStep : Prop

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