NYLL
Module

OModulePresheaf_cechFinite_toOrderedAffineCover_iff.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
50 declarations indexed from sourceView source ↗

Module documentation

Comparison of two-chart Cech cohomology with the associated ordered affine cover.

Imports2
Imported by13

Declarations

def

idx0

L49 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.idx0
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
Lean source · statement
def _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.idx0 (i : ULift.{u} (Fin 2)) :
    (K).Idx 0
def

idx01

L54 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.idx01
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
def _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.idx01 : (K).Idx 1
theorem

idx0_val

L60 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.Scheme.TwoAffineOpenCover.idx0_val
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem idx0_val (i : ULift.{u} (Fin 2)) (j : Fin 1) : (𝒱.idx0 i).1 j = i
theorem

eq_idx0

L62 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.eq_idx0
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.eq_idx0 (s : (K).Idx 0) : s =
    𝒱.idx0 (s.1 0)
def

idxZeroEquiv

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.Scheme.TwoAffineOpenCover.idxZeroEquiv
Documentation

The equivalence between degree zero cochain indices and the two affine charts.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · full declaration
def idxZeroEquiv : (K).Idx 0 ≃ ULift.{u} (Fin 2) where
  toFun s := s.1 0
  invFun := 𝒱.idx0
  left_inv s := (𝒱.eq_idx0 s).symm
  right_inv _ := rfl
theorem

eq_idx01

L75 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.eq_idx01
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.eq_idx01 (s : (K).Idx 1) : s =
    𝒱.idx01
instance

uniqueIdxOne

L89 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.Scheme.TwoAffineOpenCover.uniqueIdxOne
Documentation

The unique degree one cochain index of the ordered cover with two affine charts.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · full declaration
instance uniqueIdxOne : Unique ((K).Idx 1) where
  default := 𝒱.idx01
  uniq := 𝒱.eq_idx01
theorem

isEmpty_Idx_add_two

L93 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.isEmpty_Idx_add_two
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.isEmpty_Idx_add_two (i : ℕ) :
    IsEmpty ((K).Idx (i + 2))
theorem

inter_idx0

L104 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.inter_idx0
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.inter_idx0 (i : ULift.{u} (Fin
    2)) : (K).inter (𝒱.idx0 i) = (K).U i
theorem

inter_idx01

L109 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.inter_idx01
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.inter_idx01 : (K).inter 𝒱.idx01
    = 𝒱.U0 ⊓ 𝒱.U1
def

resEq

L121 ↗
AlgebraicGeometry.OModulePresheaf.resEq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · full declaration
def _root_.AlgebraicGeometry.OModulePresheaf.resEq {U U' : X.Opens} (h : U = U') : F.obj
    U' ≃ₗ[R] F.obj U where
  toLinearMap := F.res h.le
  invFun := F.res h.ge
  left_inv x := by
    change F.res h.ge (F.res h.le x) = x
    rw [F.res_res]; exact F.res_refl_apply _ x
  right_inv x := by
    change F.res h.le (F.res h.ge x) = x
    rw [F.res_res]; exact F.res_refl_apply _ x
theorem

resEq_apply

