Module

OrderedAffineCoverOf.lean

Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverOf

24 declarations indexed from sourceView source ↗

Module documentation

Ordered affine covers of an open subset

An ordered affine cover of an open has increasing-index Cech cochains, alternating restriction differentials, and an augmentation from sections of the structure sheaf.

Imports1

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafHom

Imported by11

structure

OrderedAffineCoverOf

L33 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf

Documentation

A finite linearly ordered family of affine opens covering the specified open subset.

Source context 5 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}

Lean source · full declaration

structure Scheme.OrderedAffineCoverOf {V : Scheme.{u}} (W : V.Opens) where
  /-- The index type of the affine opens in the cover. -/
  ι : Type u
  /-- A finite enumeration of the cover indices. -/
  [instFintype : Fintype ι]
  /-- The linear order used to form increasing Cech indices. -/
  [instLinearOrder : LinearOrder ι]
  /-- The affine open associated with each cover index. -/
  U : ι → V.Opens
  /-- Each member of the cover is an affine open. -/
  isAffineOpen : ∀ i, IsAffineOpen (U i)
  /-- Each member of the cover lies in the specified open subset. -/
  le : ∀ i, U i ≤ W
  /-- The supremum of the cover members is the specified open subset. -/
  iSup_eq : ⨆ i, U i = W

def

Idx

L58 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.Idx

Documentation

Strictly increasing tuples of cover indices for intersections in the given Cech degree.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

def Idx (i : ℕ) : Type u

instance

(anonymous instance)

L60 ↗

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

instance (i : ℕ) : Fintype (K.Idx i)

instance

(anonymous instance)

L61 ↗

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

instance (i : ℕ) : DecidableEq (K.Idx i)

def

inter

L64 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.inter

Documentation

The intersection of the cover members selected by an increasing tuple.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

def inter {i : ℕ} (s : K.Idx i) : V.Opens

def

face

L67 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.face

Documentation

The increasing tuple obtained by deleting the specified index.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

def face {i : ℕ} (s : K.Idx (i + 1)) (j : Fin (i + 2)) : K.Idx i

theorem

inter_le_inter_face

L70 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.inter_le_inter_face

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable {W : V.Opens} (K : V.OrderedAffineCoverOf W)

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)

theorem

inter_le

L74 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.inter_le

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable {W : V.Opens} (K : V.OrderedAffineCoverOf W)

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_base

L76 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.inter_le_base

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

theorem inter_le_base {i : ℕ} (s : K.Idx i) : K.inter s ≤ W

def

toCoverOf

L83 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf

Documentation

Regard an ordered affine cover of the scheme as a cover of its top open.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCover

Lean source · full declaration

def toCoverOf (K : V.OrderedAffineCover) : V.OrderedAffineCoverOf ⊤ where
  ι := K.ι
  U := K.U
  isAffineOpen := K.isAffineOpen
  le _ := le_top
  iSup_eq := K.iSup_eq_top

theorem

toCoverOf_U

L90 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCover

Lean source · statement

theorem toCoverOf_U (K : V.OrderedAffineCover) (i : K.ι) : K.toCoverOf.U i = K.U i

def

restrict

L93 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.restrict

Documentation

Intersect an ordered affine cover with an affine open in a separated scheme over the base.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCover

Lean source · full declaration

def restrict (π : V ⟶ Spec (.of R)) [IsSeparated π] (K : V.OrderedAffineCover) {W : V.Opens}
    (hW : IsAffineOpen W) : V.OrderedAffineCoverOf W where
  ι := K.ι
  U i := K.U i ⊓ W
  isAffineOpen i := isAffineOpen_inf_of_isSeparated π (K.isAffineOpen i) hW
  le _ := inf_le_right
  iSup_eq := by rw [← iSup_inf_eq, K.iSup_eq_top, top_inf_eq]

theorem

restrict_U

L101 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCover

Lean source · statement

theorem restrict_U (π : V ⟶ Spec (.of R)) [IsSeparated π] (K : V.OrderedAffineCover) {W
    : V.Opens}
    (hW : IsAffineOpen W) (i : K.ι) : (K.restrict π hW).U i = K.U i ⊓ W

