NYLL
Module

BiCech.lean

Nyll.AlgebraicCurves.Cohomology.Cech.BiCech
37 declarations indexed from sourceView source ↗

Module documentation

Bi Cech

Imports7
Imported by3

Declarations

structure

OrderedOpenFamily

L34 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily
Documentation

A finite linearly ordered family of open subschemes.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
Lean source · full declaration
structure Scheme.OrderedOpenFamily (Z : Scheme.{u}) where
  /-- The index type of the family. -/
  ι : Type u
  /-- Finiteness of the index type. -/
  [instFintype : Fintype ι]
  /-- The order used to orient intersections. -/
  [instLinearOrder : LinearOrder ι]
  /-- The open subscheme at each index. -/
  U : ι → Z.Opens
def

Idx

L51 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.Idx
Documentation

Strictly increasing index tuples for intersections in degree p.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
def Idx (p : ℕ) : Type u
instance

instFintypeIdx

L53 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.instFintypeIdx
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
instance instFintypeIdx (p : ℕ) : Fintype (𝔄.Idx p)
instance

instDecidableEqIdx

L55 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.instDecidableEqIdx
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
instance instDecidableEqIdx (p : ℕ) : DecidableEq (𝔄.Idx p)
def

inter

L58 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.inter
Documentation

The intersection of the opens indexed by a tuple.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
def inter {p : ℕ} (s : 𝔄.Idx p) : Z.Opens
def

face

L61 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.face
Documentation

Delete one entry from an increasing index tuple.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
def face {p : ℕ} (s : 𝔄.Idx (p + 1)) (j : Fin (p + 2)) : 𝔄.Idx p
theorem

face_val

L64 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.face_val
Source context 7 commands

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

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

inter_le

L67 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.inter_le
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
theorem inter_le {p : ℕ} (s : 𝔄.Idx p) (j : Fin (p + 1)) : 𝔄.inter s ≤ 𝔄.U (s.1 j)
theorem

inter_le_inter_face

L69 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.inter_le_inter_face
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
theorem inter_le_inter_face {p : ℕ} (s : 𝔄.Idx (p + 1)) (j : Fin (p + 2)) :
    𝔄.inter s ≤ 𝔄.inter (𝔄.face s j)
theorem

isEmpty_idx_of_card_le

L73 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.isEmpty_idx_of_card_le
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
theorem isEmpty_idx_of_card_le {p : ℕ} (h : Fintype.card 𝔄.ι ≤ p) : IsEmpty (𝔄.Idx p)
def

prodCover

L80 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.prodCover
Documentation

The ordered affine cover formed by pairwise intersections of two open families.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · full declaration
def prodCover (𝔄 𝔅 : Z.OrderedOpenFamily) (haff : ∀ i j, IsAffineOpen (𝔄.U i ⊓ 𝔅.U j))
    (hcov : ⨆ ij : 𝔄.ι × 𝔅.ι, 𝔄.U ij.1 ⊓ 𝔅.U ij.2 = ⊤) : Z.OrderedAffineCover where
  ι := 𝔄.ι ×ₗ 𝔅.ι
  instFintype := inferInstanceAs (Fintype (𝔄.ι × 𝔅.ι))
  instLinearOrder := inferInstance
  U ij := 𝔄.U (ofLex ij).1 ⊓ 𝔅.U (ofLex ij).2
  isAffineOpen ij := haff _ _
  iSup_eq_top := by
    rw [← hcov]
    exact le_antisymm (iSup_le fun ij => le_iSup (fun ij : 𝔄.ι × 𝔅.ι => 𝔄.U ij.1 ⊓ 𝔅.U ij.2)
      (ofLex ij))
      (iSup_le fun ij => le_iSup (fun ij : 𝔄.ι ×ₗ 𝔅.ι => 𝔄.U (ofLex ij).1 ⊓ 𝔅.U (ofLex ij).2)
        (toLex ij))
theorem

prodCover_ι

L94 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.prodCover_ι
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
theorem prodCover_ι (𝔄 𝔅 : Z.OrderedOpenFamily) (haff : ∀ i j, IsAffineOpen (𝔄.U i ⊓ 𝔅.U j))
    (hcov : ⨆ ij : 𝔄.ι × 𝔅.ι, 𝔄.U ij.1 ⊓ 𝔅.U ij.2 = ⊤) : (𝔄.prodCover 𝔅 haff hcov).ι = (𝔄.ι ×ₗ
      𝔅.ι)
theorem

prodCover_U

