1.5. w-local spaces
Definition1.5.1
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 10
Associated Lean declarations
-
WLocalSpace[complete]
A topological space X is w-local if it satisfies:
-
Xis spectral, -
every point specializes to a unique closed point,
-
the subspace
X^cof closed points is closed.
(Bhatt–Scholze, Definition 2.1.1; Stacks Project, Tag 096A)
Lean code for Definition1.5.1●1 definition
Associated Lean declarations
-
WLocalSpace[complete]
Associated Lean declarations
-
WLocalSpace[complete]
-
classdefined in Proetale/Topology/SpectralSpace/WLocal/Basic.leancomplete
class WLocalSpace.{u_1} (X : Type u_1) [TopologicalSpace X] : Prop
class WLocalSpace.{u_1} (X : Type u_1) [TopologicalSpace X] : Prop
A spectral space is w-local if every point specializes to a unique closed point and the set of closed points is closed. Note: In a spectral space, every point specializes to a closed point, so we only require the uniqueness.
Extends
-
SpectralSpace X
Methods
t0 : ∀ ⦃x y : X⦄, Inseparable x y → x = y
Inherited from-
SpectralSpace -
T0Space
isCompact_univ : IsCompact Set.univ
Inherited from-
SpectralSpace -
CompactSpace
sober : ∀ {S : Set X}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S
Inherited from-
SpectralSpace -
QuasiSober
inter_isCompact : ∀ (U V : Set X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
Inherited from-
SpectralSpace -
QuasiSeparatedSpace
isTopologicalBasis : TopologicalSpace.IsTopologicalBasis {U | IsOpen U ∧ IsCompact U}
Inherited from-
SpectralSpace -
PrespectralSpace
eq_of_specializes : ∀ {x c c' : X}, IsClosed {c} → IsClosed {c'} → x ⤳ c → x ⤳ c' → c = c'
Any two closed specializations of a point are equal.
isClosed_closedPoints : IsClosed (closedPoints X)
The set of closed points is closed.
-
Definition1.5.2
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 4
Associated Lean declarations
-
IsWLocalMap[complete]
Let X and Y be w-local spaces. A morphism f \colon X \to Y is w-local
if it is spectral and the image of closed points f(X^c) \subseteq Y^c.
(Bhatt–Scholze, Definition 2.1.1; Stacks Project,
Tag 096A)
Lean code for Definition1.5.2●1 definition
Associated Lean declarations
-
IsWLocalMap[complete]
Associated Lean declarations
-
IsWLocalMap[complete]
-
structuredefined in Proetale/Topology/SpectralSpace/WLocal/Basic.leancomplete
structure IsWLocalMap.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop
structure IsWLocalMap.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop
A w-local map is a spectral map that maps closed points to closed points.
Extends
-
IsSpectralMap f
Fields
isOpen_preimage : ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)
Inherited from-
IsSpectralMap -
Continuous
isCompact_preimage_of_isOpen : ∀ ⦃s : Set Y⦄, IsOpen s → IsCompact s → IsCompact (f ⁻¹' s)
Inherited from-
IsSpectralMap
closedPoints_subset_preimage_closedPoints : closedPoints X ⊆ f ⁻¹' closedPoints Y
-
Definition1.5.3
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Lean status
- No associated Lean code or declarations.
Let X and Y be w-local spaces. A morphism f \colon X \to Y is
w-purely-local if f^{-1}(Y^c) = X^c.
Obviously, every w-purely-local morphism is w-local.
Lemma1.5.4
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Statement uses 2
Associated Lean declarations
-
IsWLocalMap.comp[complete]
Let f \colon X \to Y and g \colon Y \to Z be w-local maps between w-local
spaces. Then the composition g \circ f \colon X \to Z is w-local.
Lean code for Lemma1.5.4●1 theorem
Associated Lean declarations
-
IsWLocalMap.comp[complete]
Associated Lean declarations
-
IsWLocalMap.comp[complete]
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/Basic.leancomplete
theorem IsWLocalMap.comp.{u_1, u_2, u_3} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsWLocalMap f) (hg : IsWLocalMap g) : IsWLocalMap (g ∘ f)
theorem IsWLocalMap.comp.{u_1, u_2, u_3} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsWLocalMap f) (hg : IsWLocalMap g) : IsWLocalMap (g ∘ f)
Lemma1.5.5
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 2
Associated Lean declarations
Let X be w-local and Z \subseteq X a subset closed under specialization.
Then the generalization Z^g in X is still closed under specialization.
Lean code for Lemma1.5.5●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/Basic.leancomplete
theorem StableUnderSpecialization.generalizationHull_of_wLocalSpace.{u_1} {X : Type u_1} [TopologicalSpace X] [WLocalSpace X] {s : Set X} (hs : StableUnderSpecialization s) : StableUnderSpecialization (generalizationHull s)
theorem StableUnderSpecialization.generalizationHull_of_wLocalSpace.{u_1} {X : Type u_1} [TopologicalSpace X] [WLocalSpace X] {s : Set X} (hs : StableUnderSpecialization s) : StableUnderSpecialization (generalizationHull s)
Proof for Lemma 1.5.5
uses 0
Let x \rightsquigarrow y in X with x \in Z^g. Then x specializes to
some z \in Z, which in turn specializes to a unique closed point c in X
because X is w-local. Because Z is stable under specialization,
c \in Z. Also y specializes to a unique closed point c' in X and by
uniqueness we have c' = c \in Z. Hence y \in Z^g.
Lemma1.5.6
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 2
Associated Lean declarations
Let X be w-local and Z \subseteq X a subset closed under specialization.
If Z is spectral, it is w-local and the inclusion Z \to X maps closed
points to closed points.
Lean code for Lemma1.5.6●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/Basic.leancomplete
theorem Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsEmbedding f) (h : StableUnderSpecialization (Set.range f)) [SpectralSpace X] [WLocalSpace Y] : WLocalSpace X
theorem Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsEmbedding f) (h : StableUnderSpecialization (Set.range f)) [SpectralSpace X] [WLocalSpace Y] : WLocalSpace X
Proof for Lemma 1.5.6
Since Z is closed under specializations, we have Z^c = X^c \cap Z. In
particular Z^c is closed in Z and Z \to X preserves closed points. By
Lemma 1.1.10, specializations in Z are the
same as specializations in X. Since Z is closed under specializations,
every point in Z specializes to a unique closed point in X and therefore
in Z.
Lemma1.5.7
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Statement uses 2
Associated Lean declarations
-
Topology.IsClosedEmbedding.wLocalSpace[complete]
Let X be a w-local space. Then every closed subspace Y \subseteq X is
w-local. Moreover, the inclusion map Y \to X is w-local.
(Stacks Project, Tag 096B)
Lean code for Lemma1.5.7●1 theorem
Associated Lean declarations
-
Topology.IsClosedEmbedding.wLocalSpace[complete]
Associated Lean declarations
-
Topology.IsClosedEmbedding.wLocalSpace[complete]
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/Basic.leancomplete
theorem Topology.IsClosedEmbedding.wLocalSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsClosedEmbedding f) [WLocalSpace Y] : WLocalSpace X
theorem Topology.IsClosedEmbedding.wLocalSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsClosedEmbedding f) [WLocalSpace Y] : WLocalSpace X
Proof for Lemma 1.5.7
This follows from Lemma 1.5.6, because
closed subsets are stable under specialization. The inclusion Y \to X is
spectral as a closed embedding and hence w-local by the lemma.
Lemma1.5.8
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Associated Lean declarations
Let X be a profinite topological space and x, y \in X be distinct. Then
there exist U, V \subseteq X open and closed such that X = U \coprod V and
x \in U, y \in V.
Lean code for Lemma1.5.8●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Mathlib/Topology/Separation/Profinite.leancomplete
theorem instTotallySeparatedSpaceOfTotallyDisconnectedSpace.{u_3} {H : Type u_3} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] : TotallySeparatedSpace H
theorem instTotallySeparatedSpaceOfTotallyDisconnectedSpace.{u_3} {H : Type u_3} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] : TotallySeparatedSpace H
A totally disconnected compact Hausdorff space is totally separated.
Proof for Lemma 1.5.8
uses 0
Write X = \lim_{i \in I} X_i as a directed limit of finite discrete spaces.
Let \pi_i \colon X \to X_i be the projection maps. A base of the open sets of
X is given by the preimages \pi_i^{-1}(\{z\}) for z \in X_i and
i \in I. Every open set in this base is also closed, because its complement
is a finite union of such sets.
Choose an open subset in this base containing x but not y, say
U = \pi_{i_0}^{-1}(\{z_0\}) for some i_0 \in I and z_0 \in X_{i_0}.
Then V = X - U is also open and closed, and we have X = U \coprod V with
x \in U and y \in V.
Lemma1.5.9
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Associated Lean declarations
-
SpectralSpace.totallySeparatedSpace[complete]
Let X be a spectral space such that every point is closed. Then X is
profinite.
(Stacks Project, Tag 0905, (6) ⟹ (1))
Lean code for Lemma1.5.9●1 theorem
Associated Lean declarations
-
SpectralSpace.totallySeparatedSpace[complete]
Associated Lean declarations
-
SpectralSpace.totallySeparatedSpace[complete]
-
theoremdefined in Proetale/Topology/SpectralSpace/Constructible.leancomplete
theorem SpectralSpace.totallySeparatedSpace.{u_1} {X : Type u_1} [TopologicalSpace X] [SpectralSpace X] [T1Space X] : TotallySeparatedSpace X
theorem SpectralSpace.totallySeparatedSpace.{u_1} {X : Type u_1} [TopologicalSpace X] [SpectralSpace X] [T1Space X] : TotallySeparatedSpace X
[Stacks Tag 0905](https://stacks.math.columbia.edu/tag/0905) ((6) → (1))
Proof for Lemma 1.5.9
Since every point is closed, there are no nontrivial specializations between
points. By part (2) of Lemma 1.5.14,
all constructible subsets of X are closed. In particular, every compact open
subset is also closed. Since X is spectral, thus T0, for any two points there
is a quasi-compact open (also closed) containing exactly one of them. Thus X
is profinite by isTotallyDisconnected_of_isClopen_set.
Lemma1.5.10
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Associated Lean declarations
-
WLocalSpace.CompactSpace_closedPoints[complete]
Let X be a w-local space. Then the set of closed points X^c of X is
profinite.
Lean code for Lemma1.5.10●1 theorem
Associated Lean declarations
-
WLocalSpace.CompactSpace_closedPoints[complete]
Associated Lean declarations
-
WLocalSpace.CompactSpace_closedPoints[complete]
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/ClosedPoints.leancomplete
theorem WLocalSpace.CompactSpace_closedPoints.{u_1} {X : Type u_1} [TopologicalSpace X] [WLocalSpace X] : CompactSpace ↑(closedPoints X)
theorem WLocalSpace.CompactSpace_closedPoints.{u_1} {X : Type u_1} [TopologicalSpace X] [WLocalSpace X] : CompactSpace ↑(closedPoints X)
Proof for Lemma 1.5.10
It is a closed subspace of a spectral space, hence spectral. Therefore it is profinite by Lemma 1.5.9.
Lemma1.5.11
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Associated Lean declarations
Let X be a spectral space and E \subseteq X a quasi-compact subset. Then
the generalization E^g is an intersection of quasi-compact open subsets.
(Stacks Project, Tag 0A31, (3) ⟹ (4))
Lean code for Lemma1.5.11●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/Topology/Spectral/Basic.leancomplete
theorem generalizationHull.eq_sInter_of_isCompact.{u_1} {X : Type u_1} [TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsCompact s) : ∃ S ⊆ {U | IsOpen U ∧ IsCompact U}, generalizationHull s = ⋂₀ S
theorem generalizationHull.eq_sInter_of_isCompact.{u_1} {X : Type u_1} [TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsCompact s) : ∃ S ⊆ {U | IsOpen U ∧ IsCompact U}, generalizationHull s = ⋂₀ S
Proof for Lemma 1.5.11
uses 0
Let X be a spectral space and let W denote E^g. Since every point of
W specializes to a point of E we see that an open of W which contains
E is equal to W. Hence since E is quasi-compact, so is W. If
x \in X, x \notin W, then Z = \overline{\{x\}} is disjoint from W.
Since W is quasi-compact we can find a quasi-compact open U (since there
is an open basis of quasi-compact opens of X and finitely many of them
suffice to cover W) with W \subset U and U \cap Z = \emptyset. We
conclude that W is an intersection of quasi-compact open subsets.
Definition1.5.12
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 2
Associated Lean declarations
-
constructibleTopology[complete]
Let X be a topological space. The constructible topology on X is the
topology with subbase of opens the sets U and X - U for all quasi-compact
opens U of X.
(Stacks Project, Tag 08YF)
Lean code for Definition1.5.12●1 definition
Associated Lean declarations
-
constructibleTopology[complete]
Associated Lean declarations
-
constructibleTopology[complete]
-
defdefined in Mathlib/Topology/Spectral/ConstructibleTopology.leancomplete
def constructibleTopology.{u_2} (X : Type u_2) [TopologicalSpace X] : TopologicalSpace X
def constructibleTopology.{u_2} (X : Type u_2) [TopologicalSpace X] : TopologicalSpace X
The constructible topology on a topological space `X` has as a subbasis the open and compact sets of `X` and their complements.
In other words, a subset of X is open in the constructible topology if and
only if it is a union of finite intersections of sets of the form U or
X - U for a quasi-compact open U.
Lemma1.5.13
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Associated Lean declarations
-
compactSpace_withConstructibleTopology[complete]
Let X be a spectral space. Then X is quasi-compact in the constructible
topology.
(Stacks Project, Tag 0901)
Lean code for Lemma1.5.13●1 theorem
Associated Lean declarations
-
compactSpace_withConstructibleTopology[complete]
Associated Lean declarations
-
compactSpace_withConstructibleTopology[complete]
-
theoremdefined in Mathlib/Topology/Spectral/ConstructibleTopology.leancomplete
theorem compactSpace_withConstructibleTopology.{u_1} {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [QuasiSober X] [PrespectralSpace X] [QuasiSeparatedSpace X] : CompactSpace (WithConstructibleTopology X)
theorem compactSpace_withConstructibleTopology.{u_1} {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [QuasiSober X] [PrespectralSpace X] [QuasiSeparatedSpace X] : CompactSpace (WithConstructibleTopology X)
If `X` is quasi-separated, quasi-sober, prespectral and quasi-compact, then `X` is still quasi-compact in the constructible topology. This holds in particular for spectral spaces.
Proof for Lemma 1.5.13
uses 0
Let \mathfrak{B} be the set of subsets of X that are quasi-compact open or
the complement of a quasi-compact open. By definition of the constructible
topology and the Alexander subbasis theorem, it suffices to show that every
covering X = \bigcup_{i \in I} B_i with B_i \in \mathfrak{B} has a finite
subcover. Since for every B \in \mathfrak{B} also X - B \in \mathfrak{B},
it suffices to show: If \{B_i\}_{i \in I} is a family of elements of
\mathfrak{B} such that all finite subfamilies have non-empty intersection,
then \bigcap_{i \in I} B_i is non-empty.
Let \mathcal{S} be the set of families in \mathfrak{B} that are pairwise
unequal, have non-empty finite intersections and empty intersection. For the
sake of contradiction, suppose \mathcal{S} is non-empty. If we equip
\mathcal{S} with the ordering by subset inclusion, Zorn's Lemma yields a
maximal family \{B_i\}_{i \in I} \in \mathcal{S}.
Let I' \subseteq I be the indices such that B_i is closed and set
Z = \bigcap_{i \in I'} B_i. This is a closed and non-empty subset of X,
because X is quasi-compact and all finite intersections are non-empty by
assumption. Note that for any i_1, \ldots, i_n \in I the intersection
\bigcap_{a=1}^n B_{i_a} is quasi-compact, hence
Z \cap \bigcap_{a=1}^n B_{i_a} is non-empty by the same argument.
Suppose Z = Z' \cup Z'' is reducible with Z', Z'' \subsetneq Z closed.
Because X is a spectral space, there exist quasi-compact opens
U', U'' \subseteq X with U' \cap Z' non-empty, U'' \cap Z'' non-empty
and U' \cap Z'' = \emptyset = U'' \cap Z'. Then set
B' = X - U' \in \mathfrak{B} and B'' = X - U'' \in \mathfrak{B}. We claim
that \{B_i\}_{i \in I} with B' or B'' added is still in
\mathcal{S}. Suppose this is not the case. Then there exist finitely many
indices i_a and j_b in I such that
B' \cap \bigcap_{a=1}^n B_{i_a} = \emptyset = B'' \cap \bigcap_{b=1}^m B_{j_b}.
By construction, Z \subseteq B' \cup B'', so in particular
Z \cap \bigcap_{a=1}^n B_{i_a} \cap \bigcap_{b=1}^m B_{j_b} = \emptyset,
which is a contradiction. Hence \{B_i\}_{i \in I} is not maximal, also a
contradiction. So Z is irreducible. But for every i \in I - I', the set
B_i is open and hence the non-empty open Z \cap B_i of Z contains the
unique generic point of Z. Hence
\bigcap_{i \in I} B_i = Z \cap \bigcap_{i \in I - I'} B_i is non-empty,
which is again a contradiction.
Lemma1.5.14
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.15
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 2
Associated Lean declarations
Let X be a spectral space and E \subseteq X a subset closed in the
constructible topology.
-
If
x \in \overline{E}, thenxis the specialization of a point inE. -
If
Eis stable under specialization, thenEis closed.
(Stacks Project, Tag 0903)
Lean code for Lemma1.5.14●2 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/SpectralSpace/Constructible.leancomplete
theorem exists_specializes_of_isClosed_constructibleTopology_of_mem_closure.{u_1} {X : Type u_1} [TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsClosed s) {x : X} (hx : x ∈ closure s) : ∃ y ∈ s, y ⤳ x
theorem exists_specializes_of_isClosed_constructibleTopology_of_mem_closure.{u_1} {X : Type u_1} [TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsClosed s) {x : X} (hx : x ∈ closure s) : ∃ y ∈ s, y ⤳ x
If `s` is closed in the constructible topology and `x` is in the closure of `s`, then it is the specialization of a point in `s`.
-
theoremdefined in Proetale/Topology/SpectralSpace/Constructible.leancomplete
theorem IsClosed.of_isClosed_constructibleTopology.{u_1} {X : Type u_1} [TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsClosed s) (h : StableUnderSpecialization s) : IsClosed s
theorem IsClosed.of_isClosed_constructibleTopology.{u_1} {X : Type u_1} [TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsClosed s) (h : StableUnderSpecialization s) : IsClosed s
If `s` is closed in the constructible topology and stable under specialization, it is closed.
Proof for Lemma 1.5.14
It suffices to show the first claim. Let x \in \overline{E} and let
\{U_i\}_{i \in I} be the set of quasi-compact open neighbourhoods of x.
Since X is spectral, these form a neighbourhood basis of x, so
\bigcap_{i \in I} U_i is the set of generalizations of x. It hence
suffices to show that \bigcap_{i \in I} U_i \cap E is non-empty. Indeed, as
X is quasi-separated, any finite intersection of the U_i is another one
and since x \in \overline{E}, the intersection U_i \cap E is non-empty for
all i. Since U_i \cap E is closed in the constructible topology for all
i and X is quasi-compact in the constructible topology by
Lemma 1.5.13, the intersection
\bigcap_{i \in I} U_i \cap E is non-empty.
Lemma1.5.15
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.16
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Statement uses 2
Associated Lean declarations
Let X be a w-local space and Z \subseteq X a closed subset. Then Z^g is
closed.
Lean code for Lemma1.5.15●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/Basic.leancomplete
theorem isClosed_generalizationHull_of_wLocalSpace.{u_1} {X : Type u_1} [TopologicalSpace X] [WLocalSpace X] {s : Set X} (hs : IsClosed s) : IsClosed (generalizationHull s)
theorem isClosed_generalizationHull_of_wLocalSpace.{u_1} {X : Type u_1} [TopologicalSpace X] [WLocalSpace X] {s : Set X} (hs : IsClosed s) : IsClosed (generalizationHull s)
Proof for Lemma 1.5.15
Proof uses 3
Since Z is closed, it is quasi-compact. Hence by
Lemma 1.5.11, we see that Z^g
is closed in the constructible topology as an intersection of quasi-compact
opens. Since Z is stable under specialization, the same holds for Z^g by
Lemma 1.5.5. Thus by
Lemma 1.5.14, the claim follows.
Lemma1.5.16
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.17
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 3
Associated Lean declarations
Let X be a w-local space. Then the composition X^c \to X \to \pi_0(X) is
a homeomorphism, where X^c denotes the closed points of X.
(Stacks Project, Tag 0968)
Lean code for Lemma1.5.16●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/ConnectedComponents.leancomplete
theorem WLocalSpace.isHomeomorph_connectedComponents_closedPoints.{u_1} (X : Type u_1) [TopologicalSpace X] [WLocalSpace X] : IsHomeomorph (ConnectedComponents.mk ∘ Subtype.val)
theorem WLocalSpace.isHomeomorph_connectedComponents_closedPoints.{u_1} (X : Type u_1) [TopologicalSpace X] [WLocalSpace X] : IsHomeomorph (ConnectedComponents.mk ∘ Subtype.val)
If `X` is w-local, the composition `closedPoints X → X → ConnectedComponents X` is a homeomorphism.
Proof for Lemma 1.5.16
Proof uses 5
Since X^c is quasi-compact and \pi_0(X) is Hausdorff by
Lemma 1.1.17, it suffices to show the map is bijective. To show
injectivity let x, y \in X^c be distinct. Since X^c is profinite
(Lemma 1.5.10), there exist open and closed
subsets U_0, V_0 \subseteq X^c such that X^c = U_0 \coprod V_0 by
Lemma 1.5.8. Let U = U_0^g and
V = V_0^g. Because X is w-local, we get X = U \coprod V as sets. By
Lemma 1.5.15, both U and V are
closed and therefore also both open. Hence x and y lie in distinct
connected components of X, so the images in \pi_0(X) are distinct.
Since every connected component is closed, it is quasi-compact and hence contains a closed point. Thus the map is surjective.
Lemma1.5.17
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- Definition 1.6.1
- Definition 1.6.2
- Lemma 1.6.3
- Lemma 1.6.4
- Lemma 1.6.5
- Lemma 1.6.6
- Definition 1.6.7
- Lemma 1.6.8
- Lemma 1.6.9
- Definition 1.6.10
- Lemma 1.6.11
- Lemma 1.6.12
- Lemma 1.6.13
- Definition 1.6.14
- Lemma 1.6.15
- Lemma 1.6.16
- Lemma 1.6.17
- Definition 1.6.18
- Lemma 1.6.19
- Lemma 1.6.20
- Lemma 1.6.21
- Corollary 1.6.22
- Lemma 1.6.23
- Lemma 1.6.24
- Lemma 1.6.25
- Proposition 1.6.26
- Definition 1.6.27
- Lemma 1.6.28
- Lemma 1.6.29
- Definition 1.6.30
- Lemma 1.6.31
- Lemma 1.6.32
- Lemma 1.6.33
- Lemma 1.6.34
- Lemma 1.6.35
- Definition 1.7.1
- Lemma 1.7.2
- Lemma 1.7.3
- Definition 1.7.4
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Statement uses 2
Associated Lean declarations
-
ConnectedComponents.wlocalSpace_of_isPullback[sorry in proof] -
ConnectedComponents.isWLocalMap_of_isPullback[sorry in proof] -
ConnectedComponents.preimage_closedPoints_eq_closedPoints_of_isPullback[sorry in proof]
Let X be a spectral space. Let
\begin{CD} Y @>>> T \\ @VVV @VVV \\ X @>>> \pi_0(X) \end{CD}
be a cartesian diagram in the category of topological spaces with T
profinite. If moreover X is w-local, then Y is w-local, Y \to X is
w-local, and the set of closed points of Y is the inverse image of the set of
closed points of X.
(Stacks Project, Tag 096C, second part)
Lean code for Lemma1.5.17●3 theorems, 3 incomplete
Associated Lean declarations
-
ConnectedComponents.wlocalSpace_of_isPullback[sorry in proof]
-
ConnectedComponents.isWLocalMap_of_isPullback[sorry in proof]
-
ConnectedComponents.preimage_closedPoints_eq_closedPoints_of_isPullback[sorry in proof]
Associated Lean declarations
-
ConnectedComponents.wlocalSpace_of_isPullback[sorry in proof] -
ConnectedComponents.isWLocalMap_of_isPullback[sorry in proof] -
ConnectedComponents.preimage_closedPoints_eq_closedPoints_of_isPullback[sorry in proof]
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/Pullback.leancontains sorry
theorem ConnectedComponents.wlocalSpace_of_isPullback.{u} {X Y T : Type u} [TopologicalSpace X] [WLocalSpace X] [TopologicalSpace Y] [TopologicalSpace T] [CompactSpace T] [T2Space T] [TotallyDisconnectedSpace T] {f : C(Y, X)} {g : C(Y, T)} {i : C(T, ConnectedComponents X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g) (TopCat.ofHom f) (TopCat.ofHom i) (TopCat.ofHom { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ })) : WLocalSpace Y
theorem ConnectedComponents.wlocalSpace_of_isPullback.{u} {X Y T : Type u} [TopologicalSpace X] [WLocalSpace X] [TopologicalSpace Y] [TopologicalSpace T] [CompactSpace T] [T2Space T] [TotallyDisconnectedSpace T] {f : C(Y, X)} {g : C(Y, T)} {i : C(T, ConnectedComponents X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g) (TopCat.ofHom f) (TopCat.ofHom i) (TopCat.ofHom { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ })) : WLocalSpace Y
[Stacks Tag 096C](https://stacks.math.columbia.edu/tag/096C) (second part)
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/Pullback.leancontains sorry
theorem ConnectedComponents.isWLocalMap_of_isPullback.{u} {X Y T : Type u} [TopologicalSpace X] [WLocalSpace X] [TopologicalSpace Y] [TopologicalSpace T] [CompactSpace T] [T2Space T] [TotallyDisconnectedSpace T] {f : C(Y, X)} {g : C(Y, T)} {i : C(T, ConnectedComponents X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g) (TopCat.ofHom f) (TopCat.ofHom i) (TopCat.ofHom { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ })) : IsWLocalMap ⇑f
theorem ConnectedComponents.isWLocalMap_of_isPullback.{u} {X Y T : Type u} [TopologicalSpace X] [WLocalSpace X] [TopologicalSpace Y] [TopologicalSpace T] [CompactSpace T] [T2Space T] [TotallyDisconnectedSpace T] {f : C(Y, X)} {g : C(Y, T)} {i : C(T, ConnectedComponents X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g) (TopCat.ofHom f) (TopCat.ofHom i) (TopCat.ofHom { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ })) : IsWLocalMap ⇑f
[Stacks Tag 096C](https://stacks.math.columbia.edu/tag/096C) (second part)
-
theoremdefined in Proetale/Topology/SpectralSpace/WLocal/Pullback.leancontains sorry
theorem ConnectedComponents.preimage_closedPoints_eq_closedPoints_of_isPullback.{u} {X Y T : Type u} [TopologicalSpace X] [WLocalSpace X] [TopologicalSpace Y] [TopologicalSpace T] [CompactSpace T] [T2Space T] [TotallyDisconnectedSpace T] {f : C(Y, X)} {g : C(Y, T)} {i : C(T, ConnectedComponents X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g) (TopCat.ofHom f) (TopCat.ofHom i) (TopCat.ofHom { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ })) : ⇑f ⁻¹' closedPoints X = closedPoints Y
theorem ConnectedComponents.preimage_closedPoints_eq_closedPoints_of_isPullback.{u} {X Y T : Type u} [TopologicalSpace X] [WLocalSpace X] [TopologicalSpace Y] [TopologicalSpace T] [CompactSpace T] [T2Space T] [TotallyDisconnectedSpace T] {f : C(Y, X)} {g : C(Y, T)} {i : C(T, ConnectedComponents X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g) (TopCat.ofHom f) (TopCat.ofHom i) (TopCat.ofHom { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ })) : ⇑f ⁻¹' closedPoints X = closedPoints Y
[Stacks Tag 096C](https://stacks.math.columbia.edu/tag/096C) (second part)
Proof for Lemma 1.5.17
Proof uses 3
We know that Y is spectral and T = \pi_0(Y) by
Lemma 1.1.26. Assume X is w-local and let
X^c \subset X be its closed points. The inverse image Y^c \subset Y of
X^c maps bijectively onto T, since X^c \to \pi_0(X) is a bijection by
Lemma 1.5.16. (Note that we do not yet know whether
Y^c is the set of closed points of Y.) Moreover, Y^c is quasi-compact
as a closed subset of the spectral space Y. Hence Y^c \to \pi_0(Y) = T is
a homeomorphism by isHomeomorph_iff_continuous_bijective
(Stacks Project, Tag 08YE). It
follows that all points of Y^c are closed in Y: if some y \in Y^c
specialized to a distinct closed point y' (which also falls in Y^c since
Y^c is closed), then both would map to the same point in T, contradicting
the bijectivity of Y^c \to T.
Conversely, if y \in Y is a closed point, then it is closed in its fibre over
T, and its image x \in X is closed in the corresponding (homeomorphic)
fibre of X \to \pi_0(X). Since a point in a w-local space is closed if and
only if it is closed in its connected component (which is closed), we have
x \in X^c, so y \in Y^c. Thus Y^c is exactly the set of closed points
of Y. Moreover, since Y^c \cong T, each connected component contains a
unique closed point, and for each y \in Y^c the set of generalizations of
y is precisely the fibre of Y \to \pi_0(Y) (as any generalization of y
lies in the same connected component with y). The lemma follows.