Module

OModulePresheaf_d_comp_d.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_d_comp_d

4 declarations indexed from sourceView source ↗

Module documentation

The composite of successive Cech differentials is zero for a module presheaf.

Imports1

Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech

Imported by18

theorem

succAbove_comp_succAbove

L39 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_comp_d.AlgebraicGeometry.OModulePresheaf.DCompD.succAbove_comp_succAbove

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_comp_d
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace DCompD
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem succAbove_comp_succAbove {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) :
    Fin.succAbove j.succ ∘ Fin.succAbove i = Fin.succAbove i.castSucc ∘ Fin.succAbove j

theorem

res_at_eq

L48 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_comp_d.AlgebraicGeometry.OModulePresheaf.DCompD.res_at_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_comp_d
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace DCompD
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem res_at_eq {i : ℕ} {t t' : K.Idx i} (heq : t = t') (f : F.cochain K i) {U : V.Opens}
    (h : U ≤ K.inter t) (h' : U ≤ K.inter t') : F.res h (f t) = F.res h' (f t')

theorem

d_comp_d

L52 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_comp_d.AlgebraicGeometry.OModulePresheaf.DCompD.d_comp_d

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_comp_d
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace DCompD
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem d_comp_d (i : ℕ) : F.d K (i + 1) ∘ₗ F.d K i = 0

theorem

d_comp_d

L114 ↗

AlgebraicGeometry.OModulePresheaf.d_comp_d

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_comp_d
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
universe u
open _root_.AlgebraicCurves.Cohomology.Sheaves.Proofs in
open _root_.AlgebraicGeometry OModulePresheaf_d_comp_d.AlgebraicGeometry in

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.d_comp_d {R : Type u} [CommRing R] {V :
    Scheme.{u}} {π : V ⟶ Spec (.of R)}
    (F : OModulePresheaf π) (K : V.OrderedAffineCover) (i : ℕ) :
    F.d K (i + 1) ∘ₗ F.d K i = 0

Module documentation

Declarations

succAbove_comp_succAbove

res_at_eq

d_comp_d

d_comp_d