L98 ↗
AlgebraicGeometry.Scheme.OrderedOpenFamily.prodCover_U
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedOpenFamily
variable {Z : Scheme.{u}} (𝔄 : Z.OrderedOpenFamily)
Lean source · statement
theorem prodCover_U (𝔄 𝔅 : Z.OrderedOpenFamily) (haff : ∀ i j, IsAffineOpen (𝔄.U i ⊓ 𝔅.U j))
    (hcov : ⨆ ij : 𝔄.ι × 𝔅.ι, 𝔄.U ij.1 ⊓ 𝔅.U ij.2 = ⊤) (ij : 𝔄.ι ×ₗ 𝔅.ι) :
    (𝔄.prodCover 𝔅 haff hcov).U ij = 𝔄.U (ofLex ij).1 ⊓ 𝔅.U (ofLex ij).2
def

toOpenFamily

L107 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.toOpenFamily
Documentation

Forget the affineness and covering conditions of an ordered affine cover.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedAffineCover
Lean source · full declaration
def toOpenFamily {Z : Scheme.{u}} (K : Z.OrderedAffineCover) : Z.OrderedOpenFamily where
  ι := K.ι
  U := K.U
theorem

toOpenFamily_ι

L111 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.toOpenFamily_ι
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedAffineCover
Lean source · statement
theorem toOpenFamily_ι {Z : Scheme.{u}} (K : Z.OrderedAffineCover) : K.toOpenFamily.ι = K.ι
theorem

toOpenFamily_U

L112 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.toOpenFamily_U
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedAffineCover
Lean source · statement
theorem toOpenFamily_U {Z : Scheme.{u}} (K : Z.OrderedAffineCover) (i : K.ι) : K.toOpenFamily.U
  i = K.U i
def

imageFamily

L116 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.imageFamily
Documentation

The images of the affine opens under an open immersion.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedAffineCover
Lean source · full declaration
def imageFamily {W Z : Scheme.{u}} (K : W.OrderedAffineCover) (f : W ⟶ Z) [IsOpenImmersion f] :
    Z.OrderedOpenFamily where
  ι := K.ι
  U i := f ''ᵁ K.U i
theorem

imageFamily_ι

L121 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.imageFamily_ι
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedAffineCover
Lean source · statement
theorem imageFamily_ι {W Z : Scheme.{u}} (K : W.OrderedAffineCover) (f : W ⟶ Z) [IsOpenImmersion
  f] :
    (K.imageFamily f).ι = K.ι
theorem

imageFamily_U

L124 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.imageFamily_U
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace Scheme.OrderedAffineCover
Lean source · statement
theorem imageFamily_U {W Z : Scheme.{u}} (K : W.OrderedAffineCover) (f : W ⟶ Z) [IsOpenImmersion
  f] (i : K.ι) :
    (K.imageFamily f).U i = f ''ᵁ K.U i
theorem

inter_inf_le_left

L137 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.inter_inf_le_left
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem inter_inf_le_left {p q : ℕ} (s : 𝔄.Idx (p + 1)) (t : 𝔅.Idx q) (j : Fin (p + 2)) :
    𝔄.inter s ⊓ 𝔅.inter t ≤ 𝔄.inter (𝔄.face s j) ⊓ 𝔅.inter t
theorem

inter_inf_le_right

L141 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.inter_inf_le_right
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem inter_inf_le_right {p q : ℕ} (s : 𝔄.Idx p) (t : 𝔅.Idx (q + 1)) (j : Fin (q + 2)) :
    𝔄.inter s ⊓ 𝔅.inter t ≤ 𝔄.inter s ⊓ 𝔅.inter (𝔅.face t j)
abbrev

C

L146 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.C
Documentation

Sections over intersections indexed by the two ordered open families.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
abbrev C (p q : ℕ) : Type u
def

dH

L149 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.dH
Documentation

The alternating restriction differential in the first index.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
def dH (p q : ℕ) : C F 𝔄 𝔅 p q →ₗ[R] C F 𝔄 𝔅 (p + 1) q
def

dV

L154 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.dV
Documentation

The alternating restriction differential in the second index.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
def dV (p q : ℕ) : C F 𝔄 𝔅 p q →ₗ[R] C F 𝔄 𝔅 p (q + 1)
theorem

dH_apply

L158 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.dH_apply
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem dH_apply (p q : ℕ) (c : C F 𝔄 𝔅 p q) (st : 𝔄.Idx (p + 1) × 𝔅.Idx q) :
    dH F 𝔄 𝔅 p q c st = ∑ j : Fin (p + 2), ((-1 : ℤ) ^ (j : ℕ)) •
      F.res (inter_inf_le_left 𝔄 𝔅 st.1 st.2 j) (c (𝔄.face st.1 j, st.2))
theorem

dV_apply

L165 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.dV_apply
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem dV_apply (p q : ℕ) (c : C F 𝔄 𝔅 p q) (st : 𝔄.Idx p × 𝔅.Idx (q + 1)) :
    dV F 𝔄 𝔅 p q c st = ∑ j : Fin (q + 2), ((-1 : ℤ) ^ (j : ℕ)) •
      F.res (inter_inf_le_right 𝔄 𝔅 st.1 st.2 j) (c (st.1, 𝔅.face st.2 j))
