Module

OModulePresheaf_nonempty_cechEquiv_ofModules_of_orderEmbedding_of_forall_lt.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_ofModules_of_orderEmbedding_of_forall_lt

72 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf nonempty cech Equiv of Modules of order Embedding of forall lt

Imports6

Imported by2

theorem

appIso_inv_comp_algebraMap

L49 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.appIso_inv_comp_algebraMap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · statement

theorem appIso_inv_comp_algebraMap (W : (U : Scheme.{u}).Opens) :
    ((Scheme.ΓSpecIso (.of R)).inv ≫ (U.ι ≫ π).appLE ⊤ W le_top) ≫ (U.ι.appIso W).inv =
      (Scheme.ΓSpecIso (.of R)).inv ≫ π.appLE ⊤ (U.ι ''ᵁ W) le_top

theorem

appIso_inv_algebraMap

L63 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.appIso_inv_algebraMap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · statement

theorem appIso_inv_algebraMap (W : (U : Scheme.{u}).Opens) (r : R) :
    (U.ι.appIso W).inv.hom ((Scheme.TwoAffineOpenCover.algebraOfHom (U.ι ≫ π) W).algebraMap r) =
      (Scheme.TwoAffineOpenCover.algebraOfHom π (U.ι ''ᵁ W)).algebraMap r

theorem

appIso_inv_map

L71 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.appIso_inv_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · statement

