For a finite set S of compact opens, the space Space S consists of the membership patterns actually realized by points of X. It has the upper-set topology for inclusion of patterns. Forgetting coordinates gives continuous refinement maps with exact identity, composition, and quotient compatibility laws.
Principal opens pull back to finite intersections of compact opens. The resulting neighborhoods shrink under refinement and are cofinal among all open neighborhoods on a prespectral space. These are actual finite models for sheaf approximation; no sheaf descent is assumed. The Lean proof is original.
The compact opens in S that contain a point.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}def pattern (S : Finset (CompactOpens X)) (x : X) : Set SThe finite space of realized membership patterns, ordered by inclusion.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}abbrev Space (S : Finset (CompactOpens X)) : TopCat.{u}Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}instance finite_space (S : Finset (CompactOpens X)) : Finite (Space S)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}def quotientFn (S : Finset (CompactOpens X)) (x : X) : Space SThe open intersection specified by a realized pattern.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}def principalPreimage (S : Finset (CompactOpens X)) (p : Space S) : Opens XSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem mem_principalPreimage (S : Finset (CompactOpens X)) (p : Space S) (x : X) :
x ∈ principalPreimage S p ↔
∀ U : S, U ∈ (WithUpperSet.ofUpperSet p).1 → x ∈ (U.1 : Set X)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem quotientFn_preimage (S : Finset (CompactOpens X))
(W : Set (Space S)) (hW : IsOpen W) :
quotientFn S ⁻¹' W = ⋃ p ∈ W, (principalPreimage S p : Set X)The actual continuous quotient map recording the finite family.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}def quotient (S : Finset (CompactOpens X)) : X ⟶ Space SSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem quotient_apply (S : Finset (CompactOpens X)) (x : X) :
quotient S x = WithUpperSet.toUpperSet ⟨pattern S x, ⟨x, rfl⟩⟩Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem quotient_surjective (S : Finset (CompactOpens X)) :
Function.Surjective (quotient S)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem principal_preimage (S : Finset (CompactOpens X)) (p : Space S) :
(Opens.map (quotient S)).obj (Alexandrov.principalOpen p) =
principalPreimage S pSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem principalPreimage_isCompact [CompactSpace X] [QuasiSeparatedSpace X]
(S : Finset (CompactOpens X)) (p : Space S) :
IsCompact (principalPreimage S p : Set X)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem quotient_isSpectralMap [CompactSpace X] [QuasiSeparatedSpace X]
(S : Finset (CompactOpens X)) : IsSpectralMap (quotient S)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}def restrictPattern {S T : Finset (CompactOpens X)} (h : S ⊆ T) :
Set.range (pattern T) →o Set.range (pattern S) where
toFun p := ⟨(fun U : S => (⟨U.1, h U.2⟩ : T)) ⁻¹' p.1, by
obtain ⟨x, hx⟩ := p.2
refine ⟨x, ?_⟩
rw [← hx]
rfl⟩
monotone' := fun _ _ hp _ hU => hp hUForgetting extra compact-open coordinates defines a refinement map.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}def refinement {S T : Finset (CompactOpens X)} (h : S ⊆ T) : Space T ⟶ Space SSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem quotient_comp {S T : Finset (CompactOpens X)} (h : S ⊆ T) :
quotient T ≫ refinement h = quotient SSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem refinement_refl (S : Finset (CompactOpens X)) :
refinement (Finset.Subset.refl S) = 𝟙 (Space S)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem refinement_comp {S T R : Finset (CompactOpens X)}
(hST : S ⊆ T) (hTR : T ⊆ R) :
refinement hTR ≫ refinement hST = refinement (hST.trans hTR)The inverse image of the smallest finite-model neighborhood of x.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}def neighborhood (S : Finset (CompactOpens X)) (x : X) : Opens XSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem mem_neighborhood (S : Finset (CompactOpens X)) (x y : X) :
y ∈ neighborhood S x ↔ ∀ U ∈ S, x ∈ (U : Set X) → y ∈ (U : Set X)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem self_mem_neighborhood (S : Finset (CompactOpens X)) (x : X) :
x ∈ neighborhood S xSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem neighborhood_preimage (S : Finset (CompactOpens X)) (x : X) :
(Opens.map (quotient S)).obj (Alexandrov.principalOpen (quotient S x)) =
neighborhood S xSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem neighborhood_isCompact [CompactSpace X] [QuasiSeparatedSpace X]
(S : Finset (CompactOpens X)) (x : X) : IsCompact (neighborhood S x : Set X)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem neighborhood_antitone {S T : Finset (CompactOpens X)}
(h : S ⊆ T) (x : X) : neighborhood T x ≤ neighborhood S xOn a prespectral space the principal preimages are cofinal among open neighborhoods: one compact-open coordinate already suffices.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Topology
namespace SchemeTheory.CompactOpenFiniteModel
variable {X : TopCat.{u}}theorem exists_neighborhood_le [PrespectralSpace X] (x : X)
(V : Opens X) (hx : x ∈ V) :
∃ S : Finset (CompactOpens X), neighborhood S x ≤ V