L133 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.resEq_apply
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem resEq_apply {U U' : X.Opens} (h : U = U') (x : F.obj U') : F.resEq h x = F.res h.le x
theorem

res_resEq

L135 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.res_resEq
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem res_resEq {U U' W : X.Opens} (h : U = U') (hW : W ≤ U) (x : F.obj U') :
    F.res hW (F.resEq h x) = F.res (hW.trans h.le) x
def

pick

L141 ↗
AlgebraicGeometry.OModulePresheaf.pick
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
Lean source · full declaration
def _root_.AlgebraicGeometry.OModulePresheaf.pick (p : F.obj 𝒱.U0 × F.obj 𝒱.U1) : ∀ i :
    ULift.{u} (Fin 2), F.obj ((K).U i)
  | ⟨⟨0, _⟩⟩ => p.1
  | ⟨⟨1, _⟩⟩ => p.2
theorem

pick_zero

L147 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.pick_zero
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem pick_zero (p : F.obj 𝒱.U0 × F.obj 𝒱.U1) : F.pick 𝒱 p ⟨0⟩ = p.1
theorem

pick_one

L148 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.pick_one
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem pick_one (p : F.obj 𝒱.U0 × F.obj 𝒱.U1) : F.pick 𝒱 p ⟨1⟩ = p.2
theorem

pick_add

L150 ↗
AlgebraicGeometry.OModulePresheaf.pick_add
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.pick_add (p q : F.obj 𝒱.U0 × F.obj 𝒱.U1)
    (i : ULift.{u} (Fin 2)) :
    F.pick 𝒱 (p + q) i = F.pick 𝒱 p i + F.pick 𝒱 q i
theorem

pick_smul

L159 ↗
AlgebraicGeometry.OModulePresheaf.pick_smul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.pick_smul (r : R) (p : F.obj 𝒱.U0 × F.obj
    𝒱.U1) (i : ULift.{u} (Fin 2)) :
    F.pick 𝒱 (r • p) i = r • F.pick 𝒱 p i
def

pickₗ

L169 ↗
AlgebraicGeometry.OModulePresheaf.pickₗ
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · full declaration
def _root_.AlgebraicGeometry.OModulePresheaf.pickₗ (i : ULift.{u} (Fin 2)) : F.obj 𝒱.U0 ×
    F.obj 𝒱.U1 →ₗ[R] F.obj ((K).U i) where
  toFun p := F.pick 𝒱 p i
  map_add' p q := F.pick_add 𝒱 p q i
  map_smul' r p := F.pick_smul 𝒱 r p i
def

cochainZeroTo

L177 ↗
AlgebraicGeometry.OModulePresheaf.cochainZeroTo
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.cochainZeroTo : F.cochain K 0 →ₗ[R] F.obj
    𝒱.U0 × F.obj 𝒱.U1
def

cochainZeroOf

L184 ↗
AlgebraicGeometry.OModulePresheaf.cochainZeroOf
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.cochainZeroOf : F.obj 𝒱.U0 × F.obj 𝒱.U1 →ₗ[R]
    F.cochain K 0
theorem

cochainZeroTo_apply

L189 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.cochainZeroTo_apply
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem cochainZeroTo_apply (f : F.cochain K 0) :
    F.cochainZeroTo 𝒱 f
      = (F.res (𝒱.inter_idx0 ⟨0⟩).ge (f (𝒱.idx0 ⟨0⟩)), F.res (𝒱.inter_idx0 ⟨1⟩).ge (f (𝒱.idx0
        ⟨1⟩)))
theorem

cochainZeroOf_apply

L195 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.cochainZeroOf_apply
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem cochainZeroOf_apply (p : F.obj 𝒱.U0 × F.obj 𝒱.U1) (s : (K).Idx 0) :
    F.cochainZeroOf 𝒱 p s = F.res ((K).inter_le s 0) (F.pick 𝒱 p (s.1 0))
theorem

cochainZeroTo_cochainZeroOf

L198 ↗
AlgebraicGeometry.OModulePresheaf.cochainZeroTo_cochainZeroOf
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cochainZeroTo_cochainZeroOf (p : F.obj
    𝒱.U0 × F.obj 𝒱.U1) :
    F.cochainZeroTo 𝒱 (F.cochainZeroOf 𝒱 p) = p
theorem

cochainZeroOf_cochainZeroTo

L209 ↗
AlgebraicGeometry.OModulePresheaf.cochainZeroOf_cochainZeroTo
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cochainZeroOf_cochainZeroTo (f :
    F.cochain K 0) :
    F.cochainZeroOf 𝒱 (F.cochainZeroTo 𝒱 f) = f
def

cochainZeroEquiv

L224 ↗
AlgebraicGeometry.OModulePresheaf.cochainZeroEquiv
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.cochainZeroEquiv : F.cochain K 0 ≃ₗ[R] F.obj
    𝒱.U0 × F.obj 𝒱.U1
theorem

finite_HSucc_succ

L232 ↗
AlgebraicGeometry.OModulePresheaf.finite_HSucc_succ
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.finite_HSucc_succ (i : ℕ) : Module.Finite
    R (F.HSucc K (i + 1))
theorem

kerMap_bijective_of_bijective

L258 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.TwoChartCech.kerMap_bijective_of_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
universe uR uK uC
variable {R : Type uR} [CommRing R]
variable {K0 K1 : Type uK} [AddCommGroup K0] [Module R K0] [AddCommGroup K1] [Module R K1]
variable {C0 C1 : Type uK} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem kerMap_bijective_of_bijective (dK : K0 →ₗ[R] K1) (d : C0 →ₗ[R] C1) (ι0 : K0 →ₗ[R] C0)
    (ι1 : K1 →ₗ[R] C1) (comm : d ∘ₗ ι0 = ι1 ∘ₗ dK) (h0 : Function.Bijective ι0)
    (h1 : Function.Injective ι1) : Function.Bijective (kerMap dK d ι0 ι1 comm)
theorem

cokerMap_bijective_of_bijective

L274 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.TwoChartCech.cokerMap_bijective_of_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
universe uR uK uC
variable {R : Type uR} [CommRing R]
variable {K0 K1 : Type uK} [AddCommGroup K0] [Module R K0] [AddCommGroup K1] [Module R K1]
variable {C0 C1 : Type uK} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem cokerMap_bijective_of_bijective (dK : K0 →ₗ[R] K1) (d : C0 →ₗ[R] C1) (ι0 : K0 →ₗ[R] C0)
    (ι1 : K1 →ₗ[R] C1) (comm : d ∘ₗ ι0 = ι1 ∘ₗ dK) (h0 : Function.Surjective ι0)
    (h1 : Function.Bijective ι1) : Function.Bijective (cokerMap dK d ι0 ι1 comm)
theorem

face_idx01_zero

L316 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.face_idx01_zero
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.face_idx01_zero : (K).face
    𝒱.idx01 0 = 𝒱.idx0 ⟨1⟩
theorem

face_idx01_one

L321 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.face_idx01_one
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.face_idx01_one : (K).face
    𝒱.idx01 1 = 𝒱.idx0 ⟨0⟩
theorem

inter_le_inf

L326 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.inter_le_inf
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.inter_le_inf (s : (K).Idx 1) :
    (K).inter s ≤ 𝒱.U0 ⊓ 𝒱.U1
theorem

inf_le_inter

L331 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.inf_le_inter
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.inf_le_inter (s : (K).Idx 1) :
    𝒱.U0 ⊓ 𝒱.U1 ≤ (K).inter s
theorem

res_congr_idx

L344 ↗
AlgebraicGeometry.OModulePresheaf.res_congr_idx
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.res_congr_idx {i : ℕ} (co : F.cochain K
    i) {s s' : (K).Idx i} (e : s = s') {W : X.Opens}
    (p : W ≤ (K).inter s) (p' : W ≤ (K).inter s') : F.res p (co s) = F.res p' (co s')
def

cochainOneTo

L351 ↗
AlgebraicGeometry.OModulePresheaf.cochainOneTo
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.cochainOneTo : F.cochain K 1 →ₗ[R] F.obj
    (𝒱.U0 ⊓ 𝒱.U1)
def

cochainOneOf

L357 ↗
AlgebraicGeometry.OModulePresheaf.cochainOneOf
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.cochainOneOf : F.obj (𝒱.U0 ⊓ 𝒱.U1) →ₗ[R]
    F.cochain K 1
theorem

cochainOneTo_apply

L362 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.cochainOneTo_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem cochainOneTo_apply (co : F.cochain K 1) :
    F.cochainOneTo 𝒱 co = F.res (𝒱.inf_le_inter 𝒱.idx01) (co 𝒱.idx01)
theorem

cochainOneOf_apply

L365 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.cochainOneOf_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem cochainOneOf_apply (x : F.obj (𝒱.U0 ⊓ 𝒱.U1)) (s : (K).Idx 1) :
    F.cochainOneOf 𝒱 x s = F.res (𝒱.inter_le_inf s) x
theorem

cochainOneTo_cochainOneOf

L368 ↗
AlgebraicGeometry.OModulePresheaf.cochainOneTo_cochainOneOf
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cochainOneTo_cochainOneOf (x : F.obj
    (𝒱.U0 ⊓ 𝒱.U1)) :
    F.cochainOneTo 𝒱 (F.cochainOneOf 𝒱 x) = x
theorem

cochainOneOf_cochainOneTo

L375 ↗
AlgebraicGeometry.OModulePresheaf.cochainOneOf_cochainOneTo
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cochainOneOf_cochainOneTo (co : F.cochain
    K 1) :
    F.cochainOneOf 𝒱 (F.cochainOneTo 𝒱 co) = co
def

cochainOneEquiv

L386 ↗
AlgebraicGeometry.OModulePresheaf.cochainOneEquiv
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.cochainOneEquiv : F.cochain K 1 ≃ₗ[R] F.obj
    (𝒱.U0 ⊓ 𝒱.U1)
theorem

cochainOneTo_d

L393 ↗
AlgebraicGeometry.OModulePresheaf.cochainOneTo_d
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cochainOneTo_d (co : F.cochain K 0) :
    F.cochainOneTo 𝒱 (F.d K 0 co) = (F.twoChartSections 𝒱).cechDiff (F.cochainZeroTo 𝒱 co)
theorem

cechDiff_comp_cochainZeroEquiv

L414 ↗
AlgebraicGeometry.OModulePresheaf.cechDiff_comp_cochainZeroEquiv
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechDiff_comp_cochainZeroEquiv :
    (F.twoChartSections 𝒱).cechDiff ∘ₗ (F.cochainZeroEquiv 𝒱).toLinearMap
      = (F.cochainOneEquiv 𝒱).toLinearMap ∘ₗ F.d K 0
def

H0Equiv

L423 ↗
AlgebraicGeometry.OModulePresheaf.H0Equiv
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.H0Equiv : F.H0 K ≃ₗ[R] (F.twoChartSections
    𝒱).H0
theorem

d_one_eq_zero

L432 ↗
AlgebraicGeometry.OModulePresheaf.d_one_eq_zero
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.d_one_eq_zero : F.d K 1 = 0
theorem

ker_d_one_eq_top

L439 ↗
AlgebraicGeometry.OModulePresheaf.ker_d_one_eq_top
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.ker_d_one_eq_top : LinearMap.ker (F.d K
    1) = ⊤
def

HSuccZeroEquivCoker

L445 ↗
AlgebraicGeometry.OModulePresheaf.HSuccZeroEquivCoker
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.HSuccZeroEquivCoker : F.HSucc K 0 ≃ₗ[R]
    (F.cochain K 1 ⧸ LinearMap.range (F.d K 0))
def

HSuccZeroEquiv

L456 ↗
AlgebraicGeometry.OModulePresheaf.HSuccZeroEquiv
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
def _root_.AlgebraicGeometry.OModulePresheaf.HSuccZeroEquiv : F.HSucc K 0 ≃ₗ[R]
    (F.twoChartSections 𝒱).H1
theorem

cechFinite_toOrderedAffineCover_iff'

L466 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry.OModulePresheaf.cechFinite_toOrderedAffineCover_iff'
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
universe u
open CategoryTheory Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) {c : X ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf c)
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
local notation "K" => 𝒱.toOrderedAffineCover
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem cechFinite_toOrderedAffineCover_iff' :
    F.CechFinite K ↔
      Module.Finite R (F.twoChartSections 𝒱).H0 ∧ Module.Finite R (F.twoChartSections 𝒱).H1
theorem

cechFinite_toOrderedAffineCover_iff

L490 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_toOrderedAffineCover_iff
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_toOrderedAffineCover_iff
universe u
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.AlgebraicGeometry
  OModulePresheaf_cechFinite_toOrderedAffineCover_iff.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_toOrderedAffineCover_iff {R : Type u}
    [CommRing R] {X : Scheme.{u}} {c : X ⟶ Spec (.of R)}
    (F : OModulePresheaf c) (𝒱 : X.TwoAffineOpenCover) :
    F.CechFinite 𝒱.toOrderedAffineCover ↔
      Module.Finite R (F.twoChartSections 𝒱).H0 ∧ Module.Finite R (F.twoChartSections 𝒱).H1

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