Module

SheafApproximationGerms.lean

Nyll.SchemeTheory.Topology.SheafApproximationGerms

3 declarations indexed from sourceView source ↗

Module documentation

Germs of actual sheaf approximation maps

The inverse-image stalk comparison identifies approximation counits with direct-image stalk maps. Refinement acts on germs by restriction between inverse images of open neighborhoods. Taking the neighborhoods to be principal opens gives the stalk calculation for finite models.

The Lean proofs are original.

Imports4

Nyll.SchemeTheory.Topology.FiniteModelSheafTransitions
Nyll.SchemeTheory.Topology.SheafPullbackGerms
Mathlib.Topology.Sheaves.Functors
Mathlib.Topology.Sheaves.Stalks

Imported by2

theorem

sheafStalkPullbackIso_hom_counit

L35 ↗

SchemeTheory.sheafStalkPullbackIso_hom_counit

Documentation

Under the actual inverse-image stalk comparison, the counit is the usual morphism from a direct-image stalk.

Source context 5 commands

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

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

Lean source · statement

theorem sheafStalkPullbackIso_hom_counit (q : X ⟶ Y)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) (x : X) :
    (sheafStalkPullbackIso q ((TopCat.Sheaf.pushforward (Type u) q).obj F) x).hom ≫
        (TopCat.Presheaf.stalkFunctor (Type u) x).map
          ((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) q).counit.app F).hom =
      TopCat.Presheaf.stalkPushforward (Type u) q F.obj x

theorem

sheafApproximationTransition_unit

L87 ↗

SchemeTheory.sheafApproximationTransition_unit

Documentation

The approximation transition is the adjoint of the direct image of the finer unit.

Source context 5 commands

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

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

Lean source · statement

theorem sheafApproximationTransition_unit (q : X ⟶ Y) (p : Y ⟶ Z)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    (TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) (q ≫ p)).unit.app
        ((TopCat.Sheaf.pushforward (Type u) (q ≫ p)).obj F) ≫
        (TopCat.Sheaf.pushforward (Type u) (q ≫ p)).map
          (sheafApproximationTransition q p F) =
      (TopCat.Sheaf.pushforward (Type u) p).map
        ((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) q).unit.app
          ((TopCat.Sheaf.pushforward (Type u) q).obj F))

theorem

sheafApproximationTransition_germ

L119 ↗

SchemeTheory.sheafApproximationTransition_germ

Documentation

On germs, refinement of an actual approximation is restriction between the two inverse-image neighborhoods.

Source context 5 commands

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

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

Lean source · statement

theorem sheafApproximationTransition_germ (q : X ⟶ Y) (p : Y ⟶ Z)
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) (x : X)
    (U : Opens Z) (V : Opens Y) (i : V ⟶ (Opens.map p).obj U) (hx : q x ∈ V) :
    TopCat.Presheaf.germ ((TopCat.Sheaf.pushforward (Type u) (q ≫ p)).obj F).obj
        U ((q ≫ p) x) (i.le hx) ≫
        (sheafStalkPullbackIso (q ≫ p)
          ((TopCat.Sheaf.pushforward (Type u) (q ≫ p)).obj F) x).hom ≫
        (TopCat.Presheaf.stalkFunctor (Type u) x).map
          (sheafApproximationTransition q p F).hom =
      ((TopCat.Sheaf.pushforward (Type u) q).obj F).obj.map i.op ≫
        TopCat.Presheaf.germ ((TopCat.Sheaf.pushforward (Type u) q).obj F).obj
          V (q x) hx ≫
        (sheafStalkPullbackIso q ((TopCat.Sheaf.pushforward (Type u) q).obj F) x).hom

Module documentation

Germs of actual sheaf approximation maps

Declarations

sheafStalkPullbackIso_hom_counit

sheafApproximationTransition_unit

sheafApproximationTransition_germ