NYLL
Module

OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
52 declarations indexed from sourceView source ↗

Module documentation

Exactness of positive Cech degrees for a quasicoherent module presheaf on an affine cover. An insertion homotopy and localization on basic opens establish the kernel-range inclusion.

Imports5
Imported by6

Declarations

abbrev

altImg

L50 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altImg
Documentation

The finite set of cover indices occurring in an increasing Cech index.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
abbrev altImg {i : ℕ} (s : K.Idx i) : Finset K.ι
theorem

card_altImg

L53 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.card_altImg
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem card_altImg {i : ℕ} (s : K.Idx i) :
    (altImg K s).card = i + 1
theorem

altIdx_canonical

L57 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altIdx_canonical
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altIdx_canonical {i : ℕ} (s : K.Idx i) :
    s.1 = (altImg K s).orderEmbOfFin (card_altImg K s)
theorem

altIdx_eq_of_altImg

L61 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altIdx_eq_of_altImg
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altIdx_eq_of_altImg {i : ℕ} {s t : K.Idx i}
    (h : altImg K s = altImg K t) : s = t
theorem

altOpen_eq_biInf

L68 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altOpen_eq_biInf
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altOpen_eq_biInf {i : ℕ} (s : K.Idx i) :
    K.inter s = ⨅ j ∈ altImg K s, K.U j
theorem

altImg_altFace

L75 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altImg_altFace
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altImg_altFace {i : ℕ} (s : K.Idx (i + 1))
    (j : Fin (i + 2)) :
    altImg K (K.face s j)
      = (altImg K s).erase (s.1 j)
def

altOfFinset

L90 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altOfFinset
Documentation

The increasing Cech index enumerating a finite set of the required cardinality.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def altOfFinset {i : ℕ} (T : Finset K.ι) (hT : T.card = i + 1) :
    K.Idx i
theorem

altImg_altOfFinset

L94 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altImg_altOfFinset
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altImg_altOfFinset {i : ℕ} (T : Finset K.ι) (hT : T.card = i + 1) :
    altImg K (altOfFinset K T hT) = T
theorem

altImg_deg0

L98 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altImg_deg0
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altImg_deg0 (σ : K.Idx 0) :
    altImg K σ = {σ.1 0}
def

altPos

L105 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altPos
Documentation

The position of a cover index in the increasing Cech index.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def altPos {i : ℕ} (s : K.Idx i) (j : K.ι)
    (hj : j ∈ altImg K s) : Fin (i + 1)
theorem

altIdx_val_altPos

L109 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altIdx_val_altPos
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altIdx_val_altPos {i : ℕ} (s : K.Idx i)
    (j : K.ι) (hj : j ∈ altImg K s) :
    s.1 (altPos K s j hj) = j
theorem

altPos_val

L115 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altPos_val
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altPos_val {i : ℕ} (s : K.Idx i) (p : Fin (i + 1)) :
    altPos K s (s.1 p) (Finset.mem_image_of_mem _ (Finset.mem_univ p)) = p
def

altInsert

L120 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altInsert
Documentation

Insert a new cover index into the increasing Cech index.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def altInsert {i : ℕ} (s : K.Idx i) (j : K.ι)
    (hj : j ∉ altImg K s) : K.Idx (i + 1)
theorem

altImg_altInsert

L125 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altImg_altInsert
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altImg_altInsert {i : ℕ} (s : K.Idx i)
    (j : K.ι) (hj : j ∉ altImg K s) :
    altImg K (altInsert K s j hj)
      = insert j (altImg K s)
def

insPos

L132 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.insPos
Documentation

The position of the newly inserted cover index.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def insPos {i : ℕ} (s : K.Idx i) (j : K.ι)
    (hj : j ∉ altImg K s) : Fin (i + 2)
theorem

altInsert_val_insPos

L137 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altInsert_val_insPos
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altInsert_val_insPos {i : ℕ} (s : K.Idx i)
    (j : K.ι) (hj : j ∉ altImg K s) :
    (altInsert K s j hj).1 (insPos K s j hj) = j
