NYLL
Module

OrderedAffineCoverCech.lean

Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech
43 declarations indexed from sourceView source ↗

Module documentation

Cech cochains for an ordered affine cover

Finite ordered affine covers index increasing tuples of charts and their intersections. For a presheaf of modules over the structure sheaf, this file constructs cochains and the alternating restriction differential, and defines the associated cohomology modules and finiteness, coherence, quasicoherence, and support properties.

Imports5
Imported by105

Declarations

structure

OrderedAffineCover

L37 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover
Documentation

A finite affine open cover with a linearly ordered index type.

Source context 4 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
Lean source · full declaration
structure Scheme.OrderedAffineCover (V : Scheme.{u}) where
  /-- The finite ordered type of chart indices. -/
  ι : Type u
  /-- The finite enumeration of the chart indices. -/
  [instFintype : Fintype ι]
  /-- The linear order used to orient Cech simplices. -/
  [instLinearOrder : LinearOrder ι]
  /-- The affine open subset assigned to each chart index. -/
  U : ι → V.Opens
  /-- Each indexed open subset is affine. -/
  isAffineOpen : ∀ i, IsAffineOpen (U i)
  /-- The indexed open subsets cover the whole scheme. -/
  iSup_eq_top : ⨆ i, U i = ⊤
def

Idx

L58 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.Idx
Documentation

Strictly increasing tuples of i + 1 chart indices.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
def Idx (i : ℕ) : Type u
instance

instFintypeIdx

L60 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.instFintypeIdx
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
instance instFintypeIdx (i : ℕ) : Fintype (K.Idx i)
instance

instDecidableEqIdx

L62 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.instDecidableEqIdx
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
instance instDecidableEqIdx (i : ℕ) : DecidableEq (K.Idx i)
def

inter

L65 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.inter
Documentation

The intersection of the open subsets indexed by a Cech simplex.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
def inter {i : ℕ} (s : K.Idx i) : V.Opens
def

face

L68 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.face
Documentation

The face obtained by deleting the j-th vertex of a Cech simplex.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
def face {i : ℕ} (s : K.Idx (i + 1)) (j : Fin (i + 2)) : K.Idx i
theorem

face_val

L71 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.face_val
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem face_val {i : ℕ} (s : K.Idx (i + 1)) (j : Fin (i + 2)) :
    (K.face s j).1 = s.1 ∘ Fin.succAbove j
theorem

inter_le

L75 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.inter_le
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem inter_le {i : ℕ} (s : K.Idx i) (j : Fin (i + 1)) : K.inter s ≤ K.U (s.1 j)
theorem

inter_le_inter_face

L77 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.inter_le_inter_face
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem inter_le_inter_face {i : ℕ} (s : K.Idx (i + 1)) (j : Fin (i + 2)) :
    K.inter s ≤ K.inter (K.face s j)
def

ofAffine

L83 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ofAffine
Documentation

The singleton affine open cover whose only open subset is the whole affine scheme.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
variable (V) in
Lean source · full declaration
def ofAffine [IsAffine V] : V.OrderedAffineCover where
  ι := PUnit.{u + 1}
  U _ := ⊤
  isAffineOpen _ := isAffineOpen_top V
  iSup_eq_top := iSup_const
theorem

ofAffine_U

L89 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ofAffine_U
Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
variable (V) in
Lean source · statement
theorem ofAffine_U [IsAffine V] (i : PUnit.{u + 1}) : (ofAffine V).U i = ⊤
def

toOrderedAffineCover

L98 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.toOrderedAffineCover
Documentation

The ordered affine cover associated to two affine opens, indexed by ULift (Fin 2).

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.TwoAffineOpenCover
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover)
Lean source · full declaration
def toOrderedAffineCover : X.OrderedAffineCover where
  ι := ULift.{u} (Fin 2)
  instLinearOrder := LinearOrder.lift' ULift.down ULift.down_injective
  U i := ![𝒱.U0, 𝒱.U1] i.down
  isAffineOpen i := by
    rcases i with ⟨i⟩
    fin_cases i
    · exact 𝒱.isAffineOpen_U0
    · exact 𝒱.isAffineOpen_U1
  iSup_eq_top := by
    rw [eq_top_iff, ← 𝒱.sup_eq_top]
    exact sup_le (le_iSup (fun i : ULift.{u} (Fin 2) => ![𝒱.U0, 𝒱.U1] i.down) ⟨0⟩)
      (le_iSup (fun i : ULift.{u} (Fin 2) => ![𝒱.U0, 𝒱.U1] i.down) ⟨1⟩)
