NYLL
Module

OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
51 declarations indexed from sourceView source ↗

Module documentation

Independence of degree-one cohomology from the ordered affine cover.

Imports3
Imported by3

Declarations

def

rs

L48 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs
Documentation

Restriction of a module section along an inclusion of open sets.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
def rs {U V : X.Opens} (h : V ≤ U) (x : Γ(M, U)) : Γ(M, V)
theorem

rs_def

L50 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_def
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_def {U V : X.Opens} (h : V ≤ U) (x : Γ(M, U)) : rs M h x = M.presheaf.map (homOfLE h).op
  x
theorem

rs_rs

L53 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_rs
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_rs {U V W : X.Opens} (h : V ≤ U) (h' : W ≤ V) (x : Γ(M, U)) : rs M h' (rs M h x) = rs M
  (h'.trans h) x
theorem

rs_irrel

L57 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_irrel
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_irrel {U V : X.Opens} (h h' : V ≤ U) (x : Γ(M, U)) : rs M h x = rs M h' x
theorem

rs_refl

L59 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_refl
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_refl {U : X.Opens} (x : Γ(M, U)) : rs M (le_refl U) x = x
theorem

rs_sub

L63 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_sub
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_sub {U V : X.Opens} (h : V ≤ U) (x y : Γ(M, U)) : rs M h (x - y) = rs M h x - rs M h y
theorem

rs_add

L65 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_add
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_add {U V : X.Opens} (h : V ≤ U) (x y : Γ(M, U)) : rs M h (x + y) = rs M h x + rs M h y
theorem

rs_zero

L67 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_zero
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_zero {U V : X.Opens} (h : V ≤ U) : rs M h (0 : Γ(M, U)) = 0
theorem

rs_neg

L68 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_neg
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_neg {U V : X.Opens} (h : V ≤ U) (x : Γ(M, U)) : rs M h (-x) = -rs M h x
theorem

rs_injective_of_eq

L70 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_injective_of_eq
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem rs_injective_of_eq {U V : X.Opens} (e : V = U) : Function.Injective (rs M e.le)
def

sh

L76 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.sh
Documentation

The underlying sheaf of abelian groups of the module sheaf.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
def sh : TopCat.Sheaf Ab X.carrier
theorem

glue

L78 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.glue
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem glue {ι : Type u} (Q : ι → X.Opens) {V : X.Opens} (hQ : ∀ i, Q i ≤ V) (hcov : V ≤ ⨆ i, Q i)
    (x : ∀ i, Γ(M, Q i))
    (hx : ∀ i j, rs M (inf_le_left : Q i ⊓ Q j ≤ Q i) (x i) = rs M (inf_le_right : Q i ⊓ Q j ≤ Q j)
      (x j)) :
    ∃ s : Γ(M, V), ∀ i, rs M (hQ i) s = x i
theorem

locality

L96 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.locality
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Rs
variable (M : X.Modules)
Lean source · statement
theorem locality {ι : Type u} (Q : ι → X.Opens) {V : X.Opens} (hQ : ∀ i, Q i ≤ V) (hcov : V ≤ ⨆ i,
  Q i)
    (s t : Γ(M, V)) (h : ∀ i, rs M (hQ i) s = rs M (hQ i) t) : s = t
def

idx0

L107 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.idx0
Documentation

The zero-simplex at a cover index.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
def idx0 (a : K.ι) : K.Idx 0
def

idx1

L111 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.idx1
Documentation

The one-simplex formed by two increasing cover indices.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
def idx1 {a b : K.ι} (hab : a < b) : K.Idx 1
def

idx2

L121 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.idx2
Documentation

The two-simplex formed by three increasing cover indices.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
def idx2 {a b c : K.ι} (hab : a < b) (hbc : b < c) : K.Idx 2
theorem

inter_idx0_le

L135 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.inter_idx0_le
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem inter_idx0_le (a : K.ι) : K.inter (idx0 K a) ≤ K.U a
theorem

le_inter_idx0

L136 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.le_inter_idx0
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem le_inter_idx0 (a : K.ι) : K.U a ≤ K.inter (idx0 K a)
theorem

inter_le_pair

L138 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.inter_le_pair
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem inter_le_pair (s : K.Idx 1) : K.inter s ≤ K.U (s.1 0) ⊓ K.U (s.1 1)
theorem

pair_le_inter

L141 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.pair_le_inter
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem pair_le_inter (s : K.Idx 1) : K.U (s.1 0) ⊓ K.U (s.1 1) ≤ K.inter s
theorem

inter_pair_eq

L147 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.inter_pair_eq
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem inter_pair_eq (s : K.Idx 1) : K.inter s = K.U (s.1 0) ⊓ K.U (s.1 1)
theorem

inter_le_triple

L150 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.inter_le_triple
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem inter_le_triple (t : K.Idx 2) : K.inter t ≤ K.U (t.1 0) ⊓ K.U (t.1 1) ⊓ K.U (t.1 2)
theorem

lt01

L153 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.lt01
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem lt01 (s : K.Idx 1) : s.1 0 < s.1 1
theorem

lt01'

L154 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.lt01'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem lt01' (t : K.Idx 2) : t.1 0 < t.1 1
theorem

lt12'

L155 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.lt12'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem lt12' (t : K.Idx 2) : t.1 1 < t.1 2
theorem

face_idx1_zero

L157 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.face_idx1_zero
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem face_idx1_zero {a b : K.ι} (hab : a < b) : K.face (idx1 K hab) 0 = idx0 K b
theorem

face_idx1_one

L160 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.face_idx1_one
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem face_idx1_one {a b : K.ι} (hab : a < b) : K.face (idx1 K hab) 1 = idx0 K a
theorem

eq_idx1

L163 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.eq_idx1
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem eq_idx1 (s : K.Idx 1) : s = idx1 K (lt01 K s)
theorem

face1_val

L166 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.face1_val
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem face1_val (s : K.Idx 1) (j : Fin 2) : (K.face s j).1 0 = s.1 (j.succAbove 0)
theorem

face2_val

L167 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.face2_val
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Idx
variable (K : X.OrderedAffineCover)
Lean source · statement
theorem face2_val (t : K.Idx 2) (j : Fin 3) (k : Fin 2) : (K.face t j).1 k = t.1 (j.succAbove k)
theorem

res_eq_rs

L175 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.res_eq_rs
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Dif
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) (M : X.Modules) (K : X.OrderedAffineCover)
Lean source · full declaration
theorem res_eq_rs {O O' : X.Opens} (h : O ≤ O') (x : Γ(M, O')) :
    (OModulePresheaf.ofModules π M).res h (show (OModulePresheaf.ofModules π M).obj O' from x) = rs
      M h x := rfl
theorem

d_zero_apply

L179 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.d_zero_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Dif
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) (M : X.Modules) (K : X.OrderedAffineCover)
Lean source · statement
theorem d_zero_apply (e : (OModulePresheaf.ofModules π M).cochain K 0) (s : K.Idx 1) :
    (OModulePresheaf.ofModules π M).d K 0 e s
      = rs M (K.inter_le_inter_face s 0) (e (K.face s 0)) - rs M (K.inter_le_inter_face s 1) (e
        (K.face s 1))
theorem

d_one_apply

L188 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.d_one_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Dif
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) (M : X.Modules) (K : X.OrderedAffineCover)
Lean source · statement
theorem d_one_apply (c : (OModulePresheaf.ofModules π M).cochain K 1) (t : K.Idx 2) :
    (OModulePresheaf.ofModules π M).d K 1 c t
      = rs M (K.inter_le_inter_face t 0) (c (K.face t 0)) - rs M (K.inter_le_inter_face t 1) (c
        (K.face t 1))
        + rs M (K.inter_le_inter_face t 2) (c (K.face t 2))
theorem

rs_at_eq

L198 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_at_eq
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Dif
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) (M : X.Modules) (K : X.OrderedAffineCover)
Lean source · statement
theorem rs_at_eq {i : ℕ} (c : (OModulePresheaf.ofModules π M).cochain K i) {σ τ : K.Idx i} (e : σ =
  τ)
    {O : X.Opens} (hσ : O ≤ K.inter σ) (hτ : O ≤ K.inter τ) :
    rs M hσ (c σ) = rs M hτ (c τ)
def

cm

L205 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.cm
Documentation

The component of a one-cochain restricted to a pairwise intersection.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Dif
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) (M : X.Modules) (K : X.OrderedAffineCover)
Lean source · statement
def cm (c : (OModulePresheaf.ofModules π M).cochain K 1) {a b : K.ι} (hab : a < b) : Γ(M, K.U a ⊓
  K.U b)
theorem

rs_cm

L209 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.rs_cm
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Dif
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) (M : X.Modules) (K : X.OrderedAffineCover)
Lean source · statement
theorem rs_cm (c : (OModulePresheaf.ofModules π M).cochain K 1) (s : K.Idx 1) :
    rs M (inter_le_pair K s) (cm π M K c (lt01 K s)) = c s
