NYLL
Module

OModulePresheaf_d_zero_ofModules_eq_zero_iff_existsUnique.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_d_zero_ofModules_eq_zero_iff_existsUnique
18 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf d zero of Modules eq zero iff exists Unique

Imports2
Imported by11

Declarations

theorem

map_map

L34 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.map_map
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem map_map {U U' U'' : V.Opens} (f : U' ⟶ U) (g : U'' ⟶ U') (k : U'' ⟶ U) (x : Γ(M, U)) :
    M.presheaf.map g.op (M.presheaf.map f.op x) = M.presheaf.map k.op x
theorem

map_id'

L39 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.map_id'
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem map_id' {U : V.Opens} (k : U ⟶ U) (x : Γ(M, U)) : M.presheaf.map k.op x = x
def

idx0

L45 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.idx0
Documentation

The zero-simplex associated to a member of the ordered cover.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
def idx0 (i : K.ι) : K.Idx 0
theorem

exists_eq_idx0

L49 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.exists_eq_idx0
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem exists_eq_idx0 (s : K.Idx 0) : ∃ i, s = idx0 K i
theorem

le_inter_idx0

L52 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.le_inter_idx0
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem le_inter_idx0 (i : K.ι) : K.U i ≤ K.inter (idx0 K i)
theorem

inter_idx0_le

L54 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.inter_idx0_le
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem inter_idx0_le (i : K.ι) : K.inter (idx0 K i) ≤ K.U i
def

idx1

L57 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.idx1
Documentation

The ordered one-simplex determined by two strictly increasing cover indices.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
def idx1 {i j : K.ι} (h : i < j) : K.Idx 1
theorem

face_idx1_zero

L62 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.face_idx1_zero
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem face_idx1_zero {i j : K.ι} (h : i < j) : K.face (idx1 K h) 0 = idx0 K j
theorem

face_idx1_one

L67 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.face_idx1_one
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem face_idx1_one {i j : K.ι} (h : i < j) : K.face (idx1 K h) 1 = idx0 K i
theorem

inf_le_inter_idx1

L72 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.inf_le_inter_idx1
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem inf_le_inter_idx1 {i j : K.ι} (h : i < j) : K.U i ⊓ K.U j ≤ K.inter (idx1 K h)
theorem

map_congr_idx

L78 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.map_congr_idx
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · full declaration
theorem map_congr_idx (c : (OModulePresheaf.ofModules π M).cochain K 0) {s s' : K.Idx 0} (h : s =
  s')
    {W : V.Opens} (f : W ⟶ K.inter s) (f' : W ⟶ K.inter s') :
    M.presheaf.map f.op (show Γ(M, K.inter s) from c s) = M.presheaf.map f'.op (show Γ(M, K.inter
      s') from c s') := by
  subst h
  rw [Subsingleton.elim f f']
theorem

d_zero_apply

L86 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.d_zero_apply
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · full declaration
theorem d_zero_apply (c : (OModulePresheaf.ofModules π M).cochain K 0) (t : K.Idx 1) :
    (OModulePresheaf.ofModules π M).d K 0 c t =
      M.presheaf.map (homOfLE (K.inter_le_inter_face t 0)).op (show Γ(M, K.inter (K.face t 0))
        from c (K.face t 0)) -
      M.presheaf.map (homOfLE (K.inter_le_inter_face t 1)).op (show Γ(M, K.inter (K.face t 1))
        from c (K.face t 1)) := by
  rw [OModulePresheaf.d_apply, Fin.sum_univ_two]
  simp only [Fin.val_zero, pow_zero, one_smul, Fin.val_one, pow_one, neg_smul, ← sub_eq_add_neg]
  rfl
abbrev

abSheaf

L97 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.abSheaf
Documentation

The underlying sheaf of abelian groups of the sheaf of modules.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
abbrev abSheaf : TopCat.Sheaf Ab V.carrier
def

sfam

L100 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.sfam
Documentation

The local section family obtained from a Čech zero-cochain.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
def sfam (c : (OModulePresheaf.ofModules π M).cochain K 0) (i : K.ι) : Γ(M, K.U i)
theorem

sfam_def

L103 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.sfam_def
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · full declaration
theorem sfam_def (c : (OModulePresheaf.ofModules π M).cochain K 0) (i : K.ι) : sfam π M K c i =
    M.presheaf.map (homOfLE (le_inter_idx0 K i)).op (show Γ(M, K.inter (idx0 K i)) from c (idx0 K
      i)) := rfl
theorem

glue

L107 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.glue
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem glue (c : (OModulePresheaf.ofModules π M).cochain K 0)
    (hcompat : TopCat.Presheaf.IsCompatible M.presheaf K.U (sfam π M K c)) :
    ∃! x : Γ(M, ⊤), ∀ i, M.presheaf.map (homOfLE (le_top : K.U i ≤ ⊤)).op x = sfam π M K c i
theorem

main

L113 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent.CechH0Sol.main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace CechH0Sol
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem main (c : (OModulePresheaf.ofModules π M).cochain K 0) :
    (OModulePresheaf.ofModules π M).d K 0 c = 0 ↔
      ∃! x : Γ(M, ⊤), ∀ s : K.Idx 0, c s = M.presheaf.map (homOfLE (le_top : K.inter s ≤ ⊤)).op x
theorem

d_zero_ofModules_eq_zero_iff_existsUnique

L188 ↗
AlgebraicGeometry.OModulePresheaf.d_zero_ofModules_eq_zero_iff_existsUnique
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsDescent
universe u
section cechH0
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.d_zero_ofModules_eq_zero_iff_existsUnique
    {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) (M : V.Modules)
    (K : V.OrderedAffineCover) (c : (OModulePresheaf.ofModules π M).cochain K 0) :
    (OModulePresheaf.ofModules π M).d K 0 c = 0 ↔
      ∃! x : Γ(M, ⊤), ∀ s : K.Idx 0, c s = M.presheaf.map (homOfLE (le_top : K.inter s ≤ ⊤)).op x

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