theorem

toOrderedAffineCover_ι

L112 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.toOrderedAffineCover_ι
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.TwoAffineOpenCover
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover)
Lean source · statement
theorem toOrderedAffineCover_ι : 𝒱.toOrderedAffineCover.ι = ULift.{u} (Fin 2)
theorem

toOrderedAffineCover_U_zero

L113 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.toOrderedAffineCover_U_zero
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.TwoAffineOpenCover
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover)
Lean source · statement
theorem toOrderedAffineCover_U_zero : 𝒱.toOrderedAffineCover.U ⟨0⟩ = 𝒱.U0
theorem

toOrderedAffineCover_U_one

L114 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.toOrderedAffineCover_U_one
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.TwoAffineOpenCover
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover)
Lean source · statement
theorem toOrderedAffineCover_U_one : 𝒱.toOrderedAffineCover.U ⟨1⟩ = 𝒱.U1
theorem

toOrderedAffineCover_U

L115 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.toOrderedAffineCover_U
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
namespace Scheme.TwoAffineOpenCover
variable {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover)
Lean source · statement
theorem toOrderedAffineCover_U (i : ULift.{u} (Fin 2)) :
    𝒱.toOrderedAffineCover.U i = ![𝒱.U0, 𝒱.U1] i.down
structure

OModulePresheaf

L122 ↗
AlgebraicGeometry.OModulePresheaf
Documentation

A presheaf of modules over the structure sheaf of V, with compatible actions of R induced by π.