theorem appIso_inv_map {W W' : (U : Scheme.{u}).Opens} (h : W ≤ W') (a : Γ(↑U, W')) :
    (U.ι.appIso W).inv.hom (((U : Scheme.{u}).presheaf.map (homOfLE h).op).hom a) =
      (V.presheaf.map (homOfLE (U.ι.image_mono h)).op).hom ((U.ι.appIso W').inv.hom a)

def

restrictOpen

L81 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.restrictOpen

Documentation

The module presheaf restricted to an open subscheme using the canonical section ring isomorphisms.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · full declaration

def restrictOpen : OModulePresheaf (U.ι ≫ π) where
  obj W := F.obj (U.ι ''ᵁ W)
  addCommGroup W := inferInstance
  module W := inferInstance
  moduleSections W := Module.compHom (F.obj (U.ι ''ᵁ W)) (U.ι.appIso W).inv.hom
  isScalarTower W := by
    let : Module Γ(↑U, W) (F.obj (U.ι ''ᵁ W)) := Module.compHom (F.obj (U.ι ''ᵁ W)) (U.ι.appIso
      W).inv.hom
    let := Scheme.TwoAffineOpenCover.algebraOfHom (U.ι ≫ π) W
    let := Scheme.TwoAffineOpenCover.algebraOfHom π (U.ι ''ᵁ W)
    refine IsScalarTower.of_algebraMap_smul fun r x => ?_
    change (U.ι.appIso W).inv.hom (algebraMap R Γ(↑U, W) r) • x = r • x
    rw [appIso_inv_algebraMap, algebraMap_smul]
  res h := F.res (U.ι.image_mono h)
  res_smul {W W'} h a x := by
    change F.res (U.ι.image_mono h) ((U.ι.appIso W').inv.hom a • x) =
      (U.ι.appIso W).inv.hom (((U : Scheme.{u}).presheaf.map (homOfLE h).op).hom a) • F.res
        (U.ι.image_mono h) x
    rw [F.res_smul, appIso_inv_map]
  res_refl W := F.res_refl _
  res_comp h h' := F.res_comp _ _

theorem

restrictOpen_res

L103 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.restrictOpen_res

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · full declaration

theorem restrictOpen_res {W W' : (U : Scheme.{u}).Opens} (h : W ≤ W') (x : F.obj (U.ι ''ᵁ W')) :
    (restrictOpen F U).res h (show (restrictOpen F U).obj W' from x) = F.res (U.ι.image_mono h) x
      := rfl

theorem

restrictOpen_smul

L107 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.restrictOpen_smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · full declaration

theorem restrictOpen_smul (W : (U : Scheme.{u}).Opens) (a : Γ(↑U, W)) (x : F.obj (U.ι ''ᵁ W)) :
    (a • (show (restrictOpen F U).obj W from x)) =
      (show (restrictOpen F U).obj W from (U.ι.appIso W).inv.hom a • x) :=
  rfl

theorem

res_irrel

L112 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.res_irrel

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · statement

theorem res_irrel {A B : V.Opens} (h h' : A ≤ B) (x : F.obj B) : F.res h x = F.res h' x

theorem

res_res_eq

L114 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.res_res_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · statement

theorem res_res_eq {A B : V.Opens} (e : A = B) (x : F.obj A) : F.res (le_of_eq e) (F.res (le_of_eq
  e.symm) x) = x

theorem

isQuasicoherent_restrictOpen

L118 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.isQuasicoherent_restrictOpen

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Restrict
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (U : V.Opens)

Lean source · statement

theorem isQuasicoherent_restrictOpen (hF : F.IsQuasicoherent) : (restrictOpen F U).IsQuasicoherent

theorem

image_preimage

L158 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.image_preimage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Cover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (K : V.OrderedAffineCover) (U : V.Opens) (hUa : IsAffineOpen U)

Lean source · statement

theorem image_preimage (W : V.Opens) : U.ι ''ᵁ (U.ι ⁻¹ᵁ W) = U ⊓ W

theorem

mem_iInf_fin

L161 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.mem_iInf_fin

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Cover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (K : V.OrderedAffineCover) (U : V.Opens) (hUa : IsAffineOpen U)

Lean source · statement

theorem mem_iInf_fin {X : Scheme.{u}} {n : ℕ} (W : Fin (n + 1) → X.Opens) (x : X) :
    x ∈ (⨅ j, W j) ↔ ∀ j, x ∈ W j

theorem

preimage_iInf

L171 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.preimage_iInf

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Cover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (K : V.OrderedAffineCover) (U : V.Opens) (hUa : IsAffineOpen U)

Lean source · statement

theorem preimage_iInf {n : ℕ} (W : Fin (n + 1) → V.Opens) : (⨅ j, U.ι ⁻¹ᵁ W j) = U.ι ⁻¹ᵁ (⨅ j, W j)

def

coverOn

L180 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.coverOn

Documentation

The ordered affine cover restricted to the specified affine open subscheme.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Cover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (K : V.OrderedAffineCover) (U : V.Opens) (hUa : IsAffineOpen U)
include hUa in

Lean source · full declaration

def coverOn : (U : Scheme.{u}).OrderedAffineCover where
  ι := K.ι
  U i := U.ι ⁻¹ᵁ K.U i
  isAffineOpen i := by
    rw [← U.ι.isAffineOpen_iff_of_isOpenImmersion, image_preimage]
    exact Scheme.OrderedAffineCover.isAffineOpen_inf_of_isSeparated π hUa (K.isAffineOpen i)
  iSup_eq_top := by
    apply le_antisymm le_top
    intro x _
    have hx : (U.ι.base x) ∈ (⊤ : V.Opens) := trivial
    rw [← K.iSup_eq_top, Opens.mem_iSup] at hx
    obtain ⟨i, hi⟩ := hx
    exact Opens.mem_iSup.mpr ⟨i, hi⟩

theorem

coverOn_U

L194 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.coverOn_U

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Cover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (K : V.OrderedAffineCover) (U : V.Opens) (hUa : IsAffineOpen U)

Lean source · statement

theorem coverOn_U (i : K.ι) : (coverOn π K U hUa).U i = U.ι ⁻¹ᵁ K.U i

theorem

image_inter

L196 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.image_inter

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Cover
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (K : V.OrderedAffineCover) (U : V.Opens) (hUa : IsAffineOpen U)

Lean source · statement

theorem image_inter {n : ℕ} (s : (coverOn π K U hUa).Idx n) :
    U.ι ''ᵁ ((coverOn π K U hUa).inter s) = U ⊓ K.inter ⟨s.1, s.2⟩

theorem

subsingleton_HSucc_restrictOpen

L209 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.subsingleton_HSucc_restrictOpen

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Acyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (F : OModulePresheaf π) (K : V.OrderedAffineCover) (U : V.Opens) (hUa : IsAffineOpen U)
include hUa in

Lean source · statement

theorem subsingleton_HSucc_restrictOpen (hF : F.IsQuasicoherent) (n : ℕ) :
    Subsingleton ((restrictOpen F U).HSucc (coverOn π K U hUa) n)

theorem

exists_d_eq_of_subsingleton_HSucc

L216 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.exists_d_eq_of_subsingleton_HSucc

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Acyclic
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (F : OModulePresheaf π) (K : V.OrderedAffineCover) (U : V.Opens) (hUa : IsAffineOpen U)

Lean source · statement

theorem exists_d_eq_of_subsingleton_HSucc {W : Scheme.{u}} {ρ : W ⟶ Spec (.of R)} (G :
  OModulePresheaf ρ)
    (L : W.OrderedAffineCover) (n : ℕ) [Subsingleton (G.HSucc L n)] (x : G.cochain L (n + 1))
    (hx : G.d L (n + 1) x = 0) : ∃ y : G.cochain L n, G.d L n y = x

def

snoc'

L233 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.snoc'

Documentation

Append a final vertex to a function indexed by a finite ordinal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Snoc
variable {α : Type u} {n : ℕ}

Lean source · statement

def snoc' (f : Fin (n + 1) → α) (a : α) : Fin (n + 2) → α

theorem

snoc'_castSucc

L235 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.snoc'_castSucc

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Snoc
variable {α : Type u} {n : ℕ}

Lean source · statement

theorem snoc'_castSucc (f : Fin (n + 1) → α) (a : α) (k : Fin (n + 1)) : snoc' f a (Fin.castSucc k)
  = f k

theorem

snoc'_last

L239 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.snoc'_last

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Snoc
variable {α : Type u} {n : ℕ}

Lean source · statement

theorem snoc'_last (f : Fin (n + 1) → α) (a : α) : snoc' f a (Fin.last _) = a

theorem

fin_one_eq

L242 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.fin_one_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Snoc
variable {α : Type u} {n : ℕ}

Lean source · statement

theorem fin_one_eq (a b : Fin (0 + 1)) : a = b

def

idxE

L254 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.idxE

Documentation

The increasing Cech index obtained by applying the order embedding to each vertex.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

def idxE (n : ℕ) (s : K.Idx n) : K'.Idx n

theorem

idxE_face

L256 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.idxE_face

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem idxE_face {n : ℕ} (s : K.Idx (n + 1)) (j : Fin (n + 2)) :
    idxE K K' e n (K.face s j) = K'.face (idxE K K' e (n + 1) s) j

theorem

idxE_injective

L259 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.idxE_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem idxE_injective (n : ℕ) : Function.Injective (idxE K K' e n)

theorem

strictMono_snoc

L263 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.strictMono_snoc

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
include hlt in

Lean source · statement

theorem strictMono_snoc {n : ℕ} (s : K.Idx n) : StrictMono (snoc' (e ∘ s.1) j₀)

def

snocIdx

L278 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.snocIdx

Documentation

Append the distinguished final chart to an embedded increasing Cech index.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

def snocIdx (n : ℕ) (s : K.Idx n) : K'.Idx (n + 1)

theorem

snocIdx_apply_castSucc

L281 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.snocIdx_apply_castSucc

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem snocIdx_apply_castSucc {n : ℕ} (s : K.Idx n) (k : Fin (n + 1)) :
    (snocIdx K K' e j₀ hlt n s).1 (Fin.castSucc k) = e (s.1 k)

theorem

snocIdx_apply_last

L284 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.snocIdx_apply_last

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem snocIdx_apply_last {n : ℕ} (s : K.Idx n) : (snocIdx K K' e j₀ hlt n s).1 (Fin.last _) = j₀

def

vtx

L289 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.vtx

Documentation

The degree-zero Cech index consisting of the distinguished chart.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

def vtx : K'.Idx 0

theorem

face_snocIdx_last

L293 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_snocIdx_last

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem face_snocIdx_last {n : ℕ} (s : K.Idx (n + 1)) :
    K'.face (snocIdx K K' e j₀ hlt (n + 1) s) (Fin.last _) = idxE K K' e (n + 1) s

theorem

face_snocIdx_castSucc

L301 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_snocIdx_castSucc

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem face_snocIdx_castSucc {n : ℕ} (s : K.Idx (n + 1)) (j : Fin (n + 2)) :
    K'.face (snocIdx K K' e j₀ hlt (n + 1) s) (Fin.castSucc j) = snocIdx K K' e j₀ hlt n (K.face s
      j)

theorem

face_snocIdx_zero

L314 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_snocIdx_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem face_snocIdx_zero (s : K.Idx 0) : K'.face (snocIdx K K' e j₀ hlt 0 s) 0 = vtx K' j₀

theorem

face_snocIdx_one

L321 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_snocIdx_one

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem face_snocIdx_one (s : K.Idx 0) : K'.face (snocIdx K K' e j₀ hlt 0 s) 1 = idxE K K' e 0 s

theorem

snocIdx_injective

L329 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.snocIdx_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)

Lean source · statement

theorem snocIdx_injective (n : ℕ) : Function.Injective (snocIdx K K' e j₀ hlt n)

theorem

idxE_ne_snocIdx

L337 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.idxE_ne_snocIdx

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
include hlt in

Lean source · statement

theorem idxE_ne_snocIdx {n : ℕ} (s : K.Idx (n + 1)) (s' : K.Idx n) :
    idxE K K' e (n + 1) s ≠ snocIdx K K' e j₀ hlt n s'

theorem

idxE_ne_vtx

L345 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.idxE_ne_vtx

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
include hlt in

Lean source · statement

theorem idxE_ne_vtx (s : K.Idx 0) : idxE K K' e 0 s ≠ vtx K' j₀

theorem

idx_cases

L351 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.idx_cases

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
include hj₀ hlt in

Lean source · statement

theorem idx_cases {n : ℕ} (t : K'.Idx (n + 1)) :
    (∃ s : K.Idx (n + 1), t = idxE K K' e (n + 1) s) ∨ (∃ s : K.Idx n, t = snocIdx K K' e j₀ hlt n
      s)

theorem

idx_cases_zero

L384 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.idx_cases_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
include hj₀ in

Lean source · statement

theorem idx_cases_zero (t : K'.Idx 0) : (∃ s : K.Idx 0, t = idxE K K' e 0 s) ∨ t = vtx K' j₀

theorem

inter_idxE

L395 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.inter_idxE

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
variable (hU : ∀ i, K'.U (e i) = K.U i)
include hU in

Lean source · statement

theorem inter_idxE {n : ℕ} (s : K.Idx n) : K'.inter (idxE K K' e n s) = K.inter s

theorem

inter_snocIdx

L400 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.inter_snocIdx

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
variable (hU : ∀ i, K'.U (e i) = K.U i)
include hU in

Lean source · statement

theorem inter_snocIdx {n : ℕ} (s : K.Idx n) : K'.inter (snocIdx K K' e j₀ hlt n s) = K'.U j₀ ⊓
  K.inter s

theorem

inter_vtx

L412 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.inter_vtx

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Chains
variable {V : Scheme.{u}} (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (j₀ : K'.ι)
  (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
variable (hU : ∀ i, K'.U (e i) = K.U i)

Lean source · statement

theorem inter_vtx : K'.inter (vtx K' j₀) = K'.U j₀

theorem

cochain_congr'

L427 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.cochain_congr'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

theorem cochain_congr' {W : Scheme.{u}} {ρ : W ⟶ Spec (.of R)} (G : OModulePresheaf ρ) {L :
  W.OrderedAffineCover}
    {n : ℕ} (c : G.cochain L n) {t t' : L.Idx n} (htt : t = t') {A : W.Opens} (h : A ≤ L.inter t)
    (h' : A ≤ L.inter t') : G.res h (c t) = G.res h' (c t')

theorem

res_dcongr

L434 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.res_dcongr

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
omit [IsSeparated π] in

Lean source · statement

theorem res_dcongr {α : Type u} (β : α → V.Opens) (c : ∀ a, (𝓕).obj (β a)) {a₁ a₂ : α} (h12 : a₁ =
  a₂)
    {A : V.Opens} (h₁ : A ≤ β a₁) (h₂ : A ≤ β a₂) : (𝓕).res h₁ (c a₁) = (𝓕).res h₂ (c a₂)

theorem

res_zsmul_res

L440 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.res_zsmul_res

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
omit [IsSeparated π] in

Lean source · statement

theorem res_zsmul_res {A B C : V.Opens} (h₁ : A ≤ B) (h₂ : B ≤ C) (z : ℤ) (v : (𝓕).obj C) :
    (𝓕).res h₁ (z • (𝓕).res h₂ v) = z • (𝓕).res (h₁.trans h₂) v

theorem

cochain_congr

L445 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.cochain_congr

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
omit [IsSeparated π] in

Lean source · statement

theorem cochain_congr {L : V.OrderedAffineCover} {n : ℕ} (c : (𝓕).cochain L n) {t t' : L.Idx n}
  (htt : t = t')
    {A : V.Opens} (h : A ≤ L.inter t) (h' : A ≤ L.inter t') : (𝓕).res h (c t) = (𝓕).res h' (c t')

def

fMap

L452 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.fMap

Documentation

Restrict Cech cochains along the embedded subcover and its matching open intersections.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

def fMap (n : ℕ) : (𝓕).cochain K' n →ₗ[R] (𝓕).cochain K n

theorem

fMap_apply

L457 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.fMap_apply

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
omit [IsSeparated π] in

Lean source · statement

theorem fMap_apply (n : ℕ) (c : (𝓕).cochain K' n) (s : K.Idx n) :
    fMap π M K K' e hU n c s = (𝓕).res (le_of_eq (inter_idxE K K' e hU s).symm) (c (idxE K K' e n
      s))

theorem

d_fMap

L462 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.d_fMap

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
omit [IsSeparated π] in

Lean source · statement

theorem d_fMap (n : ℕ) (c : (𝓕).cochain K' n) :
    (𝓕).d K n (fMap π M K K' e hU n c) = fMap π M K K' e hU (n + 1) ((𝓕).d K' n c)

theorem

fMap_surjective

L471 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.fMap_surjective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
omit [IsSeparated π] in

Lean source · statement

theorem fMap_surjective (n : ℕ) : Function.Surjective (fMap π M K K' e hU n)

theorem

apply_idxE_eq_zero_of_fMap_eq_zero

L491 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.apply_idxE_eq_zero_of_fMap_eq_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
omit [IsSeparated π] in

Lean source · statement

theorem apply_idxE_eq_zero_of_fMap_eq_zero (n : ℕ) (c : (𝓕).cochain K' n) (hc : fMap π M K K' e hU
  n c = 0)
    (s : K.Idx n) : c (idxE K K' e n s) = 0

def

sing

L500 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.sing

Documentation

The degree-zero Cech index consisting of the specified chart.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

def sing (i : K.ι) : K.Idx 0

theorem

eq_sing

L504 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.eq_sing

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

theorem eq_sing (s : K.Idx 0) : s = sing K (s.1 0)

theorem

cov_le

L509 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.cov_le

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
include hU in

Lean source · statement

theorem cov_le (i : K.ι) : K'.inter (snocIdx K K' e j₀ hlt 0 (sing K i)) ≤ K'.inter (vtx K' j₀)

theorem

le_iSup_cov

L514 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.le_iSup_cov

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
include hU in

Lean source · statement

theorem le_iSup_cov : K'.inter (vtx K' j₀) ≤ ⨆ i, K'.inter (snocIdx K K' e j₀ hlt 0 (sing K i))

def

Msh

L528 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.Msh

Documentation

The sheaf of abelian groups underlying the given module sheaf.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

def Msh : TopCat.Sheaf Ab V

theorem

hex0

L532 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.hex0

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
include hj₀ hlt in
omit [IsSeparated π] in

Lean source · statement

theorem hex0 (x : (𝓕).cochain K' 0) (hf : fMap π M K K' e hU 0 x = 0) (hd : (𝓕).d K' 0 x = 0) : x =
  0

def

pairIdx

L558 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.pairIdx

Documentation

The increasing degree-one Cech index determined by two ordered chart indices.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

def pairIdx {i i' : K.ι} (h : i < i') : K.Idx 1

theorem

face_pairIdx_zero

L561 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_pairIdx_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

theorem face_pairIdx_zero {i i' : K.ι} (h : i < i') : K.face (pairIdx K h) 0 = sing K i'

theorem

face_pairIdx_one

L564 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_pairIdx_one

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

theorem face_pairIdx_one {i i' : K.ι} (h : i < i') : K.face (pairIdx K h) 1 = sing K i

theorem

inf_cov_le_inter_pair

L572 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.inf_cov_le_inter_pair

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
include hU in

Lean source · statement

theorem inf_cov_le_inter_pair {i i' : K.ι} (h : i < i') :
    K'.inter (snocIdx K K' e j₀ hlt 0 (sing K i)) ⊓ K'.inter (snocIdx K K' e j₀ hlt 0 (sing K i')) ≤
      K'.inter (snocIdx K K' e j₀ hlt 1 (pairIdx K h))

theorem

face_pair_zero

L583 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_pair_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

theorem face_pair_zero {i i' : K.ι} (h : i < i') :
    K'.face (snocIdx K K' e j₀ hlt 1 (pairIdx K h)) 0 = snocIdx K K' e j₀ hlt 0 (sing K i')

theorem

face_pair_one

L587 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_pair_one

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

theorem face_pair_one {i i' : K.ι} (h : i < i') :
    K'.face (snocIdx K K' e j₀ hlt 1 (pairIdx K h)) 1 = snocIdx K K' e j₀ hlt 0 (sing K i)

theorem

face_pair_two

L591 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.face_pair_two

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M

Lean source · statement

theorem face_pair_two {i i' : K.ι} (h : i < i') :
    K'.face (snocIdx K K' e j₀ hlt 1 (pairIdx K h)) 2 = idxE K K' e 1 (pairIdx K h)

theorem

res_pair_eq

L596 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.res_pair_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
omit [IsSeparated π] in

Lean source · statement

theorem res_pair_eq (x : (𝓕).cochain K' 1) (hE : ∀ s : K.Idx 1, x (idxE K K' e 1 s) = 0)
    (hd : (𝓕).d K' 1 x = 0) {i i' : K.ι} (h : i < i') :
    (𝓕).res ((K'.inter_le_inter_face _ 0).trans (le_of_eq (congrArg K'.inter (face_pair_zero K K' e
      j₀ hlt h))))
      (x (snocIdx K K' e j₀ hlt 0 (sing K i'))) =
    (𝓕).res ((K'.inter_le_inter_face _ 1).trans (le_of_eq (congrArg K'.inter (face_pair_one K K' e
      j₀ hlt h))))
      (x (snocIdx K K' e j₀ hlt 0 (sing K i)))

theorem

hexS_zero

L622 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.hexS_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
include hj₀ hlt hU in
omit [IsSeparated π] in

Lean source · statement

theorem hexS_zero (x : (𝓕).cochain K' 1) (hf : fMap π M K K' e hU 1 x = 0) (hd : (𝓕).d K' 1 x = 0) :
    ∃ y : (𝓕).cochain K' 0, fMap π M K K' e hU 0 y = 0 ∧ (𝓕).d K' 0 y = x

abbrev

U₀

L671 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.U₀

Documentation

The distinguished chart open of the enlarged cover.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
section Higher
variable (m : ℕ)

Lean source · statement

abbrev U₀ : V.Opens

abbrev

KU

L674 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.KU

Documentation

The original affine cover restricted to the distinguished chart open.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
section Higher
variable (m : ℕ)

Lean source · statement

abbrev KU : (U₀ K' j₀ : Scheme.{u}).OrderedAffineCover

abbrev

G

L678 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.G

Documentation

The module presheaf on the distinguished chart obtained by restriction.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
section Higher
variable (m : ℕ)

Lean source · statement

abbrev G : OModulePresheaf ((U₀ K' j₀).ι ≫ π)

theorem

eqA

L681 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.eqA

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
section Higher
variable (m : ℕ)
include hU in

Lean source · statement

theorem eqA {n : ℕ} (s : K.Idx n) :
    (U₀ K' j₀).ι ''ᵁ ((KU π K K' j₀).inter s) = K'.inter (snocIdx K K' e j₀ hlt n s)

theorem

hexS_succ

L686 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.hexS_succ

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
section Higher
variable (m : ℕ)
include hj₀ hlt hU hq in

Lean source · statement

theorem hexS_succ (x : (𝓕).cochain K' (m + 2)) (hf : fMap π M K K' e hU (m + 2) x = 0)
    (hd : (𝓕).d K' (m + 2) x = 0) :
    ∃ y : (𝓕).cochain K' (m + 1), fMap π M K K' e hU (m + 1) y = 0 ∧ (𝓕).d K' (m + 1) y = x

theorem

main

L766 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder.P2mAdjoinChart.main

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace P2mAdjoinChart
section Main
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π] (M :
  V.Modules)
  (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
  (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
  (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀)
local notation "𝓕" => OModulePresheaf.ofModules π M
include hj₀ hlt hU hq in

Lean source · statement

theorem main :
    Nonempty ((𝓕).H0 K' ≃ₗ[R] (𝓕).H0 K) ∧ ∀ i : ℕ, Nonempty ((𝓕).HSucc K' i ≃ₗ[R] (𝓕).HSucc K i)

theorem

nonempty_cechEquiv_ofModules_of_orderEmbedding_of_forall_lt

L799 ↗

AlgebraicGeometry.OModulePresheaf.nonempty_cechEquiv_ofModules_of_orderEmbedding_of_forall_lt

Source context 6 commands

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

section ProofImplementation
section PublicStatement
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
open AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesOrder
namespace AlgebraicGeometry.OModulePresheaf

Lean source · statement

theorem nonempty_cechEquiv_ofModules_of_orderEmbedding_of_forall_lt
    {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
    (M : V.Modules) (hq : (OModulePresheaf.ofModules π M).IsQuasicoherent)
    (K K' : V.OrderedAffineCover) (e : K.ι ↪o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i)
    (j₀ : K'.ι) (hj₀ : ∀ j : K'.ι, j = j₀ ∨ j ∈ Set.range e) (hlt : ∀ i, e i < j₀) :
    Nonempty ((OModulePresheaf.ofModules π M).H0 K' ≃ₗ[R] (OModulePresheaf.ofModules π M).H0 K) ∧
      ∀ i : ℕ, Nonempty ((OModulePresheaf.ofModules π M).HSucc K' i ≃ₗ[R]
        (OModulePresheaf.ofModules π M).HSucc K i)

Module documentation

OModule Presheaf nonempty cech Equiv of Modules of order Embedding of forall lt

Declarations