NYLL
Module

OModulePresheaf_od_oext.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_od_oext
11 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf od oext

Imports11
Imported by2

Declarations

theorem

units_pow_mul_self

L43 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainAux.units_pow_mul_self
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
namespace OextChainAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem units_pow_mul_self (m : ℕ) : ((-1 : ℤˣ) ^ m) * ((-1 : ℤˣ) ^ m) = 1
theorem

sorted_face_apply

L45 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainAux.sorted_face_apply
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
namespace OextChainAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem sorted_face_apply (u : Fin (n + 1) → ι) (hu : Function.Injective u) (j : Fin (n + 1)) (k :
  Fin n) :
    (u ∘ j.succAbove) (Tuple.sort (u ∘ j.succAbove) k) = (u ∘ Tuple.sort u) (((Tuple.sort u).symm
      j).succAbove k)
theorem

sign_sort_face

L53 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainAux.sign_sort_face
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
namespace OextChainAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem sign_sort_face (u : Fin (n + 1) → ι) (hu : Function.Injective u) (j : Fin (n + 1)) :
    Equiv.Perm.sign (Tuple.sort (u ∘ j.succAbove)) =
      (-1) ^ ((((Tuple.sort u).symm j) : ℕ) + (j : ℕ)) * Equiv.Perm.sign (Tuple.sort u)
theorem

collision

L68 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainAux.collision
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
namespace OextChainAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem collision (u : Fin (n + 1) → ι) {a b : Fin (n + 1)} (hab : a ≠ b) (huab : u a = u b)
    (ha : Function.Injective (u ∘ a.succAbove)) :
    Function.Injective (u ∘ b.succAbove) ∧
    (u ∘ b.succAbove) ∘ Tuple.sort (u ∘ b.succAbove) = (u ∘ a.succAbove) ∘ Tuple.sort (u ∘
      a.succAbove) ∧
    Equiv.Perm.sign (Tuple.sort (u ∘ b.succAbove)) = -((-1) ^ ((a : ℕ) + (b : ℕ)) * Equiv.Perm.sign
      (Tuple.sort (u ∘ a.succAbove)))
theorem

exists_partner

L112 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainAux.exists_partner
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
namespace OextChainAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem exists_partner (u : Fin (n + 1) → ι) (hu : ¬ Function.Injective u) {a : Fin (n + 1)}
    (ha : Function.Injective (u ∘ a.succAbove)) :
    ∃ b, b ≠ a ∧ u a = u b ∧ ∀ c, c ≠ a → c ≠ b → ¬ Function.Injective (u ∘ c.succAbove)
theorem

val_negOne_pow

L138 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainAux.val_negOne_pow
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
namespace OextChainAux
open Equiv
Lean source · statement
theorem val_negOne_pow (m : ℕ) : (((-1 : ℤˣ) ^ m : ℤˣ) : ℤ) = (-1 : ℤ) ^ m
def

qb

L153 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainMain.qb
Documentation

Restrict a cochain component to an open contained in its indexed intersection.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
namespace OextChainMain
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
  (F : OModulePresheaf π) (K : V.OrderedAffineCover) {m : ℕ} (z : F.cochain K m)
Lean source · statement
def qb (T : K.Idx m) (W : V.Opens) (hW : W ≤ K.inter T) : F.obj W
theorem

res_qb

L155 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainMain.res_qb
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
namespace OextChainMain
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
  (F : OModulePresheaf π) (K : V.OrderedAffineCover) {m : ℕ} (z : F.cochain K m)
Lean source · statement
theorem res_qb (T : K.Idx m) {W W' : V.Opens} (hW : W ≤ K.inter T) (hW' : W' ≤ W) (hW'' : W' ≤
  K.inter T) :
    F.res hW' (qb F K z T W hW) = qb F K z T W' hW''
theorem

qb_congr

L160 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.OextChainMain.qb_congr
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
namespace OextChainMain
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
  (F : OModulePresheaf π) (K : V.OrderedAffineCover) {m : ℕ} (z : F.cochain K m)
Lean source · statement
theorem qb_congr {T T' : K.Idx m} (e : T = T') (W : V.Opens) (hW : W ≤ K.inter T) (hW' : W ≤
  K.inter T') :
    qb F K z T W hW = qb F K z T' W hW'
theorem

od_oext_main

L168 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext.od_oext_main
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
open OextChainAux OextChainMain in
Lean source · statement
theorem od_oext_main
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
    (F : OModulePresheaf π) (K : V.OrderedAffineCover) (n : ℕ) (z : F.cochain K n) :
    F.od K n (F.oext K n z) = F.oext K (n + 1) (F.d K n z)
theorem

od_oext

L258 ↗
AlgebraicGeometry.OModulePresheaf.od_oext
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_od_oext
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
open AlgebraicGeometry.OModulePresheaf AlgebraicGeometry.Scheme.OrderedAffineCover
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.od_oext
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)}
    (F : OModulePresheaf π) (K : V.OrderedAffineCover) (n : ℕ) (z : F.cochain K n) :
    F.od K n (F.oext K n z) = F.oext K (n + 1) (F.d K n z)

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