theorem

altFace_altInsert_insPos

L142 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altFace_altInsert_insPos
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altFace_altInsert_insPos {i : ℕ} (s : K.Idx i)
    (j : K.ι) (hj : j ∉ altImg K s) :
    K.face (altInsert K s j hj)
      (insPos K s j hj) = s
theorem

altPos_congr

L150 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altPos_congr
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altPos_congr {i : ℕ} {s t : K.Idx i}
    (h : s = t) (j : K.ι) (hjs : j ∈ altImg K s)
    (hjt : j ∈ altImg K t) :
    altPos K s j hjs = altPos K t j hjt
theorem

altInsert_altFace_altPos

L156 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altInsert_altFace_altPos
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altInsert_altFace_altPos {i : ℕ} (σ : K.Idx (i + 1))
    (j : K.ι) (hj : j ∈ altImg K σ)
    (hjp : j ∉ altImg K
      (K.face σ (altPos K σ j hj))) :
    altInsert K (K.face σ (altPos K σ j hj))
      j hjp = σ
theorem

insPos_altFace_altPos

L166 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.insPos_altFace_altPos
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem insPos_altFace_altPos {i : ℕ} (σ : K.Idx (i + 1))
    (j : K.ι) (hj : j ∈ altImg K σ)
    (hjp : j ∉ altImg K
      (K.face σ (altPos K σ j hj))) :
    insPos K (K.face σ (altPos K σ j hj)) j hjp
      = altPos K σ j hj
theorem

altFace_altInsert_ne