def

moduleSections

L112 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.moduleSections

Documentation

The base-ring module structure on sections supplied by the structural morphism.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

def moduleSections : ∀ O : V.Opens, Module R Γ(V, O)

abbrev

cochain

L116 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.cochain

Documentation

Cech cochains of the structure sheaf on the selected intersections of the cover.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

abbrev cochain (i : ℕ) : Type u

def

res

L119 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.res

Documentation

The base-linear restriction map on structure-sheaf sections.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · full declaration

def res {O O' : V.Opens} (h : O ≤ O') :
    letI := moduleSections π
    (Γ(V, O') : Type u) →ₗ[R] (Γ(V, O) : Type u) :=
  (OModulePresheaf.unit π).res h

theorem

res_apply

L124 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.res_apply

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

theorem res_apply {O O' : V.Opens} (h : O ≤ O') (x : Γ(V, O')) :
    res π h x = (V.presheaf.map (homOfLE h).op).hom x

def

d

L128 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.d

Documentation

The alternating sum of face restriction maps defining the Cech differential.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · full declaration

def d (i : ℕ) :
    letI := moduleSections π
    K.cochain i →ₗ[R] K.cochain (i + 1) :=
  letI := moduleSections π
  LinearMap.pi fun s => ∑ j : Fin (i + 2), ((-1 : ℤ) ^ (j : ℕ)) •
    ((res π (K.inter_le_inter_face s j)).comp (LinearMap.proj (K.face s j)))

theorem

d_apply

L135 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.d_apply

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · full declaration

theorem d_apply (i : ℕ) (f : K.cochain i) (s : K.Idx (i + 1)) :
    letI := moduleSections π
    K.d π i f s = ∑ j : Fin (i + 2), ((-1 : ℤ) ^ (j : ℕ)) •
      (V.presheaf.map (homOfLE (K.inter_le_inter_face s j)).op).hom (f (K.face s j)) := by
  simp only [d, LinearMap.pi_apply, LinearMap.sum_apply, LinearMap.smul_apply, LinearMap.comp_apply,
    LinearMap.proj_apply, res_apply]

def

aug

L143 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.aug

Documentation

The augmentation sending a section on the covered open to its restrictions on the cover.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · full declaration

def aug :
    letI := moduleSections π
    (Γ(V, W) : Type u) →ₗ[R] K.cochain 0 :=
  letI := moduleSections π
  LinearMap.pi fun s => res π (K.inter_le_base s)

theorem

aug_apply

L149 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.aug_apply

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · full declaration

theorem aug_apply (w : Γ(V, W)) (s : K.Idx 0) :
    letI := moduleSections π
    K.aug π w s = (V.presheaf.map (homOfLE (K.inter_le_base s)).op).hom w := rfl

abbrev

H0

L154 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.H0

Documentation

The degree-zero Cech cohomology, represented by the kernel of the first differential.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

abbrev H0 : Type u

abbrev

HSucc

L159 ↗

AlgebraicGeometry.Scheme.OrderedAffineCoverOf.HSucc

Documentation

Positive Cech cohomology as cocycles modulo the image of the preceding differential.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder
namespace Scheme.OrderedAffineCoverOf
variable (π : V ⟶ Spec (.of R)) {W : V.Opens} (K : V.OrderedAffineCoverOf W)

Lean source · statement

abbrev HSucc (i : ℕ) : Type u

theorem

d_toCoverOf

L166 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.d_toCoverOf

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
attribute [instance]
  Scheme.OrderedAffineCoverOf.instFintype
  Scheme.OrderedAffineCoverOf.instLinearOrder

Lean source · statement

theorem Scheme.OrderedAffineCover.d_toCoverOf (π : V ⟶ Spec (.of R)) (K : V.OrderedAffineCover)
    (i : ℕ) :
    K.toCoverOf.d π i = (OModulePresheaf.unit π).d K i

Module documentation

Ordered affine covers of an open subset

Declarations