Module

SpectralClosedSubspaceRestriction.lean

Nyll.SchemeTheory.Topology.SpectralClosedSubspaceRestriction

3 declarations indexed from sourceView source ↗

Module documentation

The closed-support reduction for spectral restriction

Closed subspaces of spectral spaces are spectral. The connected point-closure intersection condition restricts to each closed subspace, because the closure of any point of that subspace remains in it. Thus the locally constant extension theorem applies on every closed support, as required in Stacks Project, tag 09ZG.

Reference: https://stacks.math.columbia.edu/tag/09ZG. The Lean proofs are original.

Imports6

Mathlib.Topology.Connected.Basic
Mathlib.Topology.Maps.Proper.Basic
Mathlib.Topology.QuasiSeparated
Mathlib.Topology.Sober
Mathlib.Topology.Spectral.Basic
Nyll.SchemeTheory.Topology.SpectralClosedRestriction

Imported by3

theorem

spectralSpace_closedSubtype

L39 ↗

SchemeTheory.spectralSpace_closedSubtype

Documentation

A closed subspace of a spectral space is spectral. Its compact-open basis is obtained by intersecting ambient compact opens with the subspace.

Source context 5 commands

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

noncomputable section
universe u
open Set TopologicalSpace Topology
namespace SchemeTheory
variable {X : Type u} [TopologicalSpace X]

Lean source · statement

theorem spectralSpace_closedSubtype [SpectralSpace X] {C : Set X} (hC : IsClosed C) :
    SpectralSpace C

theorem

connected_closed_intersections_on_closedSubset

L69 ↗

SchemeTheory.connected_closed_intersections_on_closedSubset

Documentation

The original connected, nonempty point-closure condition holds on every closed support, with no additional geometric assumption.

Source context 5 commands

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

noncomputable section
universe u
open Set TopologicalSpace Topology
namespace SchemeTheory
variable {X : Type u} [TopologicalSpace X]

Lean source · statement

theorem connected_closed_intersections_on_closedSubset {Z C : Set X} (hC : IsClosed C)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X))) (x : C) :
    IsConnected ((Subtype.val ⁻¹' Z : Set C) ∩ closure ({x} : Set C))

theorem

locallyConstant_closedSupport_restriction_bijective

L92 ↗

SchemeTheory.locallyConstant_closedSupport_restriction_bijective

Documentation

Locally constant functions on the intersection of two closed subsets extend uniquely over the closed support under the original hypotheses.

Source context 5 commands

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

noncomputable section
universe u
open Set TopologicalSpace Topology
namespace SchemeTheory
variable {X : Type u} [TopologicalSpace X]

Lean source · statement

theorem locallyConstant_closedSupport_restriction_bijective [SpectralSpace X]
    {Z C : Set X} (hZ : IsClosed Z) (hC : IsClosed C)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X))) (A : Type*) :
    Function.Bijective (LocallyConstant.comap
      (⟨Subtype.val, continuous_subtype_val⟩ : C((Subtype.val ⁻¹' Z : Set C), C)) :
        LocallyConstant C A → LocallyConstant (Subtype.val ⁻¹' Z : Set C) A)

Module documentation

The closed-support reduction for spectral restriction

Declarations

spectralSpace_closedSubtype

connected_closed_intersections_on_closedSubset

locallyConstant_closedSupport_restriction_bijective