L176 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altFace_altInsert_ne
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AltImg
variable {V : Scheme.{u}} {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altFace_altInsert_ne {i : ℕ} (s : K.Idx (i + 1))
    (j : K.ι) (hj : j ∉ altImg K s)
    (k : Fin (i + 3)) (hk : k ≠ insPos K s j hj) :
    ∃ (p : Fin (i + 2)) (hjp : j ∉ altImg K (K.face s p)),
      K.face (altInsert K s j hj) k
        = altInsert K (K.face s p) j hjp
      ∧ (altInsert K s j hj).1 k = s.1 p
abbrev

cochainOf

L208 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.cochainOf
Documentation

Cochains indexed by the ordered affine cover and valued in intersection sections.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section FCochain
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
abbrev cochainOf (i : ℕ) : Type u
def

dOf

L211 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.dOf
Documentation

The alternating restriction differential on cover-indexed cochains.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section FCochain
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
def dOf (i : ℕ) : cochainOf F K i →ₗ[R] cochainOf F K (i + 1)
theorem

dOf_apply

L215 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.dOf_apply
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section FCochain
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem dOf_apply (i : ℕ) (c : cochainOf F K i) (s : K.Idx (i + 1)) :
    dOf F K i c s = ∑ j : Fin (i + 2), ((-1 : ℤ) ^ (j : ℕ)) • F.res (K.inter_le_inter_face s j) (c
      (K.face s j))
theorem

altC_at_eq

L222 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altC_at_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section FCochain
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem altC_at_eq {n : ℕ} (z : cochainOf F K n) {σ τ : K.Idx n} (h : σ = τ)
    {O : V.Opens} (hσ : O ≤ K.inter σ) (hτ : O ≤ K.inter τ) :
    F.res hσ (z σ) = F.res hτ (z τ)
theorem

res_self

L227 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.res_self
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section FCochain
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
Lean source · statement
theorem res_self {O : V.Opens} (h : O ≤ O) (x : F.obj O) : F.res h x = x
theorem

altOpen_altInsert

L237 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altOpen_altInsert
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
Lean source · statement
theorem altOpen_altInsert {i : ℕ} (s : K.Idx i)
    (hj : i₀ ∉ altImg K s) :
    K.inter (altInsert K s i₀ hj)
      = K.inter s
def

htpy

L260 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.htpy
Documentation

The insertion homotopy associated to a cover member equal to the whole base open.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
Lean source · statement
def htpy (i : ℕ) : cochainOf F K (i + 1) →ₗ[R] cochainOf F K i
theorem

htpy_apply

L267 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.htpy_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
Lean source · full declaration
theorem htpy_apply (i : ℕ) (z : cochainOf F K (i + 1)) (σ : K.Idx i) :
    htpy F K i₀ hi₀ i z σ =
      if hσ : i₀ ∈ altImg K σ then 0
      else ((-1 : ℤ) ^ ((insPos K σ i₀ hσ : ℕ))) •
        F.res (ge_of_eq (altOpen_altInsert K i₀ hi₀ σ hσ)) (z (altInsert K σ i₀ hσ)) := by
  simp only [htpy, LinearMap.pi_apply]
  split_ifs with h
  · rfl
  · simp only [LinearMap.smul_apply, LinearMap.comp_apply, LinearMap.proj_apply]
theorem

notMem_altImg_altFace

L278 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.notMem_altImg_altFace
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
omit hi₀ in
Lean source · statement
theorem notMem_altImg_altFace {i : ℕ} (σ : K.Idx (i + 1))
    (hσ : i₀ ∉ altImg K σ) (p : Fin (i + 2)) :
    i₀ ∉ altImg K (K.face σ p)
theorem

sign_rel

L284 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.sign_rel
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
omit hi₀ in
Lean source · statement
theorem sign_rel {i : ℕ} (σ : K.Idx (i + 1))
    (hσ : i₀ ∉ altImg K σ) (p : Fin (i + 2)) :
    K.face (altInsert K σ i₀ hσ)
        ((insPos K σ i₀ hσ).succAbove p)
      = altInsert K (K.face σ p) i₀
          (notMem_altImg_altFace K i₀ σ hσ p)
    ∧ (insPos K σ i₀ hσ : ℕ)
        + ((insPos K σ i₀ hσ).succAbove p : ℕ)
      = (p : ℕ) + (insPos K (K.face σ p) i₀
          (notMem_altImg_altFace K i₀ σ hσ p) : ℕ) + 1
theorem

htpy_rel

L352 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.htpy_rel
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
Lean source · statement
theorem htpy_rel (i : ℕ) :
    dOf F K i ∘ₗ htpy F K i₀ hi₀ i
      + htpy F K i₀ hi₀ (i + 1) ∘ₗ dOf F K (i + 1)
      = LinearMap.id
theorem

wholeSpace_exact

L401 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.wholeSpace_exact
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section WholeSpace
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W) (i₀ : K.ι) (hi₀ : K.U i₀ = W)
include hi₀
Lean source · statement
theorem wholeSpace_exact (i : ℕ) :
    LinearMap.ker (dOf F K (i + 1)) ≤ LinearMap.range (dOf F K i)
theorem

isAffineOpen_altOpen

L420 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.isAffineOpen_altOpen
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
theorem isAffineOpen_altOpen :
    ∀ {i : ℕ} (σ : K.Idx i),
      IsAffineOpen (K.inter σ)
def

moduleW_altC

L443 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.moduleW_altC
Documentation

The section-ring module structure on cochains induced by intersection restrictions.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
def moduleW_altC (i : ℕ) :
    Module Γ(V, W) (cochainOf F K i)
theorem

smulW_apply

L449 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.smulW_apply
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit [IsSeparated π] in
Lean source · full declaration
theorem smulW_apply {i : ℕ} (a : Γ(V, W)) (x : cochainOf F K i)
    (σ : K.Idx i) :
    letI := moduleW_altC π F K i
    (a • x) σ = (V.presheaf.map (homOfLE (K.inter_le_base σ)).op).hom a • x σ :=
  rfl
theorem

resΓ_resΓ