Source context 5 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
Lean source · full declaration
structure OModulePresheaf {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) where
  /-- The module of sections assigned to an open subset. -/
  obj : V.Opens → Type u
  /-- The additive commutative group structure on each section module. -/
  [addCommGroup : ∀ U, AddCommGroup (obj U)]
  /-- The module structure over `R` on each section module. -/
  [module : ∀ U, Module R (obj U)]
  /-- The action of structure sheaf sections on the module over each open subset. -/
  [moduleSections : ∀ U, Module Γ(V, U) (obj U)]
  /-- Compatibility of the action of `R` with the structure sheaf action defined through `π`. -/
  [isScalarTower : ∀ U, letI := Scheme.TwoAffineOpenCover.algebraOfHom π U
    IsScalarTower R Γ(V, U) (obj U)]
  /-- The restriction map, linear over `R`, along an inclusion of open subsets. -/
  res : ∀ {U U' : V.Opens}, U ≤ U' → obj U' →ₗ[R] obj U
  /-- Restriction is compatible with restricting structure sheaf scalars. -/
  res_smul : ∀ {U U' : V.Opens} (h : U ≤ U') (a : Γ(V, U')) (x : obj U'),
    res h (a • x) = (V.presheaf.map (homOfLE h).op).hom a • res h x
  /-- Restriction along the identity inclusion is the identity. -/
  res_refl : ∀ U, res (le_refl U) = LinearMap.id
  /-- Restriction along a composite inclusion is the composite of restrictions. -/
  res_comp : ∀ {U U' U'' : V.Opens} (h : U ≤ U') (h' : U' ≤ U''), res (h.trans h') = res h ∘ₗ res h'
theorem

res_refl_apply

L153 ↗
AlgebraicGeometry.OModulePresheaf.res_refl_apply
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem res_refl_apply (U : V.Opens) (x : F.obj U) : F.res (le_refl U) x = x
theorem

res_res

L156 ↗
AlgebraicGeometry.OModulePresheaf.res_res
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem res_res {U U' U'' : V.Opens} (h : U ≤ U') (h' : U' ≤ U'') (x : F.obj U'') :
    F.res h (F.res h' x) = F.res (h.trans h') x
abbrev

cochain

L161 ↗
AlgebraicGeometry.OModulePresheaf.cochain
Documentation

Cech cochains in degree i, indexed by increasing tuples of i + 1 cover indices.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
abbrev cochain (i : ℕ) : Type u
def

d

L164 ↗
AlgebraicGeometry.OModulePresheaf.d
Documentation

The alternating sum of restrictions from faces, defining the Cech differential.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def d (i : ℕ) : F.cochain K i →ₗ[R] F.cochain K (i + 1)
theorem

d_apply

L168 ↗
AlgebraicGeometry.OModulePresheaf.d_apply
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem d_apply (i : ℕ) (c : F.cochain K i) (s : K.Idx (i + 1)) :
    F.d K i c s = ∑ j : Fin (i + 2),
      ((-1 : ℤ) ^ (j : ℕ)) • F.res (K.inter_le_inter_face s j) (c (K.face s j))
abbrev

H0

L175 ↗
AlgebraicGeometry.OModulePresheaf.H0
Documentation

Cech cocycles in degree zero, the kernel of the first differential.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
abbrev H0 : Submodule R (F.cochain K 0)
abbrev

HSucc

L178 ↗
AlgebraicGeometry.OModulePresheaf.HSucc
Documentation

Degree-i + 1 cocycles modulo the preceding differential image inside the cocycle module.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
abbrev HSucc (i : ℕ) : Type u
def

CechFinite

L183 ↗
AlgebraicGeometry.OModulePresheaf.CechFinite
Documentation

Finiteness over R of H0 and every positive degree Cech cohomology module.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def CechFinite : Prop
theorem

cechFinite_iff

L185 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_iff
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem cechFinite_iff :
    F.CechFinite K ↔ Module.Finite R (F.H0 K) ∧ ∀ i, Module.Finite R (F.HSucc K i)
def

IsCoherent

L190 ↗
AlgebraicGeometry.OModulePresheaf.IsCoherent
Documentation

Every affine open has a section module finite over its ring of functions.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def IsCoherent : Prop
theorem

isCoherent_iff

L192 ↗
AlgebraicGeometry.OModulePresheaf.isCoherent_iff
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem isCoherent_iff :
    F.IsCoherent ↔ ∀ U : V.affineOpens, Module.Finite Γ(V, U.1) (F.obj U.1)
def

IsQuasicoherent

L197 ↗
AlgebraicGeometry.OModulePresheaf.IsQuasicoherent
Documentation

On each affine basic open, powers of its defining section clear denominators and kill the kernel of restriction.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def IsQuasicoherent : Prop
theorem

isQuasicoherent_iff

L204 ↗
AlgebraicGeometry.OModulePresheaf.isQuasicoherent_iff
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem isQuasicoherent_iff : F.IsQuasicoherent ↔
    ∀ (U : V.affineOpens) (f : Γ(V, U.1)),
      (∀ x : F.obj (V.basicOpen f), ∃ (n : ℕ) (y : F.obj U.1),
          F.res (V.basicOpen_le f) y =
            (V.presheaf.map (homOfLE (V.basicOpen_le f)).op).hom (f ^ n) • x)
        ∧ (∀ y : F.obj U.1, F.res (V.basicOpen_le f) y = 0 →
          ∃ n : ℕ, (f ^ n : Γ(V, U.1)) • y = 0)
def

SupportedIn

L214 ↗
AlgebraicGeometry.OModulePresheaf.SupportedIn
Documentation

Sections over affine opens disjoint from Y form a subsingleton.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def SupportedIn (Y : Closeds V) : Prop
theorem

supportedIn_iff

L217 ↗
AlgebraicGeometry.OModulePresheaf.supportedIn_iff
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem supportedIn_iff (Y : Closeds V) :
    F.SupportedIn Y ↔
      ∀ U : V.affineOpens, ((U : V.Opens) : Set V) ∩ Y = ∅ → Subsingleton (F.obj U)
def

unit

L224 ↗
AlgebraicGeometry.OModulePresheaf.unit
Documentation

The structure sheaf presheaf, with its action of R induced by π.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
Lean source · full declaration
def unit : OModulePresheaf π where
  obj U := Γ(V, U)
  addCommGroup _ := inferInstance
  module U := (Scheme.TwoAffineOpenCover.algebraOfHom π U).toModule
  moduleSections _ := Semiring.toModule
  isScalarTower U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    exact IsScalarTower.right
  res {U U'} h :=
    letI := Scheme.TwoAffineOpenCover.algebraOfHom π U
    letI := Scheme.TwoAffineOpenCover.algebraOfHom π U'
    (Scheme.TwoAffineOpenCover.restrictAlgHom π h).toLinearMap
  res_smul h a x := by
    change (V.presheaf.map (homOfLE h).op).hom (a * x)
      = (V.presheaf.map (homOfLE h).op).hom a * (V.presheaf.map (homOfLE h).op).hom x
    exact map_mul _ a x
  res_refl U := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    refine LinearMap.ext fun x => ?_
    change (V.presheaf.map (homOfLE (le_refl U)).op).hom x = x
    rw [Subsingleton.elim (homOfLE (le_refl U)).op (𝟙 (op U)), V.presheaf.map_id]; rfl
  res_comp {U U' U''} h h' := by
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U
    let := Scheme.TwoAffineOpenCover.algebraOfHom π U''
    refine LinearMap.ext fun x => ?_
    change (V.presheaf.map (homOfLE (h.trans h')).op).hom x
      = (V.presheaf.map (homOfLE h).op).hom ((V.presheaf.map (homOfLE h').op).hom x)
    rw [← CommRingCat.comp_apply, ← V.presheaf.map_comp]; rfl
theorem

unit_obj

L253 ↗
AlgebraicGeometry.OModulePresheaf.unit_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
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
Lean source · statement
theorem unit_obj (U : V.Opens) : (unit π).obj U = Γ(V, U)
theorem

unit_res_apply

L255 ↗
AlgebraicGeometry.OModulePresheaf.unit_res_apply
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
Lean source · full declaration
theorem unit_res_apply {U U' : V.Opens} (h : U ≤ U') (x : Γ(V, U')) :
    (unit π).res h (show (unit π).obj U' from x) = (V.presheaf.map (homOfLE h).op).hom x :=
  rfl
theorem

unit_smul

L259 ↗
AlgebraicGeometry.OModulePresheaf.unit_smul
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
Lean source · full declaration
theorem unit_smul (U : V.Opens) (a x : Γ(V, U)) :
    a • (show (unit π).obj U from x) = (show (unit π).obj U from a * x) := rfl
theorem

unit_algebraMap_smul

L262 ↗
AlgebraicGeometry.OModulePresheaf.unit_algebraMap_smul
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
Lean source · full declaration
theorem unit_algebraMap_smul (U : V.Opens) (r : R) (x : Γ(V, U)) :
    r • (show (unit π).obj U from x)
      = (show (unit π).obj U from (Scheme.TwoAffineOpenCover.algebraOfHom π U).algebraMap r * x) :=
  rfl
def

twoChartSections

L272 ↗
AlgebraicGeometry.OModulePresheaf.twoChartSections
Documentation

The two chart section datum obtained by evaluating F on both opens and their overlap.

Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
section TwoChart
variable (𝒱 : V.TwoAffineOpenCover)
Lean source · statement
def twoChartSections : TwoChartCech.Sections (𝒱.cover π)
theorem

twoChartSections_M0

L288 ↗
AlgebraicGeometry.OModulePresheaf.twoChartSections_M0
Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
section TwoChart
variable (𝒱 : V.TwoAffineOpenCover)
Lean source · statement
theorem twoChartSections_M0 : (F.twoChartSections 𝒱).M0 = F.obj 𝒱.U0
theorem

twoChartSections_M1

L289 ↗
AlgebraicGeometry.OModulePresheaf.twoChartSections_M1
Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
section TwoChart
variable (𝒱 : V.TwoAffineOpenCover)
Lean source · statement
theorem twoChartSections_M1 : (F.twoChartSections 𝒱).M1 = F.obj 𝒱.U1
theorem

twoChartSections_M01

L290 ↗
AlgebraicGeometry.OModulePresheaf.twoChartSections_M01
Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
section TwoChart
variable (𝒱 : V.TwoAffineOpenCover)
Lean source · statement
theorem twoChartSections_M01 : (F.twoChartSections 𝒱).M01 = F.obj (𝒱.U0 ⊓ 𝒱.U1)
theorem

twoChartSections_r0_apply

L291 ↗
AlgebraicGeometry.OModulePresheaf.twoChartSections_r0_apply
Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
section TwoChart
variable (𝒱 : V.TwoAffineOpenCover)
Lean source · full declaration
theorem twoChartSections_r0_apply (x : F.obj 𝒱.U0) :
    (F.twoChartSections 𝒱).r0 (show (F.twoChartSections 𝒱).M0 from x) = F.res inf_le_left x := rfl
theorem

twoChartSections_r1_apply

L293 ↗
AlgebraicGeometry.OModulePresheaf.twoChartSections_r1_apply
Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
attribute [instance] Scheme.OrderedAffineCover.instFintype Scheme.OrderedAffineCover.instLinearOrder
attribute [instance] OModulePresheaf.addCommGroup OModulePresheaf.module
  OModulePresheaf.moduleSections
  OModulePresheaf.isScalarTower
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable (π) in
section TwoChart
variable (𝒱 : V.TwoAffineOpenCover)
Lean source · full declaration
theorem twoChartSections_r1_apply (x : F.obj 𝒱.U1) :
    (F.twoChartSections 𝒱).r1 (show (F.twoChartSections 𝒱).M1 from x) = F.res inf_le_right x := rfl

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