NYLL
Module

OrderedAffineCoverCechOrdered.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OrderedAffineCoverCechOrdered
32 declarations indexed from sourceView source ↗

Module documentation

Ordered Affine Cover Cech Ordered

Imports3
Imported by6

Declarations

abbrev

OIdx

L34 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.OIdx
Documentation

Tuples of cover indices, allowing repetitions and arbitrary ordering.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
abbrev OIdx (n : ℕ) : Type u
def

ointer

L37 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ointer
Documentation

The intersection of cover opens indexed by a tuple.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
def ointer {n : ℕ} (t : K.OIdx n) : V.Opens
theorem

inter_eq_ointer

L39 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.inter_eq_ointer
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem inter_eq_ointer {n : ℕ} (s : K.Idx n) : K.inter s = K.ointer s.1
theorem

ointer_le

L41 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ointer_le
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem ointer_le {n : ℕ} (t : K.OIdx n) (j : Fin (n + 1)) : K.ointer t ≤ K.U (t j)
def

oface

L44 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.oface
Documentation

Delete one entry from a tuple of cover indices.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
def oface {n : ℕ} (t : K.OIdx (n + 1)) (j : Fin (n + 2)) : K.OIdx n
theorem

oface_apply

L46 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.oface_apply
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem oface_apply {n : ℕ} (t : K.OIdx (n + 1)) (j : Fin (n + 2)) (k : Fin (n + 1)) :
    K.oface t j k = t (j.succAbove k)
theorem

ointer_le_ointer_oface

L49 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ointer_le_ointer_oface
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem ointer_le_ointer_oface {n : ℕ} (t : K.OIdx (n + 1)) (j : Fin (n + 2)) :
    K.ointer t ≤ K.ointer (K.oface t j)
def

ofrontFace

L54 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ofrontFace
Documentation

The front face of a tuple, retaining its first a + 1 entries.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
def ofrontFace (a b n : ℕ) (h : a + b = n) (t : K.OIdx n) : K.OIdx a
def

obackFace

L57 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.obackFace
Documentation

The back face of a tuple, starting at its a-th entry.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
def obackFace (a b n : ℕ) (h : a + b = n) (t : K.OIdx n) : K.OIdx b
theorem

ofrontFace_apply

L60 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ofrontFace_apply
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · full declaration
theorem ofrontFace_apply (a b n : ℕ) (h : a + b = n) (t : K.OIdx n) (j : Fin (a + 1)) :
    K.ofrontFace a b n h t j = t ⟨j.1, by omega⟩ := rfl
theorem

obackFace_apply

L63 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.obackFace_apply
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · full declaration
theorem obackFace_apply (a b n : ℕ) (h : a + b = n) (t : K.OIdx n) (j : Fin (b + 1)) :
    K.obackFace a b n h t j = t ⟨a + j.1, by omega⟩ := rfl
theorem

frontFace_val

L66 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.frontFace_val
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem frontFace_val (a b n : ℕ) (h : a + b = n) (s : K.Idx n) :
    (K.frontFace a b n h s).1 = K.ofrontFace a b n h s.1
theorem

backFace_val

L69 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.backFace_val
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem backFace_val (a b n : ℕ) (h : a + b = n) (s : K.Idx n) :
    (K.backFace a b n h s).1 = K.obackFace a b n h s.1
theorem

ointer_le_ointer_ofrontFace

L72 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ointer_le_ointer_ofrontFace
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem ointer_le_ointer_ofrontFace (a b n : ℕ) (h : a + b = n) (t : K.OIdx n) :
    K.ointer t ≤ K.ointer (K.ofrontFace a b n h t)
theorem

ointer_le_ointer_obackFace

L76 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ointer_le_ointer_obackFace
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem ointer_le_ointer_obackFace (a b n : ℕ) (h : a + b = n) (t : K.OIdx n) :
    K.ointer t ≤ K.ointer (K.obackFace a b n h t)
def

osort

L81 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.osort
Documentation

Sort an injective tuple into a strictly increasing cover index.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
def osort {n : ℕ} (t : K.OIdx n) (hinj : Function.Injective t) : K.Idx n
theorem

osort_val

L85 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.osort_val
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem osort_val {n : ℕ} (t : K.OIdx n) (hinj : Function.Injective t) :
    (K.osort t hinj).1 = t ∘ Tuple.sort t
theorem

ointer_le_inter_osort

L88 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ointer_le_inter_osort
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem ointer_le_inter_osort {n : ℕ} (t : K.OIdx n) (hinj : Function.Injective t) :
    K.ointer t ≤ K.inter (K.osort t hinj)
theorem

inter_osort_le_ointer

L92 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.inter_osort_le_ointer
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem inter_osort_le_ointer {n : ℕ} (t : K.OIdx n) (hinj : Function.Injective t) :
    K.inter (K.osort t hinj) ≤ K.ointer t
theorem

ointer_le_preimage_ointer_comp