L456 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.resΓ_resΓ
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit π [IsSeparated π] in
Lean source · statement
theorem resΓ_resΓ {O₁ O₂ O₃ : V.Opens} (h12 : O₁ ≤ O₂) (h23 : O₂ ≤ O₃) (x : Γ(V, O₃)) :
    (V.presheaf.map (homOfLE h12).op).hom ((V.presheaf.map (homOfLE h23).op).hom x)
      = (V.presheaf.map (homOfLE (h12.trans h23)).op).hom x
theorem

resΓ_pow_resΓ

L462 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.resΓ_pow_resΓ
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit π [IsSeparated π] in
Lean source · statement
theorem resΓ_pow_resΓ {O₁ O₂ O₃ : V.Opens} (h12 : O₁ ≤ O₂) (h23 : O₂ ≤ O₃) (x : Γ(V, O₃)) (N : ℕ) :
    (V.presheaf.map (homOfLE h12).op).hom ((V.presheaf.map (homOfLE h23).op).hom x ^ N)
      = (V.presheaf.map (homOfLE (h12.trans h23)).op).hom x ^ N
theorem

altd_smulW

L468 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altd_smulW
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit [IsSeparated π] in
Lean source · full declaration
theorem altd_smulW (i : ℕ) (a : Γ(V, W)) (x : cochainOf F K i) :
    letI := moduleW_altC π F K i
    letI := moduleW_altC π F K (i + 1)
    dOf F K i (a • x) = a • dOf F K i x := by
  funext τ
  rw [dOf_apply, smulW_apply, dOf_apply, Finset.smul_sum]
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [smulW_apply, F.res_smul, resΓ_resΓ, smul_comm]
def

rangeW

L478 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.rangeW
Documentation

The range of the differential as a module over sections on the base open.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · full declaration
def rangeW (p : ℕ) :
    letI := moduleW_altC π F K (p + 1)
    Submodule (V.presheaf.obj (Opposite.op W)) (cochainOf F K (p + 1)) :=
  letI := moduleW_altC π F K (p + 1)
  letI := moduleW_altC π F K p
  { carrier := Set.range (dOf F K p)
    add_mem' := fun ⟨w₁, h₁⟩ ⟨w₂, h₂⟩ => ⟨w₁ + w₂, by rw [map_add, h₁, h₂]⟩
    zero_mem' := ⟨0, map_zero _⟩
    smul_mem' := fun a _ ⟨w, hw⟩ =>
      ⟨a • w, (altd_smulW π F K p a w).trans (congrArg (a • ·) hw)⟩ }
def

restrictBasic

L490 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.restrictBasic
Documentation

Restrict the ordered affine cover to the specified basic open.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
def restrictBasic (hW : IsAffineOpen W) (f : Γ(V, W)) :
    Scheme.OrderedAffineCoverOf (V.basicOpen f)
theorem

altOpen_restrictBasic

L499 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altOpen_restrictBasic
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
theorem altOpen_restrictBasic (hW : IsAffineOpen W) (f : Γ(V, W))
    {i : ℕ} (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) i) :
    Scheme.OrderedAffineCoverOf.inter (restrictBasic π K hW f) σ
      = K.inter σ ⊓ V.basicOpen f
theorem

altOpen_restrictBasic_le

L506 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altOpen_restrictBasic_le
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
theorem altOpen_restrictBasic_le (hW : IsAffineOpen W) (f : Γ(V, W))
    {i : ℕ} (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) i) :
    Scheme.OrderedAffineCoverOf.inter (restrictBasic π K hW f) σ
      ≤ K.inter σ
def

resBasic

L513 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.resBasic
Documentation

Restrict each cochain component to the intersections with the specified basic open.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
def resBasic (hW : IsAffineOpen W) (f : Γ(V, W)) (q : ℕ) :
    cochainOf F K q →ₗ[R] cochainOf F (restrictBasic π K hW f) q
theorem

resBasic_apply

L520 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.resBasic_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
theorem resBasic_apply (hW : IsAffineOpen W) (f : Γ(V, W)) (q : ℕ)
    (x : cochainOf F K q)
    (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) q) :
    resBasic π F K hW f q x σ = F.res (altOpen_restrictBasic_le π K hW f σ) (x σ)
