Module

OrderedAffineCoverCechCup.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OrderedAffineCoverCechCup

8 declarations indexed from sourceView source ↗

Module documentation

Ordered Affine Cover Cech Cup

Imports1

Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech

Imported by7

def

frontFace

L32 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.frontFace

Documentation

The front face used to evaluate the first factor of a Cech cup product.

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 frontFace (a b n : ℕ) (h : a + b = n) (s : K.Idx n) : K.Idx a

def

backFace

L36 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.backFace

Documentation

The back face used to evaluate the second factor of a Cech cup product.

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 backFace (a b n : ℕ) (h : a + b = n) (s : K.Idx n) : K.Idx b

theorem

frontFace_apply

L40 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.frontFace_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 frontFace_apply (a b n : ℕ) (h : a + b = n) (s : K.Idx n) (j : Fin (a + 1)) :
    (K.frontFace a b n h s).1 j = s.1 ⟨j.1, by omega⟩ :=
  rfl

theorem

backFace_apply

L44 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.backFace_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 backFace_apply (a b n : ℕ) (h : a + b = n) (s : K.Idx n) (j : Fin (b + 1)) :
    (K.backFace a b n h s).1 j = s.1 ⟨a + j.1, by omega⟩ :=
  rfl

theorem

inter_le_inter_frontFace

L48 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.inter_le_inter_frontFace

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_le_inter_frontFace (a b n : ℕ) (h : a + b = n) (s : K.Idx n) :
    K.inter s ≤ K.inter (K.frontFace a b n h s)

theorem

inter_le_inter_backFace

L52 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.inter_le_inter_backFace

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_le_inter_backFace (a b n : ℕ) (h : a + b = n) (s : K.Idx n) :
    K.inter s ≤ K.inter (K.backFace a b n h s)

def

cup

L64 ↗

AlgebraicGeometry.OModulePresheaf.cup

Documentation

The Cech cup product defined by restricting to the front and back faces.

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 cup (a b n : ℕ) (h : a + b = n) (α : (unit π).cochain K a) (β : F.cochain K b) : F.cochain K
  n

theorem

cup_apply

L70 ↗

AlgebraicGeometry.OModulePresheaf.cup_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 cup_apply (a b n : ℕ) (h : a + b = n) (α : (unit π).cochain K a) (β : F.cochain K b) (s
  : K.Idx n) :
    F.cup K a b n h α β s =
      (V.presheaf.map (homOfLE (K.inter_le_inter_frontFace a b n h s)).op).hom (α (K.frontFace a
        b n h s))
        • F.res (K.inter_le_inter_backFace a b n h s) (β (K.backFace a b n h s))

Module documentation

Ordered Affine Cover Cech Cup

Declarations