L98 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.ointer_le_preimage_ointer_comp
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace Scheme.OrderedAffineCover
variable {V : Scheme.{u}} (K : V.OrderedAffineCover)
Lean source · statement
theorem ointer_le_preimage_ointer_comp {X Y : Scheme.{u}} (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover)
    (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι) (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w))
    {n : ℕ} (t : 𝒲.OIdx n) : 𝒲.ointer t ≤ h ⁻¹ᵁ 𝒦.ointer (lam ∘ t)
abbrev

ocochain

L113 ↗
AlgebraicGeometry.OModulePresheaf.ocochain
Documentation

Cochains indexed by all tuples of cover indices.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
abbrev ocochain (n : ℕ) : Type u
def

od

L116 ↗
AlgebraicGeometry.OModulePresheaf.od
Documentation

The alternating restriction differential on tuple-indexed cochains.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def od (n : ℕ) : F.ocochain K n →ₗ[R] F.ocochain K (n + 1)
theorem

od_apply

L120 ↗
AlgebraicGeometry.OModulePresheaf.od_apply
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem od_apply (n : ℕ) (c : F.ocochain K n) (t : K.OIdx (n + 1)) :
    F.od K n c t = ∑ j : Fin (n + 2), ((-1 : ℤ) ^ (j : ℕ)) • F.res (K.ointer_le_ointer_oface t
      j) (c (K.oface t j))
def

ocup

L128 ↗
AlgebraicGeometry.OModulePresheaf.ocup
Documentation

The cup product on tuple-indexed cochains.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def ocup (a b n : ℕ) (h : a + b = n) (α : (unit π).ocochain K a) (β : F.ocochain K b) :
  F.ocochain K n
theorem

ocup_apply

L134 ↗
AlgebraicGeometry.OModulePresheaf.ocup_apply
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem ocup_apply (a b n : ℕ) (h : a + b = n) (α : (unit π).ocochain K a) (β : F.ocochain K b)
  (t : K.OIdx n) :
    F.ocup K a b n h α β t =
      (V.presheaf.map (homOfLE (K.ointer_le_ointer_ofrontFace a b n h t)).op).hom (α
        (K.ofrontFace a b n h t))
        • F.res (K.ointer_le_ointer_obackFace a b n h t) (β (K.obackFace a b n h t))
def

ores

L143 ↗
AlgebraicGeometry.OModulePresheaf.ores
Documentation

Restrict tuple-indexed cochains to strictly increasing indices.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def ores (n : ℕ) : F.ocochain K n →ₗ[R] F.cochain K n
theorem

ores_apply

L146 ↗
AlgebraicGeometry.OModulePresheaf.ores_apply
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem ores_apply (n : ℕ) (c : F.ocochain K n) (s : K.Idx n) : F.ores K n c s = c s.1
def

oext

L149 ↗
AlgebraicGeometry.OModulePresheaf.oext
Documentation

Extend a cochain by signed sorting, assigning zero to tuples with repetitions.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
def oext (n : ℕ) : F.cochain K n →ₗ[R] F.ocochain K n
theorem

oext_apply_of_injective

L157 ↗
AlgebraicGeometry.OModulePresheaf.oext_apply_of_injective
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem oext_apply_of_injective (n : ℕ) (z : F.cochain K n) (t : K.OIdx n) (hinj :
  Function.Injective t) :
    F.oext K n z t = ((Equiv.Perm.sign (Tuple.sort t) : ℤˣ) : ℤ) •
      F.res (K.ointer_le_inter_osort t hinj) (z (K.osort t hinj))
theorem

oext_apply_of_not_injective

L166 ↗
AlgebraicGeometry.OModulePresheaf.oext_apply_of_not_injective
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
Lean source · statement
theorem oext_apply_of_not_injective (n : ℕ) (z : F.cochain K n) (t : K.OIdx n) (hinj : ¬
  Function.Injective t) :
    F.oext K n z t = 0
def

ounitPullback

L176 ↗
AlgebraicGeometry.OModulePresheaf.ounitPullback
Documentation

Pull back a tuple-indexed structure-sheaf cochain along a map of ordered covers.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable {R' : Type u} [CommRing R'] {X Y : Scheme.{u}} {πX : X ⟶ Spec (.of R')} {πY : Y ⟶ Spec
  (.of R)}
Lean source · statement
def ounitPullback (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι →
  𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ)
    (c : (unit πY).ocochain 𝒦 n) : (unit πX).ocochain 𝒲 n
theorem

ounitPullback_apply

L183 ↗
AlgebraicGeometry.OModulePresheaf.ounitPullback_apply
Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite TopologicalSpace
namespace OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)
variable {R' : Type u} [CommRing R'] {X Y : Scheme.{u}} {πX : X ⟶ Spec (.of R')} {πY : Y ⟶ Spec
  (.of R)}
Lean source · statement
theorem ounitPullback_apply (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover)
    (lam : 𝒲.ι → 𝒦.ι) (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ)
    (c : (unit πY).ocochain 𝒦 n) (t : 𝒲.OIdx n) :
    ounitPullback (πX := πX) h 𝒲 𝒦 lam hlam n c t =
      (X.presheaf.map (homOfLE (𝒲.ointer_le_preimage_ointer_comp h 𝒦 lam hlam t)).op).hom
        ((h.app (𝒦.ointer (lam ∘ t))).hom (c (lam ∘ t)))

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