theorem

altd_resBasic

L527 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.altd_resBasic
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
theorem altd_resBasic (hW : IsAffineOpen W) (f : Γ(V, W)) (q : ℕ)
    (x : cochainOf F K q) :
    dOf F (restrictBasic π K hW f) q (resBasic π F K hW f q x)
      = resBasic π F K hW f (q + 1) (dOf F K q x)
theorem

away_surj

L538 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.away_surj
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
theorem away_surj (hF : F.IsQuasicoherent) (hW : IsAffineOpen W) (f : Γ(V, W))
    {q : ℕ} (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) q)
    (y : F.obj (Scheme.OrderedAffineCoverOf.inter (restrictBasic π K hW f) σ)) :
    ∃ (n : ℕ) (a : F.obj (K.inter σ)),
      F.res (altOpen_restrictBasic_le π K hW f σ) a
        = (V.presheaf.map (homOfLE
            (((altOpen_restrictBasic π K hW f σ).le.trans inf_le_right).trans
              (V.basicOpen_le f))).op).hom f ^ n • y
theorem

away_ker

L556 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.away_ker
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
theorem away_ker (hF : F.IsQuasicoherent) (hW : IsAffineOpen W) (f : Γ(V, W))
    {q : ℕ} (σ : Scheme.OrderedAffineCoverOf.Idx (restrictBasic π K hW f) q)
    (x : F.obj (K.inter σ))
    (hx : F.res (altOpen_restrictBasic_le π K hW f σ) x = 0) :
    ∃ m : ℕ,
      ((V.presheaf.map (homOfLE (K.inter_le_base σ)).op).hom f ^ m) • x = 0
theorem

exists_refinement

L572 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.exists_refinement
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
omit π in
Lean source · statement
theorem exists_refinement (hW : IsAffineOpen W) :
    ∃ (s : Set Γ(V, W)) (ι : s → K.ι),
      Ideal.span s = ⊤ ∧ ∀ r : s, V.basicOpen (r : Γ(V, W)) ≤ K.U (ι r)
theorem

smul_pow_mem_range

