NYLL
Module

FiniteModelSheafDiagram.lean

Nyll.SchemeTheory.Topology.FiniteModelSheafDiagram
2 declarations indexed from sourceView source ↗

Module documentation

The actual diagram of finite-model sheaf approximations

Finite families of compact opens form a filtered index category. Their realized membership spaces and coordinate-forgetting maps give the actual approximations q⁻¹q_*F, with transition maps adjoint to the finer unit. The actual counits form a cocone with vertex F.

This is the finite-model diagram used in the proof of Stacks Project, tag 09ZG: https://stacks.math.columbia.edu/tag/09ZG. The Lean constructions and proofs are original.

Imports4
Imported by4

Declarations

def

sheafDiagram

L37 ↗
SchemeTheory.CompactOpenFiniteModel.sheafDiagram
Documentation

The actual inverse-image/direct-image approximations indexed by finite families of compact opens, with their coherent refinement maps.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}
Lean source · full declaration
def sheafDiagram (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    Finset (CompactOpens X) ⥤
      CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u) where
  obj S := sheafApproximation (quotient S) F
  map {S T} h := sheafApproximationTransition (quotient T) (refinement (leOfHom h)) F
  map_id S := by
    exact sheafApproximationTransition_id (quotient S) F
  map_comp {S T R} h k := by
    exact (sheafApproximationTransition_comp (quotient R)
      (refinement (leOfHom k)) (refinement (leOfHom h)) F).symm
def

sheafCocone

L50 ↗
SchemeTheory.CompactOpenFiniteModel.sheafCocone
Documentation

The actual adjunction counits form a cocone from the finite-model diagram to the original sheaf.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}
Lean source · full declaration
def sheafCocone (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    Cocone (sheafDiagram F) where
  pt := F
  ι :=
    { app := fun S =>
        (TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) (quotient S)).counit.app F
      naturality := fun S T h => by
        let eS : sheafApproximation (quotient S) F ⟶ F :=
          (TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) (quotient S)).counit.app F
        let eT : sheafApproximation (quotient T) F ⟶ F :=
          (TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) (quotient T)).counit.app F
        let t : sheafApproximation (quotient S) F ⟶ sheafApproximation (quotient T) F :=
          sheafApproximationTransition (quotient T) (refinement (leOfHom h)) F
        have he : t ≫ eT = eS := sheafApproximationTransition_counit (quotient T)
          (refinement (leOfHom h)) F
        change t ≫ eT = eS ≫ 𝟙 F
        exact he.trans (Category.comp_id eS).symm }

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