NYLL
Module

OModulePresheafLerayDoubleComplex.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafLerayDoubleComplex
21 declarations indexed from sourceView source ↗

Module documentation

The double-complex structure, augmentations and total cohomology of the Leray bicomplex.

Imports4
Imported by16

Declarations

theorem

succAbove_comp_succAbove

L30 ↗
AlgebraicGeometry.OModulePresheaf.Leray.succAbove_comp_succAbove
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
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_at_eq

L42 ↗
AlgebraicGeometry.OModulePresheaf.Leray.res_at_eq
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem res_at_eq {i : ℕ} {t t' : K.Idx i} (heq : t = t') (f : F.cochain K i) {U : V.Opens}
    (h : U ≤ K.inter t) (h' : U ≤ K.inter t') : F.res h (f t) = F.res h' (f t')
theorem

d_d

L46 ↗
AlgebraicGeometry.OModulePresheaf.Leray.d_d
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem d_d (i : ℕ) : F.d K (i + 1) ∘ₗ F.d K i = 0
theorem

d_d_apply

L104 ↗
AlgebraicGeometry.OModulePresheaf.Leray.d_d_apply
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem d_d_apply (i : ℕ) (c : F.cochain K i) : F.d K (i + 1) (F.d K i c) = 0
theorem

map_iInf_fin

L107 ↗
AlgebraicGeometry.OModulePresheaf.Leray.map_iInf_fin
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem map_iInf_fin {X Y : Scheme.{u}} (f : X ⟶ Y) {n : ℕ} (U : Fin (n + 1) → Y.Opens) :
    (TopologicalSpace.Opens.map f.base).obj (⨅ j, U j) = ⨅ j, (TopologicalSpace.Opens.map
      f.base).obj (U j)
theorem

dV_sq