L589 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.smul_pow_mem_range
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · full declaration
theorem smul_pow_mem_range (hF : F.IsQuasicoherent) (hW : IsAffineOpen W)
    (f : Γ(V, W)) (i₀ : K.ι) (hfi : V.basicOpen f ≤ K.U i₀)
    (p : ℕ) (z : cochainOf F K (p + 1))
    (hz : dOf F K (p + 1) z = 0) :
    letI := moduleW_altC π F K (p + 1)
    ∃ N : ℕ, f ^ N • z ∈ rangeW π F K p := by
  let := moduleW_altC π F K (p + 1)
  let := moduleW_altC π F K p
  set Kf := restrictBasic π K hW f with hKf
  have hi₀f : Kf.U i₀ = V.basicOpen f := inf_eq_right.mpr hfi
  have hzf : dOf F Kf (p + 1) (resBasic π F K hW f (p + 1) z) = 0 := by
    rw [altd_resBasic, hz, map_zero]
  obtain ⟨w, hw⟩ := wholeSpace_exact F Kf i₀ hi₀f p (LinearMap.mem_ker.mpr hzf)
  choose nσ aσ haσ using fun σ => away_surj π F K hF hW f σ (w σ)
  set N₁ : ℕ := Finset.univ.sup nσ with hN₁
  have hN₁le : ∀ σ, nσ σ ≤ N₁ := fun σ => Finset.le_sup (Finset.mem_univ σ)
  set a : cochainOf F K p := fun σ =>
    ((V.presheaf.map (homOfLE (K.inter_le_base σ)).op).hom f ^ (N₁ - nσ σ)) • aσ σ
    with ha_def
  have hresA : ∀ σ, resBasic π F K hW f p a σ
      = ((V.presheaf.map (homOfLE (((altOpen_restrictBasic π K hW f σ).le.trans
          inf_le_right).trans (V.basicOpen_le f))).op).hom f ^ N₁) • w σ := by
    intro σ
    rw [resBasic_apply, ha_def, F.res_smul, map_pow, resΓ_resΓ,
      haσ σ, smul_smul, ← pow_add, Nat.sub_add_cancel (hN₁le σ)]
  have hstep : resBasic π F K hW f (p + 1) (dOf F K p a)
      = resBasic π F K hW f (p + 1) (f ^ N₁ • z) := by
    rw [← altd_resBasic]
    funext τ
    rw [dOf_apply, resBasic_apply]
    erw [smulW_apply π F K (f ^ N₁) z (show K.Idx (p + 1) from τ)]
    rw [F.res_smul, map_pow, resΓ_pow_resΓ]
    have hwτ := congrFun hw τ
    rw [dOf_apply, resBasic_apply] at hwτ
    rw [← hwτ, Finset.smul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [hresA, F.res_smul, resΓ_pow_resΓ, smul_comm]
  have hker : ∀ τ : K.Idx (p + 1), ∃ m : ℕ,
      ((V.presheaf.map (homOfLE (K.inter_le_base τ)).op).hom f ^ m)
        • (dOf F K p a τ - (f ^ N₁ • z) τ) = 0 := by
    intro τ
    refine away_ker π F K hF hW f τ _ ?_
    have := congrFun hstep τ
    erw [resBasic_apply, resBasic_apply] at this
    rw [map_sub, this, sub_self]
  choose mτ hmτ using hker
  set N₂ : ℕ := Finset.univ.sup mτ
  refine ⟨N₁ + N₂, f ^ N₂ • a, ?_⟩
  rw [altd_smulW]
  funext τ
  rw [smulW_apply, smulW_apply, map_pow, map_pow]
  have hN₂le : mτ τ ≤ N₂ := Finset.le_sup (f := mτ) (Finset.mem_univ τ)
  have key := hmτ τ
  rw [smulW_apply, map_pow] at key
  have key2 : ((V.presheaf.map (homOfLE (K.inter_le_base τ)).op).hom f ^ N₂)
      • (dOf F K p a τ
        - ((V.presheaf.map (homOfLE (K.inter_le_base τ)).op).hom f ^ N₁) • z τ)
      = 0 := by
    conv_lhs => rw [← Nat.sub_add_cancel hN₂le, pow_add, mul_smul, key]
    exact smul_zero _
  rw [smul_sub, smul_smul, ← pow_add, sub_eq_zero, add_comm N₂ N₁] at key2
  exact key2
theorem

affine_acyclic

L652 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry.OModulePresheaf.AffineAcyclicF.affine_acyclic
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace AffineAcyclicF
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
section AffineAcyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R))
variable [IsSeparated π] (F : OModulePresheaf π) {W : V.Opens} (K : Scheme.OrderedAffineCoverOf W)
include π
Lean source · statement
theorem affine_acyclic (hF : F.IsQuasicoherent) (hW : IsAffineOpen W) (p : ℕ) :
    LinearMap.ker (dOf F K (p + 1)) ≤ LinearMap.range (dOf F K p)
theorem

ker_d_succ_le_range_d_of_isQuasicoherent

L673 ↗
AlgebraicGeometry.OModulePresheaf.ker_d_succ_le_range_d_of_isQuasicoherent
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.Opposite
universe u
open _root_.AlgebraicCurves.Cohomology.Sheaves.Proofs in
open _root_.AlgebraicGeometry
  OModulePresheaf_ker_d_succ_le_range_d_of_isQuasicoherent.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.ker_d_succ_le_range_d_of_isQuasicoherent
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsAffine V] [IsSeparated π]
    (F : OModulePresheaf π) (hF : F.IsQuasicoherent) (K : V.OrderedAffineCover) (i : ℕ) :
    LinearMap.ker (F.d K (i + 1)) ≤ LinearMap.range (F.d K i)

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