theorem

cocycle

L214 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.cocycle
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Dif
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) (M : X.Modules) (K : X.OrderedAffineCover)
Lean source · statement
theorem cocycle (c : (OModulePresheaf.ofModules π M).cochain K 1) (hc : (OModulePresheaf.ofModules
  π M).d K 1 c = 0)
    {a b e : K.ι} (hab : a < b) (hbe : b < e) :
    rs M (le_inf (inf_le_left.trans inf_le_right) inf_le_right : K.U a ⊓ K.U b ⊓ K.U e ≤ K.U b ⊓
      K.U e) (cm π M K c hbe)
      - rs M (le_inf (inf_le_left.trans inf_le_left) inf_le_right : K.U a ⊓ K.U b ⊓ K.U e ≤ K.U a ⊓
        K.U e)
          (cm π M K c (hab.trans hbe))
      + rs M (inf_le_left : K.U a ⊓ K.U b ⊓ K.U e ≤ K.U a ⊓ K.U b) (cm π M K c hab) = 0
theorem

isAffineOpen_inf

L270 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.isAffineOpen_inf
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
include π in
Lean source · statement
theorem isAffineOpen_inf {P Q : X.Opens} (hP : IsAffineOpen P) (hQ : IsAffineOpen Q) : IsAffineOpen
  (P ⊓ Q)
