Module

FiniteModelSheafTransitions.lean

Nyll.SchemeTheory.Topology.FiniteModelSheafTransitions

8 declarations indexed from sourceView source ↗

Module documentation

Actual sheaf approximation maps under refinement of a space

For a continuous map q, the approximation to a sheaf F is the actual inverse image of its direct image, with its adjunction counit to F. Factoring a map through a finer space gives a map between these actual approximations. It is the adjoint of the finer unit after direct image. The triangle identities prove compatibility with the counits, and the same Hom equivalence proves identity and composition under refinement.

These maps are used to construct the finite-model approximation diagram in the proof of Stacks Project, tag 09ZG: https://stacks.math.columbia.edu/tag/09ZG. The Lean proof is original.

Imports1

Mathlib.Topology.Sheaves.Functors

Imported by3

abbrev

actualSheafPullback

L36 ↗

SchemeTheory.actualSheafPullback

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SchemeTheory
variable {X Y Z W : TopCat.{u}}

Lean source · statement

abbrev actualSheafPullback (q : X ⟶ Y) :
    CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u) ⥤
      CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)

abbrev

actualSheafPushforward

L41 ↗

SchemeTheory.actualSheafPushforward

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SchemeTheory
variable {X Y Z W : TopCat.{u}}

Lean source · statement

abbrev actualSheafPushforward (q : X ⟶ Y) :
    CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u) ⥤
      CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u)

abbrev

actualSheafAdjunction

L46 ↗

SchemeTheory.actualSheafAdjunction

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SchemeTheory
variable {X Y Z W : TopCat.{u}}

Lean source · statement

abbrev actualSheafAdjunction (q : X ⟶ Y) :
    actualSheafPullback q ⊣ actualSheafPushforward q

abbrev

sheafApproximation

L51 ↗

SchemeTheory.sheafApproximation

Documentation

The actual inverse image of the direct image of a sheaf.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SchemeTheory
variable {X Y Z W : TopCat.{u}}

Lean source · statement

abbrev sheafApproximation (q : X ⟶ Y)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)

def

sheafApproximationTransition

L58 ↗

SchemeTheory.sheafApproximationTransition

Documentation

Refinement acts on actual sheaf approximations by the adjoint of the direct image of the finer adjunction unit.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SchemeTheory
variable {X Y Z W : TopCat.{u}}

Lean source · statement

def sheafApproximationTransition (q : X ⟶ Y) (p : Y ⟶ Z)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    sheafApproximation (q ≫ p) F ⟶ sheafApproximation q F

theorem

sheafApproximationTransition_counit

L77 ↗

SchemeTheory.sheafApproximationTransition_counit

Documentation

Approximation refinement commutes with the actual adjunction counits.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SchemeTheory
variable {X Y Z W : TopCat.{u}}

Lean source · statement

theorem sheafApproximationTransition_counit (q : X ⟶ Y) (p : Y ⟶ Z)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    sheafApproximationTransition q p F ≫
        (actualSheafAdjunction q).counit.app F =
      (actualSheafAdjunction (q ≫ p)).counit.app F

theorem

sheafApproximationTransition_id

L111 ↗

SchemeTheory.sheafApproximationTransition_id

Documentation

Refining by the identity map gives the identity approximation map.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SchemeTheory
variable {X Y Z W : TopCat.{u}}

Lean source · statement

theorem sheafApproximationTransition_id (q : X ⟶ Y)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    sheafApproximationTransition q (𝟙 Y) F = 𝟙 (sheafApproximation q F)

theorem

sheafApproximationTransition_comp

L119 ↗

SchemeTheory.sheafApproximationTransition_comp

Documentation

The actual approximation maps compose when finite-space refinements compose.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SchemeTheory
variable {X Y Z W : TopCat.{u}}

Lean source · statement

theorem sheafApproximationTransition_comp (q : X ⟶ Y) (p : Y ⟶ Z) (r : Z ⟶ W)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    sheafApproximationTransition (q ≫ p) r F ≫ sheafApproximationTransition q p F =
      sheafApproximationTransition q (p ≫ r) F

Module documentation

Actual sheaf approximation maps under refinement of a space

Declarations