theorem

succAbove_comp_succAbove

L172 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.succAbove_comp_succAbove
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem succAbove_comp_succAbove {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) :
    Fin.succAbove j.succ ∘ Fin.succAbove i = Fin.succAbove i.castSucc ∘ Fin.succAbove j
theorem

res_left_eq

L181 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.res_left_eq
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem res_left_eq {p q : ℕ} {s s' : 𝔄.Idx p} (heq : s = s') (t : 𝔅.Idx q) (f : C F 𝔄 𝔅 p q)
    {O : Z.Opens} (h : O ≤ 𝔄.inter s ⊓ 𝔅.inter t) (h' : O ≤ 𝔄.inter s' ⊓ 𝔅.inter t) :
    F.res h (f (s, t)) = F.res h' (f (s', t))
theorem

res_right_eq

L186 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.res_right_eq
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem res_right_eq {p q : ℕ} (s : 𝔄.Idx p) {t t' : 𝔅.Idx q} (heq : t = t') (f : C F 𝔄 𝔅 p q)
    {O : Z.Opens} (h : O ≤ 𝔄.inter s ⊓ 𝔅.inter t) (h' : O ≤ 𝔄.inter s ⊓ 𝔅.inter t') :
    F.res h (f (s, t)) = F.res h' (f (s, t'))
theorem

dH_sq

L191 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.dH_sq
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem dH_sq (p q : ℕ) : dH F 𝔄 𝔅 (p + 1) q ∘ₗ dH F 𝔄 𝔅 p q = 0
theorem

dV_sq

L250 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.dV_sq
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem dV_sq (p q : ℕ) : dV F 𝔄 𝔅 p (q + 1) ∘ₗ dV F 𝔄 𝔅 p q = 0
theorem

dHV_comm

L309 ↗
AlgebraicGeometry.OModulePresheaf.BiCech.dHV_comm
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
namespace BiCech
Lean source · statement
theorem dHV_comm (p q : ℕ) :
    dV F 𝔄 𝔅 (p + 1) q ∘ₗ dH F 𝔄 𝔅 p q = dH F 𝔄 𝔅 p (q + 1) ∘ₗ dV F 𝔄 𝔅 p q
def

biCech

L322 ↗
AlgebraicGeometry.OModulePresheaf.biCech
Documentation

The bounded double complex of sections over the two open families.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
Lean source · full declaration
def biCech : DoubleComplex.Bounded R where
  C := BiCech.C F 𝔄 𝔅
  dH := BiCech.dH F 𝔄 𝔅
  dV := BiCech.dV F 𝔄 𝔅
  dH_sq := BiCech.dH_sq F 𝔄 𝔅
  dV_sq := BiCech.dV_sq F 𝔄 𝔅
  dHV_comm := BiCech.dHV_comm F 𝔄 𝔅
  N := max (Fintype.card 𝔄.ι) (Fintype.card 𝔅.ι)
  hBound p q h := by
    rcases h with h | h
    · have := 𝔄.isEmpty_idx_of_card_le ((le_max_left _ _).trans h)
      infer_instance
    · have := 𝔅.isEmpty_idx_of_card_le ((le_max_right _ _).trans h)
      infer_instance
theorem

biCech_C

L337 ↗
AlgebraicGeometry.OModulePresheaf.biCech_C
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
Lean source · statement
theorem biCech_C (p q : ℕ) : (F.biCech 𝔄 𝔅).C p q = BiCech.C F 𝔄 𝔅 p q
theorem

biCech_N

L338 ↗
AlgebraicGeometry.OModulePresheaf.biCech_N
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
Lean source · statement
theorem biCech_N : (F.biCech 𝔄 𝔅).N = max (Fintype.card 𝔄.ι) (Fintype.card 𝔅.ι)
theorem

biCech_dH

L339 ↗
AlgebraicGeometry.OModulePresheaf.biCech_dH
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
Lean source · statement
theorem biCech_dH (p q : ℕ) : (F.biCech 𝔄 𝔅).dH p q = BiCech.dH F 𝔄 𝔅 p q
theorem

biCech_dV

L340 ↗
AlgebraicGeometry.OModulePresheaf.biCech_dV
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace AlgebraicGeometry
attribute [instance] Scheme.OrderedOpenFamily.instFintype Scheme.OrderedOpenFamily.instLinearOrder
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {π : Z ⟶ Spec (.of R)} (F : OModulePresheaf π)
variable (𝔄 𝔅 : Z.OrderedOpenFamily)
Lean source · statement
theorem biCech_dV (p q : ℕ) : (F.biCech 𝔄 𝔅).dV p q = BiCech.dV F 𝔄 𝔅 p q

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