L133 ↗
AlgebraicGeometry.OModulePresheaf.Leray.dV_sq
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · full declaration
theorem dV_sq (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    dV p πZ K K' a (b + 1) ∘ₗ dV p πZ K K' a b = 0 := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  refine LinearMap.ext fun x => (biC_uncurry p πZ K K' a (b + 2)).injective (funext fun σ => ?_)
  have h₁ := dV_uncurry p πZ K K' a (b + 1) (dV p πZ K K' a b x) σ
  rw [dV_uncurry p πZ K K' a b x σ, relAltd_eq_d, relAltd_eq_d] at h₁
  exact (h₁.trans (d_d_apply (pushOpen p πZ (K.inter σ)) K' b _)).trans
    (congrFun (map_zero (biC_uncurry p πZ K K' a (b + 2))) σ).symm
theorem

dH_sq

L143 ↗
AlgebraicGeometry.OModulePresheaf.Leray.dH_sq
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · full declaration
theorem dH_sq (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    dH p πZ K K' (a + 1) b ∘ₗ dH p πZ K K' a b = 0 := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  refine LinearMap.ext fun x => (biC_uncurry' p πZ K K' (a + 2) b).injective (funext fun τ => ?_)
  have h₁ := dH_uncurry p πZ K K' (a + 1) b (dH p πZ K K' a b x) τ
  rw [dH_uncurry p πZ K K' a b x τ] at h₁
  exact (h₁.trans (d_d_apply (pullOpen p πZ (K'.inter τ)) K a _)).trans
    (congrFun (map_zero (biC_uncurry' p πZ K K' (a + 2) b)) τ).symm
theorem

dHV_comm

L153 ↗
AlgebraicGeometry.OModulePresheaf.Leray.dHV_comm
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · full declaration
theorem dHV_comm (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    dV p πZ K K' (a + 1) b ∘ₗ dH p πZ K K' a b = dH p πZ K K' a (b + 1) ∘ₗ dV p πZ K K' a b := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  refine LinearMap.ext fun x => funext fun στ => ?_
  simp only [LinearMap.comp_apply, dH_apply', dV_apply', map_sum, map_zsmul,
    Finset.smul_sum, smul_smul]
  rw [Finset.sum_comm]
  refine Finset.sum_congr rfl fun j _ => Finset.sum_congr rfl fun k _ => ?_
  rw [mul_comm]
  erw [Scheme.TwoAffineOpenCover.res_res, Scheme.TwoAffineOpenCover.res_res]
def

LerayDblCpx

L166 ↗
AlgebraicGeometry.OModulePresheaf.Leray.LerayDblCpx
Documentation

The bounded double complex formed by horizontal and vertical Čech differentials.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · statement
def LerayDblCpx : DoubleComplex.Bounded R
theorem

LerayDblCpx_C

L177 ↗
AlgebraicGeometry.OModulePresheaf.Leray.LerayDblCpx_C
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · statement
theorem LerayDblCpx_C (a b : ℕ) : (LerayDblCpx p πZ K K').C a b = biC p πZ K K' a b
theorem

LerayDblCpx_N

L178 ↗
AlgebraicGeometry.OModulePresheaf.Leray.LerayDblCpx_N
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · statement
theorem LerayDblCpx_N : (LerayDblCpx p πZ K K').N = max (Fintype.card K.ι) (Fintype.card K'.ι)
theorem

LerayDblCpx_dH

L180 ↗
AlgebraicGeometry.OModulePresheaf.Leray.LerayDblCpx_dH
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · full declaration
theorem LerayDblCpx_dH (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (LerayDblCpx p πZ K K').dH a b = dH p πZ K K' a b := rfl
theorem

LerayDblCpx_dV

L183 ↗
AlgebraicGeometry.OModulePresheaf.Leray.LerayDblCpx_dV
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · full declaration
theorem LerayDblCpx_dV (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (LerayDblCpx p πZ K K').dV a b = dV p πZ K K' a b := rfl
def

biAug

L188 ↗
AlgebraicGeometry.OModulePresheaf.Leray.biAug
Documentation

The augmentation from source Čech cochains to the horizontal degree-zero column.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · full declaration
def biAug (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (OModulePresheaf.unit (p ≫ πZ)).cochain K' b →ₗ[R] biC p πZ K K' 0 b :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  LinearMap.pi fun στ => Scheme.OrderedAffineCoverOf.res (p ≫ πZ) inf_le_left ∘ₗ LinearMap.proj στ.2
theorem

biAug_apply

L194 ↗
AlgebraicGeometry.OModulePresheaf.Leray.biAug_apply
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section DblCpx
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R))
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · statement
theorem biAug_apply (b : ℕ) (y : (OModulePresheaf.unit (p ≫ πZ)).cochain K' b) (στ : BiIdx K K' 0
    b) :
    biAug p πZ K K' b y στ
      = (V'.presheaf.map (homOfLE (inf_le_left : biOpen p K K' 0 b στ.1 στ.2 ≤ K'.inter
        στ.2)).op).hom (y στ.2)
def

relAug

L210 ↗
AlgebraicGeometry.OModulePresheaf.Leray.relAug
Documentation

The augmentation from sections on a preimage open to relative Čech cochains.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section RelAug
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) (K' : Scheme.OrderedAffineCover V') (U :
  Z.Opens)
Lean source · full declaration
def relAug :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (pullOpen p πZ (⊤ : V'.Opens)).obj U →ₗ[R] relAltC p πZ K' U 0 :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  LinearMap.pi fun _ => Scheme.OrderedAffineCoverOf.res (p ≫ πZ) (inf_le_inf_right _ le_top)
theorem

relAug_apply

L216 ↗
AlgebraicGeometry.OModulePresheaf.Leray.relAug_apply
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section RelAug
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) (K' : Scheme.OrderedAffineCover V') (U :
  Z.Opens)
Lean source · statement
theorem relAug_apply (w : (pullOpen p πZ (⊤ : V'.Opens)).obj U) (τ : K'.Idx 0) :
    relAug p πZ K' U w τ
      = (V'.presheaf.map (homOfLE (inf_le_inf_right ((Opens.map p.base).obj U)
          (le_top : K'.inter τ ≤ ⊤))).op).hom w
def

rowCoverOf

L231 ↗
AlgebraicGeometry.OModulePresheaf.Leray.rowCoverOf
Documentation

The affine cover of a vertical intersection induced by the base affine cover.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section RowCover
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · full declaration
def rowCoverOf {q : ℕ} (τ : K'.Idx q) : V'.OrderedAffineCoverOf (K'.inter τ) where
  ι := K.ι
  U i := K'.inter τ ⊓ (Opens.map p.base).obj (K.U i)
  isAffineOpen i := Scheme.OrderedAffineCover.fiberAffineOpen p πZ
    (Scheme.OrderedAffineCover.isAffineOpen_inter (p ≫ πZ) K' τ) (K.isAffineOpen i)
  le _ := inf_le_left
  iSup_eq := le_antisymm (iSup_le fun _ => inf_le_left) fun x hx =>
    let ⟨i, hi⟩ := Opens.mem_iSup.mp (show p.base x ∈ ⨆ i, K.U i from K.iSup_eq_top.symm ▸ trivial)
    Opens.mem_iSup.mpr ⟨i, hx, hi⟩
theorem

rowCoverOf_U

L241 ↗
AlgebraicGeometry.OModulePresheaf.Leray.rowCoverOf_U
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section RowCover
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · statement
theorem rowCoverOf_U {q : ℕ} (τ : K'.Idx q) (i : K.ι) :
    (rowCoverOf p πZ K K' τ).U i = K'.inter τ ⊓ (Opens.map p.base).obj (K.U i)
theorem

inter_rowCoverOf

L244 ↗
AlgebraicGeometry.OModulePresheaf.Leray.inter_rowCoverOf
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section RowCover
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] [IsSeparated (p ≫ πZ)]
variable (K : Scheme.OrderedAffineCover Z) (K' : Scheme.OrderedAffineCover V')
Lean source · statement
theorem inter_rowCoverOf {a b : ℕ} (τ : K'.Idx b) (σ : (rowCoverOf p πZ K K' τ).Idx a) :
    (rowCoverOf p πZ K K' τ).inter σ = biOpen p K K' a b σ τ
theorem

inter_restrictToPreimage

L258 ↗
AlgebraicGeometry.OModulePresheaf.Leray.inter_restrictToPreimage
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace AlgebraicGeometry.OModulePresheaf.Leray
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
section RestrictToPreimage
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ] (K' :
  Scheme.OrderedAffineCover V')
Lean source · statement
theorem inter_restrictToPreimage {U : Z.Opens} (hU : IsAffineOpen U) {b : ℕ}
    (τ : (restrictToPreimage p πZ K' hU).Idx b) :
    (restrictToPreimage p πZ K' hU).inter τ = K'.inter τ ⊓ (Opens.map p.base).obj U

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