Module

CompactOpenPresentable.lean

Nyll.SchemeTheory.Topology.CompactOpenPresentable

1 declaration indexed from sourceView source ↗

Module documentation

Finite presentability of compact-open generators

Maps from the actual sheafified one-generator free representable are sections over the corresponding open. For a compact open, the naturality of this correspondence transfers preservation of filtered colimits from the sections functor to the represented Hom functor.

No subcanonicity instance is needed: the generator is defined by actual sheafification. This is an input to the finite-presentation argument in Stacks Project, tag 0CAI: https://stacks.math.columbia.edu/tag/0CAI. The Lean proof is original.

Imports3

Mathlib.CategoryTheory.Presentable.Finite
Nyll.SchemeTheory.Topology.CompactOpenGenerators
Nyll.SchemeTheory.Topology.CompactOpenSections

Imported by1

Nyll.SchemeTheory.Topology.All

theorem

isFinitelyPresentable_openGenerator

L37 ↗

SchemeTheory.isFinitelyPresentable_openGenerator

Documentation

The sheafified free representable with one generator on a compact open is a finitely presentable object of the topological sheaf category.

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 : TopCat.{u}} [PrespectralSpace X] [QuasiSeparatedSpace X]

Lean source · statement

theorem isFinitelyPresentable_openGenerator
    (U : Opens X) (hU : IsCompact (U : Set X)) :
    IsFinitelyPresentable.{u} (openGenerator U)

Module documentation

Finite presentability of compact-open generators

Declarations

isFinitelyPresentable_openGenerator