Module

FiniteSkyscraperEmbedding.lean

Nyll.SchemeTheory.Topology.FiniteSkyscraperEmbedding

4 declarations indexed from sourceView source ↗

Module documentation

The actual stalk-skyscraper embedding

The units of the stalk-skyscraper adjunction give a monomorphism from a sheaf into the product of its stalk skyscrapers. The proof uses the adjunction triangle to split every stalk map, then the conservativity of stalks for monomorphisms.

For a finite topological space this is a finite product indexed explicitly by Fin n. This is the finite-space embedding step of Stacks Project, tag 0CAL: https://stacks.math.columbia.edu/tag/0CAL. The finite-space reduction and the closed-constant comparison are separate requirements; neither is assumed or asserted here.

Imports6

Mathlib.CategoryTheory.Limits.Shapes.Products
Mathlib.CategoryTheory.EpiMono
Mathlib.Data.Fintype.EquivFin
Mathlib.Topology.Sheaves.Limits
Mathlib.Topology.Sheaves.Skyscraper
Mathlib.Topology.Sheaves.Stalks

Imported by3

abbrev

stalkSkyscraper

L40 ↗

SchemeTheory.stalkSkyscraper

Documentation

The skyscraper at a point, with its actual stalk as value.

Source context 5 commands

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

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

Lean source · statement

abbrev stalkSkyscraper (F : X.Sheaf (Type u)) (x : X) : X.Sheaf (Type u)

def

toStalkSkyscrapers

L45 ↗

SchemeTheory.toStalkSkyscrapers

Documentation

The actual product of the adjunction units.

Source context 5 commands

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

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

Lean source · statement

def toStalkSkyscrapers (F : X.Sheaf (Type u)) :
    F ⟶ ∏ᶜ (stalkSkyscraper F)

theorem

mono_toStalkSkyscrapers

L52 ↗

SchemeTheory.mono_toStalkSkyscrapers

Documentation

Every stalk map of the product unit is split by a product projection followed by the counit, so the original sheaf map is a monomorphism.

Source context 5 commands

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

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

Lean source · statement

theorem mono_toStalkSkyscrapers (F : X.Sheaf (Type u)) :
    Mono (toStalkSkyscrapers F)

theorem

exists_finite_skyscraper_embedding

L79 ↗

SchemeTheory.exists_finite_skyscraper_embedding

Documentation

On an actual finite topological space the stalk embedding has finitely many factors; the points are enumerated rather than supplied as missing covering data.

Source context 5 commands

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

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

Lean source · full declaration

theorem exists_finite_skyscraper_embedding [Finite X] (F : X.Sheaf (Type u)) :
    ∃ (n : ℕ) (p : Fin n → X) (m : F ⟶ ∏ᶜ (fun i => stalkSkyscraper F (p i))),
      Mono m := by
  classical
  let : Fintype X := Fintype.ofFinite X
  let e : X ≃ Fin (Fintype.card X) := Fintype.equivFin X
  have : Mono (toStalkSkyscrapers F) := mono_toStalkSkyscrapers F
  refine ⟨Fintype.card X, e.symm,
    toStalkSkyscrapers F ≫ (Pi.reindex e.symm (stalkSkyscraper F)).inv, ?_⟩
  infer_instance

Module documentation

The actual stalk-skyscraper embedding

Declarations

stalkSkyscraper

toStalkSkyscrapers

mono_toStalkSkyscrapers

exists_finite_skyscraper_embedding