Module

SheafPullbackStalks.lean

Nyll.SchemeTheory.Topology.SheafPullbackStalks

2 declarations indexed from sourceView source ↗

Module documentation

Stalks of the actual inverse-image sheaf

The chosen left adjoint defining topological sheaf pullback is compared with sheafification of presheaf pullback. The adjunction units are related using uniqueness of the left adjoint and the unit formula for restricting an adjunction to a full subcategory. The stalk comparison is then built from presheaf pullback and invariance of stalks under sheafification.

The Lean proofs are original.

Imports5

Mathlib.CategoryTheory.Adjunction.Restrict
Mathlib.CategoryTheory.Adjunction.Unique
Mathlib.Topology.Sheaves.Functors
Mathlib.Topology.Sheaves.Sheafify
Mathlib.Topology.Sheaves.Stalks

Imported by7

theorem

sheafPullback_unit_comparison

L37 ↗

SchemeTheory.sheafPullback_unit_comparison

Documentation

The actual sheaf pullback unit becomes the composed presheaf-pullback and sheafification unit under the canonical comparison isomorphism.

Source context 5 commands

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

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

Lean source · statement

theorem sheafPullback_unit_comparison (f : X ⟶ Y)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u)) :
    ((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app F).hom ≫
        (TopCat.Presheaf.pushforward (Type u) f).map
          (((TopCat.Sheaf.pullbackIso (Type u) f).hom.app F).hom) =
      (TopCat.Presheaf.pullbackPushforwardAdjunction (Type u) f).unit.app F.obj ≫
        (TopCat.Presheaf.pushforward (Type u) f).map
          (CategoryTheory.toSheafify (Opens.grothendieckTopology X)
            ((TopCat.Presheaf.pullback (Type u) f).obj F.obj))

def

sheafStalkPullbackIso

L80 ↗

SchemeTheory.sheafStalkPullbackIso