Module

CompactOpenGenerators.lean

Nyll.SchemeTheory.Topology.CompactOpenGenerators

6 declarations indexed from sourceView source ↗

Module documentation

Compact-open generators of topological sheaves

The actual sheafifications of the free representables on compact opens form a strong generator on a prespectral space. Their maps into a sheaf are its sections on those opens. Compact-open neighbourhoods therefore detect equality and supply the local lifts needed to detect isomorphisms.

This is the generator part of the finite-presentation argument in the Stacks Project, tag 0CAI: https://stacks.math.columbia.edu/tag/0CAI. The Lean proof is original and uses Mathlib's sheafified free representables.

Imports8

Mathlib.CategoryTheory.Generator.Sheaf
Mathlib.CategoryTheory.Generator.StrongGenerator
Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
Mathlib.CategoryTheory.Sites.ConcreteSheafification
Mathlib.CategoryTheory.Sites.LocallyBijective
Mathlib.Topology.Sheaves.Sheaf
Mathlib.Topology.Sheaves.LocallySurjective
Mathlib.Topology.Spectral.Prespectral

Imported by2

def

openGenerator

L40 ↗

SchemeTheory.openGenerator

Documentation

The actual sheafified free representable, with one generator, on an open.

Source context 5 commands

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

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

Lean source · statement

def openGenerator (U : Opens X) : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)

def

openGeneratorHomEquiv

L44 ↗

SchemeTheory.openGeneratorHomEquiv

Documentation

Maps from the sheafified open representable are actual sections.

Source context 5 commands

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

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

Lean source · statement

def openGeneratorHomEquiv {U : Opens X}
    {F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)} :
    (openGenerator U ⟶ F) ≃ F.obj.obj (op U)

theorem

openGeneratorHomEquiv_comp

L51 ↗

SchemeTheory.openGeneratorHomEquiv_comp

Documentation

The section represented by a composite is the image of the represented section.

Source context 5 commands

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

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

Lean source · statement

theorem openGeneratorHomEquiv_comp {U : Opens X}
    {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)}
    (α : openGenerator U ⟶ F) (f : F ⟶ G) :
    openGeneratorHomEquiv (α ≫ f) = f.hom.app (op U) (openGeneratorHomEquiv α)

def