theorem

cover_by_K'

L275 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.cover_by_K'
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
omit [IsSeparated π] in
Lean source · statement
theorem cover_by_K' (W : X.Opens) : W ≤ ⨆ k, W ⊓ K'.U k
theorem

cover_by_K

L278 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.cover_by_K
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
omit [IsSeparated π] in
Lean source · statement
theorem cover_by_K (W : X.Opens) : W ≤ ⨆ a, K.U a ⊓ W
theorem

step1

L281 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.step1
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
include htriv in
Lean source · statement
theorem step1 (c : (OModulePresheaf.ofModules π M).cochain K' 1) (hc : (OModulePresheaf.ofModules π
  M).d K' 1 c = 0)
    (a : K.ι) :
    ∃ v : ∀ k : K'.ι, Γ(M, K.U a ⊓ K'.U k), ∀ k l : K'.ι, ∀ hkl : k < l,
      rs M (le_inf (inf_le_left.trans inf_le_right) (inf_le_right.trans inf_le_right) :
          (K.U a ⊓ K'.U k) ⊓ (K.U a ⊓ K'.U l) ≤ K'.U k ⊓ K'.U l) (cm π M K' c hkl)
        = rs M inf_le_right (v l) - rs M inf_le_left (v k)
theorem

compat_of_lt

L314 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.compat_of_lt
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
Lean source · statement
theorem compat_of_lt {ι : Type u} [LinearOrder ι] (Q : ι → X.Opens) (x : ∀ i, Γ(M, Q i))
    (h : ∀ i j, i < j → rs M (inf_le_left : Q i ⊓ Q j ≤ Q i) (x i) = rs M (inf_le_right : Q i ⊓ Q j
      ≤ Q j) (x j)) :
    ∀ i j, rs M (inf_le_left : Q i ⊓ Q j ≤ Q i) (x i) = rs M (inf_le_right : Q i ⊓ Q j ≤ Q j) (x j)
theorem

step2

L327 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.step2
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
omit [IsSeparated π] in
Lean source · statement
theorem step2 (c : (OModulePresheaf.ofModules π M).cochain K' 1)
    (v : ∀ (a : K.ι) (k : K'.ι), Γ(M, K.U a ⊓ K'.U k))
    (hv : ∀ (a : K.ι) (k l : K'.ι) (hkl : k < l),
      rs M (le_inf (inf_le_left.trans inf_le_right) (inf_le_right.trans inf_le_right) :
          (K.U a ⊓ K'.U k) ⊓ (K.U a ⊓ K'.U l) ≤ K'.U k ⊓ K'.U l) (cm π M K' c hkl)
        = rs M inf_le_right (v a l) - rs M inf_le_left (v a k))
    (a b : K.ι) :
    ∃ δ : Γ(M, K.U a ⊓ K.U b), ∀ k : K'.ι,
      rs M (inf_le_left : (K.U a ⊓ K.U b) ⊓ K'.U k ≤ K.U a ⊓ K.U b) δ
        = rs M (le_inf (inf_le_left.trans inf_le_right) inf_le_right : (K.U a ⊓ K.U b) ⊓ K'.U k ≤
          K.U b ⊓ K'.U k) (v b k)
          - rs M (le_inf (inf_le_left.trans inf_le_left) inf_le_right : (K.U a ⊓ K.U b) ⊓ K'.U k ≤
            K.U a ⊓ K'.U k) (v a k)
def

δK

L367 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.δK
Documentation

The one-cochain obtained by restricting sections on pairwise intersections.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
Lean source · statement
def δK (δ : ∀ a b : K.ι, Γ(M, K.U a ⊓ K.U b)) : (OModulePresheaf.ofModules π M).cochain K 1
theorem

step3

L371 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.step3
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
omit [IsSeparated π] in
Lean source · statement
theorem step3 (v : ∀ (a : K.ι) (k : K'.ι), Γ(M, K.U a ⊓ K'.U k)) (δ : ∀ a b : K.ι, Γ(M, K.U a ⊓ K.U
  b))
    (hδ : ∀ (a b : K.ι) (k : K'.ι),
      rs M (inf_le_left : (K.U a ⊓ K.U b) ⊓ K'.U k ≤ K.U a ⊓ K.U b) (δ a b)
        = rs M (le_inf (inf_le_left.trans inf_le_right) inf_le_right : (K.U a ⊓ K.U b) ⊓ K'.U k ≤
          K.U b ⊓ K'.U k) (v b k)
          - rs M (le_inf (inf_le_left.trans inf_le_left) inf_le_right : (K.U a ⊓ K.U b) ⊓ K'.U k ≤
            K.U a ⊓ K'.U k) (v a k)) :
    (OModulePresheaf.ofModules π M).d K 1 (δK π M K δ) = 0
theorem

step4

L410 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.step4
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
omit [IsSeparated π] in
Lean source · statement
theorem step4 (h : Subsingleton ((OModulePresheaf.ofModules π M).HSucc K 0))
    (δ : ∀ a b : K.ι, Γ(M, K.U a ⊓ K.U b)) (hd : (OModulePresheaf.ofModules π M).d K 1 (δK π M K δ)
      = 0) :
    ∃ η : ∀ a : K.ι, Γ(M, K.U a), ∀ a b : K.ι, a < b →
      δ a b = rs M inf_le_right (η b) - rs M inf_le_left (η a)
theorem

step5

L451 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.step5
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
Lean source · statement
theorem step5 (v : ∀ (a : K.ι) (k : K'.ι), Γ(M, K.U a ⊓ K'.U k)) (δ : ∀ a b : K.ι, Γ(M, K.U a ⊓ K.U
  b))
    (hδ : ∀ (a b : K.ι) (k : K'.ι),
      rs M (inf_le_left : (K.U a ⊓ K.U b) ⊓ K'.U k ≤ K.U a ⊓ K.U b) (δ a b)
        = rs M (le_inf (inf_le_left.trans inf_le_right) inf_le_right : (K.U a ⊓ K.U b) ⊓ K'.U k ≤
          K.U b ⊓ K'.U k) (v b k)
          - rs M (le_inf (inf_le_left.trans inf_le_left) inf_le_right : (K.U a ⊓ K.U b) ⊓ K'.U k ≤
            K.U a ⊓ K'.U k) (v a k))
    (η : ∀ a : K.ι, Γ(M, K.U a))
    (hη : ∀ a b : K.ι, a < b → δ a b = rs M inf_le_right (η b) - rs M inf_le_left (η a)) (k : K'.ι)
      :
    ∃ e : Γ(M, K'.U k), ∀ a : K.ι,
      rs M (inf_le_right : K.U a ⊓ K'.U k ≤ K'.U k) e = v a k - rs M inf_le_left (η a)
theorem

step6

L481 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.step6
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
omit [IsSeparated π] in
Lean source · statement
theorem step6 (c : (OModulePresheaf.ofModules π M).cochain K' 1)
    (v : ∀ (a : K.ι) (k : K'.ι), Γ(M, K.U a ⊓ K'.U k))
    (hv : ∀ (a : K.ι) (k l : K'.ι) (hkl : k < l),
      rs M (le_inf (inf_le_left.trans inf_le_right) (inf_le_right.trans inf_le_right) :
          (K.U a ⊓ K'.U k) ⊓ (K.U a ⊓ K'.U l) ≤ K'.U k ⊓ K'.U l) (cm π M K' c hkl)
        = rs M inf_le_right (v a l) - rs M inf_le_left (v a k))
    (η : ∀ a : K.ι, Γ(M, K.U a)) (e : ∀ k : K'.ι, Γ(M, K'.U k))
    (he : ∀ (k : K'.ι) (a : K.ι),
      rs M (inf_le_right : K.U a ⊓ K'.U k ≤ K'.U k) (e k) = v a k - rs M inf_le_left (η a))
    {k l : K'.ι} (hkl : k < l) :
    rs M inf_le_right (e l) - rs M inf_le_left (e k) = cm π M K' c hkl
theorem

chase

L509 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.chase
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
include htriv in
Lean source · statement
theorem chase (h : Subsingleton ((OModulePresheaf.ofModules π M).HSucc K 0))
    (c : (OModulePresheaf.ofModules π M).cochain K' 1) (hc : (OModulePresheaf.ofModules π M).d K' 1
      c = 0) :
    ∃ eK : (OModulePresheaf.ofModules π M).cochain K' 0, (OModulePresheaf.ofModules π M).d K' 0 eK
      = c
theorem

main

L530 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton.AlgebraicGeometry.OModulePresheaf.CoverIndepH1.main
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace CoverIndepH1
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Chase
variable {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R)) [IsSeparated π] (M : X.Modules)
  (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
    Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
  (K K' : X.OrderedAffineCover)
include htriv in
Lean source · statement
theorem main (h : Subsingleton ((OModulePresheaf.ofModules π M).HSucc K 0)) :
    Subsingleton ((OModulePresheaf.ofModules π M).HSucc K' 0)
theorem

subsingleton_HSucc_zero_ofModules_of_subsingleton

L543 ↗
AlgebraicGeometry.OModulePresheaf.subsingleton_HSucc_zero_ofModules_of_subsingleton
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_zero_ofModules_of_subsingleton
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
noncomputable section
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.subsingleton_HSucc_zero_ofModules_of_subsingleton
    {R : Type u} [CommRing R] {X : Scheme.{u}} (π : X ⟶ Spec (.of R)) [IsSeparated π] (M :
      X.Modules)
    (htriv : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧
      Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
    (K K' : X.OrderedAffineCover) (h : Subsingleton ((OModulePresheaf.ofModules π M).HSucc K 0)) :
    Subsingleton ((OModulePresheaf.ofModules π M).HSucc K' 0)

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