1.1. Preliminaries
Definition1.1.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)
- 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
- 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 6
Associated Lean declarations
-
ExtremallyDisconnected[complete]
A topological space X is extremally disconnected if the closure of every
open subset is open.
Lean code for Definition1.1.1●1 definition
Associated Lean declarations
-
ExtremallyDisconnected[complete]
Associated Lean declarations
-
ExtremallyDisconnected[complete]
-
classdefined in Mathlib/Topology/ExtremallyDisconnected.leancomplete
class ExtremallyDisconnected.{u} (X : Type u) [TopologicalSpace X] : Prop
class ExtremallyDisconnected.{u} (X : Type u) [TopologicalSpace X] : Prop
An extremally disconnected topological space is a space in which the closure of every open set is open.
Methods
open_closure : ∀ (U : Set X), IsOpen U → IsOpen (closure U)
The closure of every open set is open.
The reason that we are interested in extremally disconnected spaces is the following theorem.
Theorem1.1.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
- 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
- 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
-
CompHaus.toStonean[complete] -
Stonean.instProjectiveCompHausCompHaus[complete]
Let X be a quasi-compact Hausdorff topological space. Then X is extremally
disconnected if and only if it is a projective object in the category of
quasi-compact Hausdorff spaces, i.e., for every continuous surjection
f : Y \to Z of quasi-compact Hausdorff spaces and every continuous map
g : X \to Z, there exists a continuous map h : X \to Y such that
f \circ h = g.
Lean code for Theorem1.1.2●2 declarations
Associated Lean declarations
-
CompHaus.toStonean[complete]
-
Stonean.instProjectiveCompHausCompHaus[complete]
Associated Lean declarations
-
CompHaus.toStonean[complete] -
Stonean.instProjectiveCompHausCompHaus[complete]
-
defdefined in Mathlib/Topology/Category/Stonean/Basic.leancomplete
def CompHaus.toStonean.{u} (X : CompHaus) [CategoryTheory.Projective X] : Stonean
def CompHaus.toStonean.{u} (X : CompHaus) [CategoryTheory.Projective X] : Stonean
`Projective` implies `Stonean`.
-
theoremdefined in Mathlib/Topology/Category/Stonean/Basic.leancomplete
theorem Stonean.instProjectiveCompHausCompHaus.{u_1} (X : Stonean) : CategoryTheory.Projective (Stonean.toCompHaus.obj X)
theorem Stonean.instProjectiveCompHausCompHaus.{u_1} (X : Stonean) : CategoryTheory.Projective (Stonean.toCompHaus.obj X)
Every Stonean space is projective in `CompHaus`
Definition1.1.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
- 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
- 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
-
StoneCech[complete]
Let X be a topological space. The Stone-Čech compactification of X is
the profinite space \beta(X) such that
-
Xis dense in\beta(X); -
every continuous map
f \colon X \to Yto a quasi-compact Hausdorff spaceYextends uniquely to a continuous map\beta(f) \colon \beta(X) \to Y.
We denote the Stone-Čech compactification of X by \beta(X).
Lean code for Definition1.1.3●1 definition
Associated Lean declarations
-
StoneCech[complete]
Associated Lean declarations
-
StoneCech[complete]
-
defdefined in Mathlib/Topology/Compactification/StoneCech.leancomplete
def StoneCech.{u} (α : Type u) [TopologicalSpace α] : Type u
def StoneCech.{u} (α : Type u) [TopologicalSpace α] : Type u
The Stone-Čech compactification of a topological space.
Theorem1.1.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
- 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
- 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
-
StoneCech.projective[complete]
Let X be a topological space. Then the Stone-Čech compactification
\beta(X) is extremally disconnected.
Lean code for Theorem1.1.4●1 theorem
Associated Lean declarations
-
StoneCech.projective[complete]
Associated Lean declarations
-
StoneCech.projective[complete]
-
theoremdefined in Mathlib/Topology/ExtremallyDisconnected.leancomplete
theorem StoneCech.projective.{u} {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : CompactT2.Projective (StoneCech X)
theorem StoneCech.projective.{u} {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : CompactT2.Projective (StoneCech X)
Proposition1.1.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
- 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
- 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
-
CompHaus.presentation[complete] -
CompHaus.presentation.π[complete] -
CompHaus.presentation.epi_π[complete] -
CompHaus.lift[complete]
Let X be a quasi-compact Hausdorff space. There exists a continuous
surjection X' \to X with X' quasi-compact, Hausdorff, and extremally
disconnected. (Stacks Project, Tag 090D)
Lean code for Proposition1.1.5●4 declarations
Associated Lean declarations
-
CompHaus.presentation[complete]
-
CompHaus.presentation.π[complete]
-
CompHaus.presentation.epi_π[complete]
-
CompHaus.lift[complete]
Associated Lean declarations
-
CompHaus.presentation[complete] -
CompHaus.presentation.π[complete] -
CompHaus.presentation.epi_π[complete] -
CompHaus.lift[complete]
-
defdefined in Mathlib/Topology/Category/Stonean/Basic.leancomplete
def CompHaus.presentation.{u_1} (X : CompHaus) : Stonean
def CompHaus.presentation.{u_1} (X : CompHaus) : Stonean
If `X` is compact Hausdorff, `presentation X` is a Stonean space equipped with an epimorphism down to `X` (see `CompHaus.presentation.π` and `CompHaus.presentation.epi_π`). It is a "constructive" witness to the fact that `CompHaus` has enough projectives.
-
defdefined in Mathlib/Topology/Category/Stonean/Basic.leancomplete
def CompHaus.presentation.π.{u_1} (X : CompHaus) : Stonean.toCompHaus.obj X.presentation ⟶ X
def CompHaus.presentation.π.{u_1} (X : CompHaus) : Stonean.toCompHaus.obj X.presentation ⟶ X
The morphism from `presentation X` to `X`.
-
theoremdefined in Mathlib/Topology/Category/Stonean/Basic.leancomplete
theorem CompHaus.presentation.epi_π.{u_1} (X : CompHaus) : CategoryTheory.Epi (CompHaus.presentation.π X)
theorem CompHaus.presentation.epi_π.{u_1} (X : CompHaus) : CategoryTheory.Epi (CompHaus.presentation.π X)
The morphism from `presentation X` to `X` is an epimorphism.
-
defdefined in Mathlib/Topology/Category/Stonean/Basic.leancomplete
def CompHaus.lift.{u_1} {X Y : CompHaus} {Z : Stonean} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [CategoryTheory.Epi f] : Z.compHaus ⟶ X
def CompHaus.lift.{u_1} {X Y : CompHaus} {Z : Stonean} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [CategoryTheory.Epi f] : Z.compHaus ⟶ X
``` X | (f) | \/ Z ---(e)---> Y ``` If `Z` is a Stonean space, `f : X ⟶ Y` an epi in `CompHaus` and `e : Z ⟶ Y` is arbitrary, then `lift e f` is a fixed (but arbitrary) lift of `e` to a morphism `Z ⟶ X`. It exists because `Z` is a projective object in `CompHaus`.
Proof for Proposition 1.1.5
Let Y = X but endowed with the discrete topology. Let X' = \beta(Y),
which is extremally disconnected by
Theorem 1.1.4. The continuous map
Y \to X factors as Y \to X' \to X.
We need the following lemmas about connected components. (Note by Jiedong: This
is WRONG. In general, \pi_0(X) \times \pi_0(Y) is continuous and bijective,
but not necessarily homeomorphic.)
Lemma1.1.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.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
- 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
-
connectedComponent.prod[complete] -
ConnectedComponents.bijective_connectedComponentsLift_prod[complete] -
ConnectedComponents.isHomeomorph_connectedComponentsLift_prod[sorry in proof] -
ConnectedComponents.prodMap[complete]
Let X, Y be topological spaces. Then we have
\pi_0 (X \times Y) \simeq \pi_0(X) \times \pi_0(Y) as topological spaces.
Lean code for Lemma1.1.6●4 declarations, 1 incomplete
Associated Lean declarations
-
connectedComponent.prod[complete]
-
ConnectedComponents.bijective_connectedComponentsLift_prod[complete]
-
ConnectedComponents.isHomeomorph_connectedComponentsLift_prod[sorry in proof]
-
ConnectedComponents.prodMap[complete]
Associated Lean declarations
-
connectedComponent.prod[complete] -
ConnectedComponents.bijective_connectedComponentsLift_prod[complete] -
ConnectedComponents.isHomeomorph_connectedComponentsLift_prod[sorry in proof] -
ConnectedComponents.prodMap[complete]
-
theoremdefined in Proetale/Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
theorem connectedComponent.prod.{u_2, u_3} (S : Type u_2) (T : Type u_3) [TopologicalSpace S] [TopologicalSpace T] (s : S) (t : T) : connectedComponent (s, t) = connectedComponent s ×ˢ connectedComponent t
theorem connectedComponent.prod.{u_2, u_3} (S : Type u_2) (T : Type u_3) [TopologicalSpace S] [TopologicalSpace T] (s : S) (t : T) : connectedComponent (s, t) = connectedComponent s ×ˢ connectedComponent t
-
theoremdefined in Proetale/Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
theorem ConnectedComponents.bijective_connectedComponentsLift_prod.{u_2, u_3} (S : Type u_2) (T : Type u_3) [TopologicalSpace S] [TopologicalSpace T] : Function.Bijective ⋯.connectedComponentsLift
theorem ConnectedComponents.bijective_connectedComponentsLift_prod.{u_2, u_3} (S : Type u_2) (T : Type u_3) [TopologicalSpace S] [TopologicalSpace T] : Function.Bijective ⋯.connectedComponentsLift
-
theoremdefined in Proetale/Mathlib/Topology/Connected/TotallyDisconnected.leancontains sorry
theorem ConnectedComponents.isHomeomorph_connectedComponentsLift_prod.{u_2, u_3} (S : Type u_2) (T : Type u_3) [TopologicalSpace S] [TopologicalSpace T] : IsHomeomorph ⋯.connectedComponentsLift
theorem ConnectedComponents.isHomeomorph_connectedComponentsLift_prod.{u_2, u_3} (S : Type u_2) (T : Type u_3) [TopologicalSpace S] [TopologicalSpace T] : IsHomeomorph ⋯.connectedComponentsLift
-
defdefined in Proetale/Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
def ConnectedComponents.prodMap.{u_2, u_3} {S : Type u_2} {T : Type u_3} [TopologicalSpace S] [TopologicalSpace T] : ConnectedComponents (S × T) ≃ₜ ConnectedComponents S × ConnectedComponents T
def ConnectedComponents.prodMap.{u_2, u_3} {S : Type u_2} {T : Type u_3} [TopologicalSpace S] [TopologicalSpace T] : ConnectedComponents (S × T) ≃ₜ ConnectedComponents S × ConnectedComponents T
Proof for Lemma 1.1.6
uses 0
Let x, y be points of X, Y, respectively. To show the above map is
bijective, it suffices to show that the connected component of (x,y) in
X \times Y is the product of the connected component of x in X and the
connected component of y in Y. We know that the product of connected
subsets is still connected (IsPreconnected.prod). The connected component of
(x, y) cannot be larger because its projections to X and Y are also
connected.
To show that the bijective map is homeomorphic, we notice that the topology on
both sides is generated by the basis of the form
\text{image } U \times \text{image } V.
Lemma1.1.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.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
- 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
-
ConnectedComponents.mkHomeomorph[complete]
Let X be a totally disconnected topological space. Then X \simeq \pi_0(X)
as topological spaces.
Lean code for Lemma1.1.7●1 definition
Associated Lean declarations
-
ConnectedComponents.mkHomeomorph[complete]
Associated Lean declarations
-
ConnectedComponents.mkHomeomorph[complete]
-
defdefined in Proetale/Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
def ConnectedComponents.mkHomeomorph.{u_2} (S : Type u_2) [TopologicalSpace S] [TotallyDisconnectedSpace S] : S ≃ₜ ConnectedComponents S
def ConnectedComponents.mkHomeomorph.{u_2} (S : Type u_2) [TopologicalSpace S] [TotallyDisconnectedSpace S] : S ≃ₜ ConnectedComponents S
Proof for Lemma 1.1.7
uses 0
Use the universal property of connected components.
Lemma1.1.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.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
- 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 = \lim_i X_i be a limit of topological spaces over some index category
I and let s \subseteq X be a subset of X. Denote by s_i the image of
s in X_i. Then \overline{s} = \bigcap_i \pi_i^{-1} (\overline{s_i}),
where \pi_i : X \to X_i is the projection map.
Lean code for Lemma1.1.8●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Preliminaries/Closure.leancomplete
theorem TopCat.closure_eq_iInter_preimage_closure_image.{u, v, w} {I : Type v} [CategoryTheory.Category.{w, v} I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I TopCat} {C : CategoryTheory.Limits.Cone F} (hC : CategoryTheory.Limits.IsLimit C) (s : Set ↑C.pt) : closure s = ⋂ i, ⇑(CategoryTheory.ConcreteCategory.hom (C.π.app i)) ⁻¹' closure (⇑(CategoryTheory.ConcreteCategory.hom (C.π.app i)) '' s)
theorem TopCat.closure_eq_iInter_preimage_closure_image.{u, v, w} {I : Type v} [CategoryTheory.Category.{w, v} I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I TopCat} {C : CategoryTheory.Limits.Cone F} (hC : CategoryTheory.Limits.IsLimit C) (s : Set ↑C.pt) : closure s = ⋂ i, ⇑(CategoryTheory.ConcreteCategory.hom (C.π.app i)) ⁻¹' closure (⇑(CategoryTheory.ConcreteCategory.hom (C.π.app i)) '' s)
Lemma1.1.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.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
- 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
-
image_closure_image_subset_closure_image[complete]
Let X = \lim_i X_i be a limit of topological spaces over some index category
I and let s \subseteq X be a subset of X. Denote by s_i the image of
s in X_i. Then for any morphism f : i \to j in I with transition map
\varphi_{f} : X_i \to X_j, we have
\varphi_{f}(\overline{s_i}) \subseteq \overline{s_j}.
Lean code for Lemma1.1.9●1 theorem
Associated Lean declarations
-
image_closure_image_subset_closure_image[complete]
Associated Lean declarations
-
image_closure_image_subset_closure_image[complete]
-
theoremdefined in Proetale/Topology/Preliminaries/Closure.leancomplete
theorem image_closure_image_subset_closure_image.{u_1, u_2, u_3} {I : Type u_1} [CategoryTheory.Category.{u_2, u_1} I] {F : CategoryTheory.Functor I TopCat} (C : CategoryTheory.Limits.Cone F) (s : Set ↑C.pt) {i j : I} (f : i ⟶ j) : ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) '' closure (⇑(CategoryTheory.ConcreteCategory.hom (C.π.app i)) '' s) ⊆ closure (⇑(CategoryTheory.ConcreteCategory.hom (C.π.app j)) '' s)
theorem image_closure_image_subset_closure_image.{u_1, u_2, u_3} {I : Type u_1} [CategoryTheory.Category.{u_2, u_1} I] {F : CategoryTheory.Functor I TopCat} (C : CategoryTheory.Limits.Cone F) (s : Set ↑C.pt) {i j : I} (f : i ⟶ j) : ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) '' closure (⇑(CategoryTheory.ConcreteCategory.hom (C.π.app i)) '' s) ⊆ closure (⇑(CategoryTheory.ConcreteCategory.hom (C.π.app j)) '' s)
Lemma1.1.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
- 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
- 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
-
Topology.IsEmbedding.specializes_iff[complete]
Let f \colon X \to Y be an embedding of topological spaces. Then f
preserves and reflects specializations, i.e. for a, b \in X, a specializes
to b if and only if f(a) specializes to f(b).
Lean code for Lemma1.1.10●1 theorem
Associated Lean declarations
-
Topology.IsEmbedding.specializes_iff[complete]
Associated Lean declarations
-
Topology.IsEmbedding.specializes_iff[complete]
-
theoremdefined in Proetale/Mathlib/Topology/Inseparable.leancomplete
theorem Topology.IsEmbedding.specializes_iff.{u_2, u_3} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsEmbedding f) {x y : X} : f x ⤳ f y ↔ x ⤳ y
theorem Topology.IsEmbedding.specializes_iff.{u_2, u_3} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsEmbedding f) {x y : X} : f x ⤳ f y ↔ x ⤳ y
Proof for Lemma 1.1.10
uses 0
The only if direction holds for any continuous map. Conversely, if f(a)
specializes to f(b), then
b \in f^{-1}(\overline{\{f(a)\}}) = \overline{\{a\}}.
Definition1.1.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
- 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
- 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 5
Associated Lean declarations
-
generalizationHull[complete]
Let X be a topological space and Z \subseteq X a subset. The set
Z^g = \{ x \in X \mid \exists z \in Z, x \rightsquigarrow z \}
is called the generalization of Z in X.
Lean code for Definition1.1.11●1 definition
Associated Lean declarations
-
generalizationHull[complete]
Associated Lean declarations
-
generalizationHull[complete]
-
defdefined in Proetale/Mathlib/Topology/Inseparable.leancomplete
def generalizationHull.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : Set X
def generalizationHull.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : Set X
The generalization hull of `s` is the smallest set containing `s` that is stable under generalization. It is equal to the set of points specializing to a point in `s`, see `generalizationHull_eq`.
Lemma1.1.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
- 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
- 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 Z \subseteq X be a subset of a topological space. Then Z^g is closed
under generalization.
Lean code for Lemma1.1.12●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/Topology/Inseparable.leancomplete
theorem stableUnderGeneralization_generalizationHull.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : StableUnderGeneralization (generalizationHull s)
theorem stableUnderGeneralization_generalizationHull.{u_1} {X : Type u_1} [TopologicalSpace X] (s : Set X) : StableUnderGeneralization (generalizationHull s)
Proof for Lemma 1.1.12
uses 0
This is immediate from the definition.
The following pure topological lemmas will be used in Lemma 1.7.17 and Lemma 1.5.17.
Definition1.1.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
- 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
- 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
-
Continuous.connectedComponentsLift[complete] -
Continuous.connectedComponentsLift_continuous[complete] -
Continuous.connectedComponentsLift_apply_coe[complete] -
Continuous.connectedComponentsLift_comp_coe[complete]
Let X be a topological space. Let \pi_0(X) be the set of connected
components of X. Let X \to \pi_0(X) be the map which sends x \in X to
the connected component of X passing through x. Endow \pi_0(X) with the
quotient topology. Then any continuous map X \to Y from X to a totally
disconnected space Y factors through \pi_0(X).
(Stacks Project, Tag 08ZL)
Lean code for Definition1.1.13●4 declarations
Associated Lean declarations
-
Continuous.connectedComponentsLift[complete]
-
Continuous.connectedComponentsLift_continuous[complete]
-
Continuous.connectedComponentsLift_apply_coe[complete]
-
Continuous.connectedComponentsLift_comp_coe[complete]
Associated Lean declarations
-
Continuous.connectedComponentsLift[complete] -
Continuous.connectedComponentsLift_continuous[complete] -
Continuous.connectedComponentsLift_apply_coe[complete] -
Continuous.connectedComponentsLift_comp_coe[complete]
-
defdefined in Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
def Continuous.connectedComponentsLift.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : ConnectedComponents α → β
def Continuous.connectedComponentsLift.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : ConnectedComponents α → β
The lift to `connectedComponents α` of a continuous map from `α` to a totally disconnected space
-
theoremdefined in Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
theorem Continuous.connectedComponentsLift_continuous.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : Continuous h.connectedComponentsLift
theorem Continuous.connectedComponentsLift_continuous.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : Continuous h.connectedComponentsLift
-
theoremdefined in Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
theorem Continuous.connectedComponentsLift_apply_coe.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (x : α) : h.connectedComponentsLift (ConnectedComponents.mk x) = f x
theorem Continuous.connectedComponentsLift_apply_coe.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (x : α) : h.connectedComponentsLift (ConnectedComponents.mk x) = f x
-
theoremdefined in Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
theorem Continuous.connectedComponentsLift_comp_coe.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : h.connectedComponentsLift ∘ ConnectedComponents.mk = f
theorem Continuous.connectedComponentsLift_comp_coe.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : h.connectedComponentsLift ∘ ConnectedComponents.mk = f
Lemma1.1.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.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
- 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 topological space. Let \pi_0(X) be the topological space of
connected components of X. Let Y be a totally disconnected space. If every
fiber of X \to Y is connected, then the map \pi_0(X) \to Y is injective.
Lean code for Lemma1.1.14●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
theorem Continuous.connectedComponentsLift_injective.{u_2, u_3} {X : Type u_2} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] [TotallyDisconnectedSpace Y] {f : X → Y} (hf : Continuous f) (h : ∀ (y : Y), IsPreconnected (f ⁻¹' {y})) : Function.Injective hf.connectedComponentsLift
theorem Continuous.connectedComponentsLift_injective.{u_2, u_3} {X : Type u_2} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] [TotallyDisconnectedSpace Y] {f : X → Y} (hf : Continuous f) (h : ∀ (y : Y), IsPreconnected (f ⁻¹' {y})) : Function.Injective hf.connectedComponentsLift
Lemma1.1.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.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
- 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 topological space. Assume X is quasi-compact, quasi-separated
and prespectral. Then for any x \in X the connected component of X
containing x is the intersection of all open and closed subsets of X
containing x.
(Stacks Project, Tag 005F)
Lean code for Lemma1.1.15●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/SpectralSpace/ConnectedComponent.leancomplete
theorem sInter_isClopen_and_mem_eq_connectedComponent.{u} {X : Type u} [TopologicalSpace X] [PrespectralSpace X] [CompactSpace X] [QuasiSeparatedSpace X] {x : X} : ⋂ U, ↑U = connectedComponent x
theorem sInter_isClopen_and_mem_eq_connectedComponent.{u} {X : Type u} [TopologicalSpace X] [PrespectralSpace X] [CompactSpace X] [QuasiSeparatedSpace X] {x : X} : ⋂ U, ↑U = connectedComponent x
[Stacks Tag 005F](https://stacks.math.columbia.edu/tag/005F)
Proof for Lemma 1.1.15
uses 0
Let T be the connected component containing x. Let
S = \bigcap_{\alpha \in A} Z_\alpha be the intersection of all open and
closed subsets Z_\alpha of X containing x. Note that S is closed in
X. Note that any finite intersection of Z_\alpha's is a Z_\alpha.
Because T is connected and x \in T we have T \subset Z_\alpha for every
Z_\alpha, thus T \subset S. It suffices to show that S is connected. If
not, then there exists a disjoint union decomposition S = B \amalg C with
B and C open and closed in S. In particular, B and C are closed
in X, and so quasi-compact by assumption (1). By assumption (2) there exist
quasi-compact opens U, V \subset X with B = S \cap U and C = S \cap V.
Then U \cap V \cap S = \emptyset. Hence
\bigcap_\alpha U \cap V \cap Z_\alpha = \emptyset. By assumption (3) the
intersection U \cap V is quasi-compact. Hence for some \alpha' \in A we
have U \cap V \cap Z_{\alpha'} = \emptyset. Since X - (U \cup V) is
disjoint from S and closed in X hence quasi-compact, we can use the same
argument to see that Z_{\alpha''} \subset U \cup V for some \alpha'' \in A.
Then Z_\alpha = Z_{\alpha'} \cap Z_{\alpha''} is contained in U \cup V and
disjoint from U \cap V. Hence
Z_\alpha = U \cap Z_\alpha \amalg V \cap Z_\alpha is a decomposition into two
open pieces, hence U \cap Z_\alpha and V \cap Z_\alpha are open and closed
in X. Thus, if x \in B say, then we see that S \subset U \cap Z_\alpha
and we conclude that C = \emptyset.
Lemma1.1.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.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
- 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 topological space. Assume X is quasi-compact, quasi-separated
and prespectral. Then for a subset T \subset X the following are equivalent:
-
Tis an intersection of open and closed subsets ofX, and -
Tis closed inXand is a union of connected components ofX.
(Stacks Project, Tag 04PL)
Lean code for Lemma1.1.16●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/SpectralSpace/ConnectedComponent.leancomplete
theorem isClosed_and_iUnion_connectedComponent_eq_iff.{u} {X : Type u} [TopologicalSpace X] [PrespectralSpace X] [CompactSpace X] [QuasiSeparatedSpace X] {T : Set X} : (IsClosed T ∧ ∃ I, ⋃ x ∈ I, connectedComponent x = T) ↔ ∃ J, ⋂ U, ↑↑U = T
theorem isClosed_and_iUnion_connectedComponent_eq_iff.{u} {X : Type u} [TopologicalSpace X] [PrespectralSpace X] [CompactSpace X] [QuasiSeparatedSpace X] {T : Set X} : (IsClosed T ∧ ∃ I, ⋃ x ∈ I, connectedComponent x = T) ↔ ∃ J, ⋂ U, ↑↑U = T
[Stacks Tag 04PL](https://stacks.math.columbia.edu/tag/04PL)
Proof for Lemma 1.1.16
It is clear that (a) implies (b). Assume (b). Let x \in X, x \notin T. Let
x \in C \subset X be the connected component of X containing x. By
Lemma 1.1.15 we see that
C = \bigcap V_\alpha is the intersection of all open and closed subsets
V_\alpha of X which contain C. In particular, any pairwise intersection
V_\alpha \cap V_\beta occurs as a V_\alpha i.e. is still open and closed.
As T is a union of connected components of X we see that
C \cap T = \emptyset. Hence T \cap \bigcap V_\alpha = \emptyset. Since
T is quasi-compact as a closed subset of a quasi-compact space, we deduce
that T \cap V_\alpha = \emptyset for some \alpha. For this \alpha we
see that U_\alpha = X - V_\alpha is an open and closed subset of X which
contains T and not x. The lemma follows.
Lemma1.1.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.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
- 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
-
compactSpace_connectedComponent[complete] -
t2Space_connectedComponent[complete]
Let X be a spectral space. Then \pi_0(X) is a profinite space.
(Stacks Project, Tag 0906)
Lean code for Lemma1.1.17●2 theorems
Associated Lean declarations
-
compactSpace_connectedComponent[complete]
-
t2Space_connectedComponent[complete]
Associated Lean declarations
-
compactSpace_connectedComponent[complete] -
t2Space_connectedComponent[complete]
-
theoremdefined in Proetale/Topology/SpectralSpace/ConnectedComponent.leancomplete
theorem compactSpace_connectedComponent.{u} {X : Type u} [TopologicalSpace X] [CompactSpace X] : CompactSpace (ConnectedComponents X)
theorem compactSpace_connectedComponent.{u} {X : Type u} [TopologicalSpace X] [CompactSpace X] : CompactSpace (ConnectedComponents X)
-
theoremdefined in Proetale/Topology/SpectralSpace/ConnectedComponent.leancomplete
theorem t2Space_connectedComponent.{u} {X : Type u} [TopologicalSpace X] [CompactSpace X] [QuasiSeparatedSpace X] [PrespectralSpace X] : T2Space (ConnectedComponents X)
theorem t2Space_connectedComponent.{u} {X : Type u} [TopologicalSpace X] [CompactSpace X] [QuasiSeparatedSpace X] [PrespectralSpace X] : T2Space (ConnectedComponents X)
[Stacks Tag 0906](https://stacks.math.columbia.edu/tag/0906)
Proof for Lemma 1.1.17
We will show that \pi_0(X) is Hausdorff, quasi-compact, and totally
disconnected. By Lemma 1.1.15,
every connected component of X is the intersection of the open and closed
subsets containing it. Since \pi_0(X) is the image of a quasi-compact space,
it is also quasi-compact. It is totally disconnected by construction. Let
C, D \subset X be distinct connected components of X. Write
C = \bigcap_{\alpha} U_\alpha as the intersection of the open and closed
subsets of X containing C. Any finite intersection of U_\alpha's is
another U_\alpha. Since \bigcap_\alpha U_\alpha \cap D = \emptyset we
conclude that U_\alpha \cap D = \emptyset for some \alpha (connected
components are closed, thus quasi-compact). Since U_\alpha is open and
closed, it is the union of the connected components it contains, i.e.,
U_\alpha is the inverse image of some open and closed subset
V_\alpha \subset \pi_0(X). This proves that the points corresponding to C
and D are contained in disjoint open subsets, i.e., \pi_0(X) is Hausdorff.
Lemma1.1.18
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.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
- 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
-
Topology.IsClosedEmbedding.isOpen_and_isCompact_and_preimage_eq[complete] -
Topology.IsClosedEmbedding.spectralSpace[complete] -
SpectralSpace.of_isClosed[complete]
Let X be a spectral space. Let Y \subset X be a closed subspace. Then Y
is spectral.
Lean code for Lemma1.1.18●3 theorems
Associated Lean declarations
-
Topology.IsClosedEmbedding.isOpen_and_isCompact_and_preimage_eq[complete]
-
Topology.IsClosedEmbedding.spectralSpace[complete]
-
SpectralSpace.of_isClosed[complete]
Associated Lean declarations
-
Topology.IsClosedEmbedding.isOpen_and_isCompact_and_preimage_eq[complete] -
Topology.IsClosedEmbedding.spectralSpace[complete] -
SpectralSpace.of_isClosed[complete]
-
theoremdefined in Proetale/Mathlib/Topology/Spectral/Prespectral.leancomplete
theorem Topology.IsClosedEmbedding.isOpen_and_isCompact_and_preimage_eq.{u_1, u_2} {X : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Z] [PrespectralSpace X] [CompactSpace X] {f : Z → X} (hf : Topology.IsClosedEmbedding f) {V : Set Z} (h₁ : IsOpen V) (h₂ : IsCompact V) : ∃ U, IsOpen U ∧ IsCompact U ∧ f ⁻¹' U = V
theorem Topology.IsClosedEmbedding.isOpen_and_isCompact_and_preimage_eq.{u_1, u_2} {X : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Z] [PrespectralSpace X] [CompactSpace X] {f : Z → X} (hf : Topology.IsClosedEmbedding f) {V : Set Z} (h₁ : IsOpen V) (h₂ : IsCompact V) : ∃ U, IsOpen U ∧ IsCompact U ∧ f ⁻¹' U = V
-
theoremdefined in Proetale/Mathlib/Topology/Spectral/Basic.leancomplete
theorem Topology.IsClosedEmbedding.spectralSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsClosedEmbedding f) [SpectralSpace Y] : SpectralSpace X
theorem Topology.IsClosedEmbedding.spectralSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsClosedEmbedding f) [SpectralSpace Y] : SpectralSpace X
-
theoremdefined in Proetale/Mathlib/Topology/Spectral/Basic.leancomplete
theorem SpectralSpace.of_isClosed.{u_1} (X : Type u_1) [TopologicalSpace X] [SpectralSpace X] {C : Set X} [IsClosed C] : SpectralSpace ↑C
theorem SpectralSpace.of_isClosed.{u_1} (X : Type u_1) [TopologicalSpace X] [SpectralSpace X] {C : Set X} [IsClosed C] : SpectralSpace ↑C
Proof for Lemma 1.1.18
uses 0
The only remaining part in Lean is quasi-separatedness. Suppose that V is
open compact in Y, we show that there exists an open compact U in X
such that V = U \cap Y. We can find U' in X such that V = U' \cap Y.
Write U' = \bigcup_{i \in I} U_i as a union of compact opens, then a finite
subset i \in I_0 of U_i already covers V. Take
U := \bigcup_{i \in I_0} U_i as desired.
For any compact opens V_1, V_2 \subset Y, there exist compact opens
U_1, U_2 \subset X such that V_i = U_i \cap Y. Then
V_1 \cap V_2 = (U_1 \cap U_2) \cap Y is still open compact in Y. Here
U_1 \cap U_2 is quasi-compact since X is quasi-separated.
Lemma1.1.19
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.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
- 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
-
closure_prod_eq[complete] -
Set.singleton_prod_singleton[complete]
Let X and Y be topological spaces. Let (x, y) \in X \times Y be a
point. Then
\overline{\{(x, y)\}} = \overline{\{x\}} \times \overline{\{y\}}.
Lean code for Lemma1.1.19●2 theorems
Associated Lean declarations
-
closure_prod_eq[complete]
-
Set.singleton_prod_singleton[complete]
Associated Lean declarations
-
closure_prod_eq[complete] -
Set.singleton_prod_singleton[complete]
-
theoremdefined in Mathlib/Topology/Constructions/SumProd.leancomplete
theorem closure_prod_eq.{u, v} {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} : closure (s ×ˢ t) = closure s ×ˢ closure t
theorem closure_prod_eq.{u, v} {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} : closure (s ×ˢ t) = closure s ×ˢ closure t
-
theoremdefined in Mathlib/Data/Set/Prod.leancomplete
theorem Set.singleton_prod_singleton.{u_1, u_2} {α : Type u_1} {β : Type u_2} {a : α} {b : β} : {a} ×ˢ {b} = {(a, b)}
theorem Set.singleton_prod_singleton.{u_1, u_2} {α : Type u_1} {β : Type u_2} {a : α} {b : β} : {a} ×ˢ {b} = {(a, b)}
Proof for Lemma 1.1.19
uses 0
It is clear that
\overline{\{(x, y)\}} \subseteq \overline{\{x\}} \times \overline{\{y\}}.
If z \notin \overline{\{(x, y)\}}, there exist opens U \subset X,
V \subset Y such that z \notin U \times V, thus
(x, y) \notin U \times V. Either x \notin U or y \notin V, suppose
x \notin U. Then U \cap \overline{\{x\}} = \emptyset, thus
U \times V \cap \overline{\{x\}} \times \overline{\{y\}} = \emptyset. This
shows that
\overline{\{x\}} \times \overline{\{y\}} \subseteq \overline{\{(x, y)\}}.
Lemma1.1.20
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.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
- 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
-
QuasiSeparatedSpace.prod[complete] -
QuasiSober.prod[complete] -
PrespectralSpace.prod[complete] -
SpectralSpace.prod[complete]
Let X and Y be spectral spaces. Then the product X \times Y is
spectral.
(Stacks Project, Tag 0907)
Lean code for Lemma1.1.20●4 theorems
Associated Lean declarations
-
QuasiSeparatedSpace.prod[complete]
-
QuasiSober.prod[complete]
-
PrespectralSpace.prod[complete]
-
SpectralSpace.prod[complete]
Associated Lean declarations
-
QuasiSeparatedSpace.prod[complete] -
QuasiSober.prod[complete] -
PrespectralSpace.prod[complete] -
SpectralSpace.prod[complete]
-
theoremdefined in Proetale/Mathlib/Topology/QuasiSeparated.leancomplete
theorem QuasiSeparatedSpace.prod.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [QuasiSeparatedSpace α] [PrespectralSpace α] [QuasiSeparatedSpace β] [PrespectralSpace β] : QuasiSeparatedSpace (α × β)
theorem QuasiSeparatedSpace.prod.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [QuasiSeparatedSpace α] [PrespectralSpace α] [QuasiSeparatedSpace β] [PrespectralSpace β] : QuasiSeparatedSpace (α × β)
-
theoremdefined in Proetale/Mathlib/Topology/Sober.leancomplete
theorem QuasiSober.prod.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [QuasiSober X] [QuasiSober Y] : QuasiSober (X × Y)
theorem QuasiSober.prod.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [QuasiSober X] [QuasiSober Y] : QuasiSober (X × Y)
The product of two quasi-sober spaces is quasi-sober.
-
theoremdefined in Proetale/Mathlib/Topology/Spectral/Prespectral.leancomplete
theorem PrespectralSpace.prod.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace X] [PrespectralSpace Y] : PrespectralSpace (X × Y)
theorem PrespectralSpace.prod.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace X] [PrespectralSpace Y] : PrespectralSpace (X × Y)
The product of two prespectral spaces is prespectral.
-
theoremdefined in Proetale/Mathlib/Topology/Spectral/Basic.leancomplete
theorem SpectralSpace.prod.{u_1, u_2} (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [SpectralSpace X] [SpectralSpace Y] : SpectralSpace (X × Y)
theorem SpectralSpace.prod.{u_1, u_2} (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [SpectralSpace X] [SpectralSpace Y] : SpectralSpace (X × Y)
[Stacks Tag 0907](https://stacks.math.columbia.edu/tag/0907)
Proof for Lemma 1.1.20
Let X, Y be spectral spaces. Denote p : X \times Y \to X and
q : X \times Y \to Y the projections. We first show that X \times Y is
sober. Let Z \subset X \times Y be a closed irreducible subset. Then
p(Z) \subset X is irreducible and q(Z) \subset Y is irreducible. Let
x \in X be the generic point of the closure of p(Z) and let y \in Y be
the generic point of the closure of q(Z). If (x, y) \notin Z, then there
exist opens x \in U \subset X, y \in V \subset Y such that
Z \cap (U \times V) = \emptyset. Hence Z is contained in
(X - U) \times Y \cup X \times (Y - V). Since Z is irreducible, we see
that either Z \subset (X - U) \times Y or Z \subset X \times (Y - V). In
the first case p(Z) \subset (X - U) and in the second case
q(Z) \subset (Y - V). Both cases are absurd as x is in the closure of
p(Z) and y is in the closure of q(Z). Thus we conclude that
(x, y) \in Z, which means that (x, y) is the generic point of Z
(Lemma 1.1.19).
A basis of the topology of X \times Y consists of opens of the form
U \times V with U \subset X and V \subset Y quasi-compact open (here we
use that X and Y are spectral). Then U \times V is quasi-compact as the
product of quasi-compact spaces is quasi-compact. Moreover, any quasi-compact
open of X \times Y is a finite union of such quasi-compact rectangles
U \times V. It follows that the intersection of two such is again
quasi-compact (since X and Y are spectral). This concludes the proof.
Lemma1.1.21
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.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
- 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
-
t2Space_iff_diagonal_closed[complete]
Let X be a topological space. Then X is Hausdorff if and only if the
diagonal map \Delta : X \to X \times X is a closed embedding.
(Stacks Project, Tag 08ZE)
Lean code for Lemma1.1.21●1 theorem
Associated Lean declarations
-
t2Space_iff_diagonal_closed[complete]
Associated Lean declarations
-
t2Space_iff_diagonal_closed[complete]
-
theoremdefined in Proetale/Mathlib/Topology/Separation/Hausdorff.leancomplete
theorem t2Space_iff_diagonal_closed.{u_1} {X : Type u_1} [TopologicalSpace X] : T2Space X ↔ IsClosed (Set.range fun x => (x, x))
theorem t2Space_iff_diagonal_closed.{u_1} {X : Type u_1} [TopologicalSpace X] : T2Space X ↔ IsClosed (Set.range fun x => (x, x))
[Stacks Tag 08ZE](https://stacks.math.columbia.edu/tag/08ZE)
Lemma1.1.22
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.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
- 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, Y, and S be topological spaces. Assume that S is Hausdorff.
Let f : X \to S and g : Y \to S be continuous maps. The natural map
X \times_S Y \to X \times Y is a closed embedding.
(Stacks Project, Tag 08ZH)
Lean code for Lemma1.1.22●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.leancomplete
theorem TopCat.isClosedEmbedding_pullback_to_prod.{u} {X Y Z : TopCat} [T2Space ↑Z] (f : X ⟶ Z) (g : Y ⟶ Z) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g)))
theorem TopCat.isClosedEmbedding_pullback_to_prod.{u} {X Y Z : TopCat} [T2Space ↑Z] (f : X ⟶ Z) (g : Y ⟶ Z) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g)))
[Stacks Tag 08ZH](https://stacks.math.columbia.edu/tag/08ZH)
Proof for Lemma 1.1.22
X \times_S Y is the inverse image of the image \Delta(S) of the diagonal
map \Delta : S \to S \times S. It follows from
Lemma 1.1.21 that \Delta(S) is a closed subset.
Lemma1.1.23
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.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
- 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
-
Homeomorph.spectralSpace[complete] -
Homeomorph.t0Space[complete] -
Homeomorph.t2Space[complete] -
Homeomorph.quasiSober[complete] -
Homeomorph.quasiSeparatedSpace[complete] -
Homeomorph.compactSpace[complete] -
Homeomorph.prespectralSpace[complete]
Let X and Y be topological spaces. If X is spectral (resp. T0,
Hausdorff, sober, quasi-separated, quasi-compact, prespectral) and there is a
homeomorphism X \cong Y, then Y is spectral (resp. T0, Hausdorff, sober,
quasi-separated, quasi-compact, prespectral).
Lean code for Lemma1.1.23●7 theorems
Associated Lean declarations
-
Homeomorph.spectralSpace[complete]
-
Homeomorph.t0Space[complete]
-
Homeomorph.t2Space[complete]
-
Homeomorph.quasiSober[complete]
-
Homeomorph.quasiSeparatedSpace[complete]
-
Homeomorph.compactSpace[complete]
-
Homeomorph.prespectralSpace[complete]
Associated Lean declarations
-
Homeomorph.spectralSpace[complete] -
Homeomorph.t0Space[complete] -
Homeomorph.t2Space[complete] -
Homeomorph.quasiSober[complete] -
Homeomorph.quasiSeparatedSpace[complete] -
Homeomorph.compactSpace[complete] -
Homeomorph.prespectralSpace[complete]
-
theoremdefined in Proetale/Mathlib/Topology/Spectral/Basic.leancomplete
theorem Homeomorph.spectralSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SpectralSpace X] (f : X ≃ₜ Y) : SpectralSpace Y
theorem Homeomorph.spectralSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SpectralSpace X] (f : X ≃ₜ Y) : SpectralSpace Y
-
theoremdefined in Mathlib/Topology/Separation/Basic.leancomplete
theorem Homeomorph.t0Space.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] (h : X ≃ₜ Y) : T0Space Y
theorem Homeomorph.t0Space.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] (h : X ≃ₜ Y) : T0Space Y
-
theoremdefined in Mathlib/Topology/Separation/Hausdorff.leancomplete
theorem Homeomorph.t2Space.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) : T2Space Y
theorem Homeomorph.t2Space.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) : T2Space Y
-
theoremdefined in Proetale/Mathlib/Topology/Sober.leancomplete
theorem Homeomorph.quasiSober.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [QuasiSober X] (f : X ≃ₜ Y) : QuasiSober Y
theorem Homeomorph.quasiSober.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [QuasiSober X] (f : X ≃ₜ Y) : QuasiSober Y
-
theoremdefined in Proetale/Mathlib/Topology/QuasiSeparated.leancomplete
theorem Homeomorph.quasiSeparatedSpace.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [QuasiSeparatedSpace α] (f : α ≃ₜ β) : QuasiSeparatedSpace β
theorem Homeomorph.quasiSeparatedSpace.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [QuasiSeparatedSpace α] (f : α ≃ₜ β) : QuasiSeparatedSpace β
Quasi-separatedness transfers along homeomorphisms.
-
theoremdefined in Mathlib/Topology/Homeomorph/Lemmas.leancomplete
theorem Homeomorph.compactSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] (h : X ≃ₜ Y) : CompactSpace Y
theorem Homeomorph.compactSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] (h : X ≃ₜ Y) : CompactSpace Y
-
theoremdefined in Proetale/Mathlib/Topology/Spectral/Prespectral.leancomplete
theorem Homeomorph.prespectralSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace X] (f : X ≃ₜ Y) : PrespectralSpace Y
theorem Homeomorph.prespectralSpace.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace X] (f : X ≃ₜ Y) : PrespectralSpace Y
A prespectral space structure transfers along homeomorphisms.
Lemma1.1.24
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.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
- 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
-
T0Space.pullback[complete] -
PrespectralSpace.pullback[complete] -
SpectralSpace.pullback[complete] -
QuasiSober.pullback[complete] -
CompactSpace.pullback[complete] -
CategoryTheory.IsPullback.t0Space[complete] -
CategoryTheory.IsPullback.quasiSober[complete] -
CategoryTheory.IsPullback.compactSpace[complete] -
CategoryTheory.IsPullback.prespectralSpace[complete] -
CategoryTheory.IsPullback.spectralSpace[complete]
Let X and Y be spectral spaces. Let S be a Hausdorff topological space.
Let f : X \to S and g : Y \to S be continuous maps. Then the fiber product
X \times_S Y is spectral.
Lean code for Lemma1.1.24●10 theorems
Associated Lean declarations
-
T0Space.pullback[complete]
-
PrespectralSpace.pullback[complete]
-
SpectralSpace.pullback[complete]
-
QuasiSober.pullback[complete]
-
CompactSpace.pullback[complete]
-
CategoryTheory.IsPullback.t0Space[complete]
-
CategoryTheory.IsPullback.quasiSober[complete]
-
CategoryTheory.IsPullback.compactSpace[complete]
-
CategoryTheory.IsPullback.prespectralSpace[complete]
-
CategoryTheory.IsPullback.spectralSpace[complete]
Associated Lean declarations
-
T0Space.pullback[complete] -
PrespectralSpace.pullback[complete] -
SpectralSpace.pullback[complete] -
QuasiSober.pullback[complete] -
CompactSpace.pullback[complete] -
CategoryTheory.IsPullback.t0Space[complete] -
CategoryTheory.IsPullback.quasiSober[complete] -
CategoryTheory.IsPullback.compactSpace[complete] -
CategoryTheory.IsPullback.prespectralSpace[complete] -
CategoryTheory.IsPullback.spectralSpace[complete]
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem T0Space.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T0Space X] [T0Space Y] (f : C(X, S)) (g : C(Y, S)) : T0Space ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
theorem T0Space.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T0Space X] [T0Space Y] (f : C(X, S)) (g : C(Y, S)) : T0Space ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem PrespectralSpace.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T2Space S] [PrespectralSpace X] [PrespectralSpace Y] (f : C(X, S)) (g : C(Y, S)) : PrespectralSpace ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
theorem PrespectralSpace.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T2Space S] [PrespectralSpace X] [PrespectralSpace Y] (f : C(X, S)) (g : C(Y, S)) : PrespectralSpace ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem SpectralSpace.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T2Space S] [SpectralSpace X] [SpectralSpace Y] (f : C(X, S)) (g : C(Y, S)) : SpectralSpace ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
theorem SpectralSpace.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T2Space S] [SpectralSpace X] [SpectralSpace Y] (f : C(X, S)) (g : C(Y, S)) : SpectralSpace ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem QuasiSober.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T2Space S] [QuasiSober X] [QuasiSober Y] (f : C(X, S)) (g : C(Y, S)) : QuasiSober ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
theorem QuasiSober.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T2Space S] [QuasiSober X] [QuasiSober Y] (f : C(X, S)) (g : C(Y, S)) : QuasiSober ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem CompactSpace.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T2Space S] [CompactSpace X] [CompactSpace Y] (f : C(X, S)) (g : C(Y, S)) : CompactSpace ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
theorem CompactSpace.pullback.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] [T2Space S] [CompactSpace X] [CompactSpace Y] (f : C(X, S)) (g : C(Y, S)) : CompactSpace ↑(CategoryTheory.Limits.pullback (TopCat.ofHom f) (TopCat.ofHom g))
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem CategoryTheory.IsPullback.t0Space.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T0Space X] [T0Space Y] : T0Space P
theorem CategoryTheory.IsPullback.t0Space.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T0Space X] [T0Space Y] : T0Space P
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem CategoryTheory.IsPullback.quasiSober.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T2Space S] [QuasiSober X] [QuasiSober Y] : QuasiSober P
theorem CategoryTheory.IsPullback.quasiSober.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T2Space S] [QuasiSober X] [QuasiSober Y] : QuasiSober P
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem CategoryTheory.IsPullback.compactSpace.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T2Space S] [CompactSpace X] [CompactSpace Y] : CompactSpace P
theorem CategoryTheory.IsPullback.compactSpace.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T2Space S] [CompactSpace X] [CompactSpace Y] : CompactSpace P
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem CategoryTheory.IsPullback.prespectralSpace.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T2Space S] [PrespectralSpace X] [PrespectralSpace Y] : PrespectralSpace P
theorem CategoryTheory.IsPullback.prespectralSpace.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T2Space S] [PrespectralSpace X] [PrespectralSpace Y] : PrespectralSpace P
-
theoremdefined in Proetale/Topology/Preliminaries/Pullback.leancomplete
theorem CategoryTheory.IsPullback.spectralSpace.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T2Space S] [SpectralSpace X] [SpectralSpace Y] : SpectralSpace P
theorem CategoryTheory.IsPullback.spectralSpace.{u} {X Y S : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace S] {f : C(X, S)} {g : C(Y, S)} {P : Type u} [TopologicalSpace P] {f' : C(P, Y)} {g' : C(P, X)} (pb : CategoryTheory.IsPullback (TopCat.ofHom g') (TopCat.ofHom f') (TopCat.ofHom f) (TopCat.ofHom g)) [T2Space S] [SpectralSpace X] [SpectralSpace Y] : SpectralSpace P
Proof for Lemma 1.1.24
Proof uses 4
Note that X \times_S Y is a closed subspace of X \times Y by
Lemma 1.1.22. (For subspace, see
TopCat.pullbackIsoProdSubtype.) Since X \times Y is spectral
(Lemma 1.1.20) it follows that X \times_S Y is spectral
(Lemma 1.1.18). Note that we also used
Lemma 1.1.23 to translate between categorical
constructions and non-categorical constructions.
Lemma1.1.25
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.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
- 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
-
Prespectral.of_profinite[complete] -
Spectral.of_profinite[complete]
Let X be a profinite space. Then X is spectral.
Lean code for Lemma1.1.25●2 theorems
Associated Lean declarations
-
Prespectral.of_profinite[complete]
-
Spectral.of_profinite[complete]
Associated Lean declarations
-
Prespectral.of_profinite[complete] -
Spectral.of_profinite[complete]
-
theoremdefined in Proetale/Topology/Preliminaries/Profinite.leancomplete
theorem Prespectral.of_profinite.{u_1} {T : Type u_1} [TopologicalSpace T] [T2Space T] [CompactSpace T] [TotallyDisconnectedSpace T] : PrespectralSpace T
theorem Prespectral.of_profinite.{u_1} {T : Type u_1} [TopologicalSpace T] [T2Space T] [CompactSpace T] [TotallyDisconnectedSpace T] : PrespectralSpace T
-
theoremdefined in Proetale/Topology/Preliminaries/Profinite.leancomplete
theorem Spectral.of_profinite.{u_1} {T : Type u_1} [TopologicalSpace T] [T2Space T] [CompactSpace T] [TotallyDisconnectedSpace T] : SpectralSpace T
theorem Spectral.of_profinite.{u_1} {T : Type u_1} [TopologicalSpace T] [T2Space T] [CompactSpace T] [TotallyDisconnectedSpace T] : SpectralSpace T
Proof for Lemma 1.1.25
uses 0
Since R1 implies sober and Hausdorff implies quasi-separated, it only remains to
show that X is prespectral. Write X as an inverse limit of finite discrete
topological spaces. The preimages of singletons in every finite discrete space
are open and closed subsets and form a topological basis for the topology on
X. Thus X is prespectral.
Lemma1.1.26
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.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
- 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. 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. Then Y is spectral and the canonical map \pi_0(Y) \to T defined
in Definition 1.1.13 is an isomorphism.
(Stacks Project, Tag 096C, first part)
Lean code for Lemma1.1.26●3 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/SpectralSpace/ConnectedComponent.leancomplete
theorem ConnectedComponents.spectralSpace_of_isPullback.{u} {X : Type u} [TopologicalSpace X] [SpectralSpace X] {Y T : Type u} [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 := ⋯ })) : SpectralSpace Y
theorem ConnectedComponents.spectralSpace_of_isPullback.{u} {X : Type u} [TopologicalSpace X] [SpectralSpace X] {Y T : Type u} [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 := ⋯ })) : SpectralSpace Y
-
theoremdefined in Proetale/Topology/SpectralSpace/ConnectedComponent.leancomplete
theorem ConnectedComponents.lift_bijective_of_isPullback.{u} {X : Type u} [TopologicalSpace X] {Y T : Type u} [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 := ⋯ })) : Function.Bijective ⋯.connectedComponentsLift
theorem ConnectedComponents.lift_bijective_of_isPullback.{u} {X : Type u} [TopologicalSpace X] {Y T : Type u} [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 := ⋯ })) : Function.Bijective ⋯.connectedComponentsLift
-
theoremdefined in Proetale/Topology/SpectralSpace/ConnectedComponent.leancomplete
theorem ConnectedComponents.isHomeomorph_lift_of_isPullback.{u} {X : Type u} [TopologicalSpace X] [SpectralSpace X] {Y T : Type u} [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 := ⋯ })) : IsHomeomorph ⋯.connectedComponentsLift
theorem ConnectedComponents.isHomeomorph_lift_of_isPullback.{u} {X : Type u} [TopologicalSpace X] [SpectralSpace X] {Y T : Type u} [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 := ⋯ })) : IsHomeomorph ⋯.connectedComponentsLift
[Stacks Tag 096C](https://stacks.math.columbia.edu/tag/096C) (first part)
Proof for Lemma 1.1.26
Proof uses 5
By Lemma 1.1.25, T is spectral. By
Lemma 1.1.17 \pi_0(X) is Hausdorff. By
Lemma 1.1.24, Y is spectral. Let
Y \to \pi_0(Y) \to T be the canonical factorization in
Definition 1.1.13. It is clear that \pi_0(Y) \to T
is surjective. The fibres of Y \to T are homeomorphic to the fibres of
X \to \pi_0(X). Hence these fibres are connected. It follows that
\pi_0(Y) \to T is injective by
Lemma 1.1.14. We conclude that
\pi_0(Y) \to T is a homeomorphism since it is a bijective map from a
quasi-compact space to a Hausdorff space by
isHomeomorph_iff_continuous_bijective.
The following pure algebraic lemma will be used in Lemma 1.6.6.
Lemma1.1.27
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
- 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
- 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 A \to B be a ring map which has going down. Let \p \subset A be a
prime ideal and let \q \subset B be a prime ideal lying over \p. Assume
that there is at most one prime of B above every prime of A. Then the
natural map B_{\p B} \to B_{\q} is an isomorphism.
(Stacks Project, Tag 00EA, (1) + (2)(a))
Lean code for Lemma1.1.27●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/RingTheory/Ideal/GoingDown.leancomplete
theorem Algebra.HasGoingDown.isLocalization_atPrime_of_subsingleton.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingDown R S] (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p] (h : ∀ (p : Ideal R) [p.IsPrime], Subsingleton { q // q.IsPrime ∧ q.LiesOver p }) : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) (Localization.AtPrime q)
theorem Algebra.HasGoingDown.isLocalization_atPrime_of_subsingleton.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingDown R S] (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p] (h : ∀ (p : Ideal R) [p.IsPrime], Subsingleton { q // q.IsPrime ∧ q.LiesOver p }) : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) (Localization.AtPrime q)
Stacks 00EA, (1) + (2)(a): if `R → S` has going down and there is at most one prime of `S` above every prime of `R`, then for every prime `q` of `S` lying over `p`, the natural map `S_{pS} → S_q` is an isomorphism, i.e. `Localization.AtPrime q` is the localization of `S` at the image of `R \ p`.
Proof for Lemma 1.1.27
uses 0
It suffices to show that the elements of B - \q are all invertible in
B_{\p B}. Suppose the contrary, let x \in B - \q be an element not
invertible in B_{\p B}. We can find a prime ideal \q' \subseteq \p B of
B containing x. By going down there exists a prime \q'' \subseteq \q
lying over \p' = A \cap \q'. By the uniqueness of primes lying over \p' we
see that \q' = \q'', which contradicts the fact that x \notin \q.
Definition1.1.28
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.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
- 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
-
Algebra.IsLocalIso[complete] -
RingHom.IsLocalIso[complete]
We say A \to B is a local isomorphism if for every prime
\mathfrak{q} \subset B there exists a g \in B, g \notin \mathfrak{q}
such that A \to B_g induces an open immersion \Spec (B_g) \to \Spec (A).
(Stacks Project, Tag 096E (1))
Lean code for Definition1.1.28●2 definitions
Associated Lean declarations
-
Algebra.IsLocalIso[complete]
-
RingHom.IsLocalIso[complete]
Associated Lean declarations
-
Algebra.IsLocalIso[complete] -
RingHom.IsLocalIso[complete]
-
classdefined in Mathlib/RingTheory/LocalIso.leancomplete
class Algebra.IsLocalIso.{u_1, u_2} (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] : Prop
class Algebra.IsLocalIso.{u_1, u_2} (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] : Prop
An `R`-algebra `S` is a local isomorphism if source locally (in the geometric sense), it is a standard open immersion.
Methods
exists_notMem_isStandardOpenImmersion : ∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, Algebra.IsStandardOpenImmersion R (Localization.Away g)
-
defdefined in Proetale/Algebra/LocalIso.leancomplete
def RingHom.IsLocalIso.{u_3, u_4} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) : Prop
def RingHom.IsLocalIso.{u_3, u_4} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) : Prop
A ring homomorphism is a local isomorphism if source locally (in the geometric sense), it is a standard open immersion.
Definition1.1.29
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
- 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
- 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 11
Associated Lean declarations
-
RingHom.BijectiveOnStalks[complete]
A ring map A \to B identifies local rings if for every prime
\mathfrak{q} \subset B the canonical map
A_{\varphi^{-1}(\mathfrak{q})} \to B_{\mathfrak{q}} is an isomorphism.
(Stacks Project, Tag 096E (2))
Lean code for Definition1.1.29●1 definition
Associated Lean declarations
-
RingHom.BijectiveOnStalks[complete]
Associated Lean declarations
-
RingHom.BijectiveOnStalks[complete]
-
defdefined in Proetale/Algebra/StalkIso.leancomplete
def RingHom.BijectiveOnStalks.{u, v} {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : Prop
def RingHom.BijectiveOnStalks.{u, v} {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : Prop
A ring homomorphism `R →+* S` is bijective on stalks if `R_q →+* S_p` is bijective for every pair of primes `q = f⁻¹(p)`.
Lemma1.1.30
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.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
- 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
-
RingHom.BijectiveOnStalks.pi[complete] -
RingHom.BijectiveOnStalks.prod[complete]
The map A \to \prod_{i = 1}^{n} A_i identifies local rings, if A \to A_i
identifies local rings for all i.
Lean code for Lemma1.1.30●2 theorems
Associated Lean declarations
-
RingHom.BijectiveOnStalks.pi[complete]
-
RingHom.BijectiveOnStalks.prod[complete]
Associated Lean declarations
-
RingHom.BijectiveOnStalks.pi[complete] -
RingHom.BijectiveOnStalks.prod[complete]
-
theoremdefined in Proetale/Algebra/StalkIso.leancomplete
theorem RingHom.BijectiveOnStalks.pi.{u, v, u_1} {R : Type u} [CommRing R] {ι : Type u_1} [Finite ι] {B : ι → Type v} [(i : ι) → CommRing (B i)] {f : (i : ι) → R →+* B i} (hf : ∀ (i : ι), (f i).BijectiveOnStalks) : (Pi.ringHom f).BijectiveOnStalks
theorem RingHom.BijectiveOnStalks.pi.{u, v, u_1} {R : Type u} [CommRing R] {ι : Type u_1} [Finite ι] {B : ι → Type v} [(i : ι) → CommRing (B i)] {f : (i : ι) → R →+* B i} (hf : ∀ (i : ι), (f i).BijectiveOnStalks) : (Pi.ringHom f).BijectiveOnStalks
A finite product of ring homomorphisms that are bijective on stalks is bijective on stalks, provided each factor is bijective on stalks.
-
theoremdefined in Proetale/Algebra/StalkIso.leancomplete
theorem RingHom.BijectiveOnStalks.prod.{u, v} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {T : Type v} [CommRing T] {f : R →+* S} {g : R →+* T} (hf : f.BijectiveOnStalks) (hg : g.BijectiveOnStalks) : (f.prod g).BijectiveOnStalks
theorem RingHom.BijectiveOnStalks.prod.{u, v} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {T : Type v} [CommRing T] {f : R →+* S} {g : R →+* T} (hf : f.BijectiveOnStalks) (hg : g.BijectiveOnStalks) : (f.prod g).BijectiveOnStalks
A binary product of ring homomorphisms that are bijective on stalks is bijective on stalks, provided each factor is bijective on stalks.
Lemma1.1.31
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.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
- 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
-
RingHom.BijectiveOnStalks.comp[complete]
Let A \to B and B \to C be ring maps that identify local rings. Then the
composition A \to C also identifies local rings.
Lean code for Lemma1.1.31●1 theorem
Associated Lean declarations
-
RingHom.BijectiveOnStalks.comp[complete]
Associated Lean declarations
-
RingHom.BijectiveOnStalks.comp[complete]
-
theoremdefined in Proetale/Algebra/StalkIso.leancomplete
theorem RingHom.BijectiveOnStalks.comp.{u, v, u_1} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {T : Type u_1} [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.BijectiveOnStalks) (hg : g.BijectiveOnStalks) : (g.comp f).BijectiveOnStalks
theorem RingHom.BijectiveOnStalks.comp.{u, v, u_1} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {T : Type u_1} [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.BijectiveOnStalks) (hg : g.BijectiveOnStalks) : (g.comp f).BijectiveOnStalks
Lemma1.1.32
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
- 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
- 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
-
Algebra.BijectiveOnStalks.of_comp[complete] -
RingHom.BijectiveOnStalks.of_comp[complete]
Let A be a ring and B \to C be an A-algebra map. Suppose both
A \to B and A \to C are bijective on stalks. Then B \to C is bijective
on stalks.
(Stacks Project, Tag 096D)
Lean code for Lemma1.1.32●2 theorems
Associated Lean declarations
-
Algebra.BijectiveOnStalks.of_comp[complete]
-
RingHom.BijectiveOnStalks.of_comp[complete]
Associated Lean declarations
-
Algebra.BijectiveOnStalks.of_comp[complete] -
RingHom.BijectiveOnStalks.of_comp[complete]
-
theoremdefined in Proetale/Algebra/StalkIso.leancomplete
theorem Algebra.BijectiveOnStalks.of_comp.{u_1, u_2, u_3} (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [Algebra.BijectiveOnStalks R S] [Algebra.BijectiveOnStalks R T] : Algebra.BijectiveOnStalks S T
theorem Algebra.BijectiveOnStalks.of_comp.{u_1, u_2, u_3} (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [Algebra.BijectiveOnStalks R S] [Algebra.BijectiveOnStalks R T] : Algebra.BijectiveOnStalks S T
If `R → S → T` is a tower of `R`-algebras such that `R → S` and `R → T` are both bijective on stalks, then `S → T` is bijective on stalks.
-
theoremdefined in Proetale/Algebra/StalkIso.leancomplete
theorem RingHom.BijectiveOnStalks.of_comp.{u, v, u_1} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {T : Type u_1} [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.BijectiveOnStalks) (hgf : (g.comp f).BijectiveOnStalks) : g.BijectiveOnStalks
theorem RingHom.BijectiveOnStalks.of_comp.{u, v, u_1} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {T : Type u_1} [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.BijectiveOnStalks) (hgf : (g.comp f).BijectiveOnStalks) : g.BijectiveOnStalks
If `f : R →+* S` and the composition `g.comp f : R →+* T` are both bijective on stalks, then `g : S →+* T` is bijective on stalks.
Proof for Lemma 1.1.32
uses 0
Holds because the same holds for bijective maps of sets.
Definition1.1.33
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
- 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
- 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
Lean status
- No associated Lean code or declarations.
Let A be a ring and X = \Spec(A). Let \operatorname{ILR}_A denote the
category of A-algebras B for which A \to B identifies local rings, and
let \operatorname{Top}_X denote the category of topological spaces over X.
Define the functor
F \colon \operatorname{ILR}_A \longrightarrow \operatorname{Top}_X
by sending B to \Spec(B).
(Stacks Project, Tag 096L)
Lemma1.1.34
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
- 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
- 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 A be a ring. Set X = \Spec (A). The functor F constructed in
Definition 1.1.33,
B \longmapsto \Spec (B),
from the category of A-algebras B such that A \to B identifies local
rings to the category of topological spaces over X is fully faithful.
(Stacks Project, Tag 096L)
Proof for Lemma 1.1.34
uses 0
The functor F is a composition of two functors:
-
The fully faithful functor from the category of
A-algebrasBfor whichA \to Bidentifies local rings to the category of ringed spaces(Y, \mathcal{O}_Y)overX = \Spec(A)satisfying\mathcal{O}_Y = p^{-1}\mathcal{O}_X, wherep \colon Y \to Xis the structure map. -
The functor sending a ringed space to its underlying topological space, and a morphism
(f, f^\#)tof.
The second functor is fully faithful because f^\# is always an isomorphism,
being given by the canonical identification
f^{-1}\mathcal{O}_Y \cong f^{-1}p^{-1}\mathcal{O}_X = q^{-1}\mathcal{O}_X \cong \mathcal{O}_Z,
where p \colon Y \to X and q \colon Z \to X are the structure maps.
Definition1.1.35
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
- 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
- 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
Used by 2
Lean status
- No associated Lean code or declarations.
Let A be a ring and X = \Spec(A). Let A \to B and A \to C be two
A-algebras that identify local rings. As a consequence of
Lemma 1.1.34, we have a bijective
map
F : \Hom_{A\text{-alg}}(B, C) \to \Hom_{\mathrm{Top}_X}(\Spec(C), \Spec(B))
sending f : B \to C to the continuous map
\Spec(f) : \Spec(C) \to \Spec(B) induced by f.
Lemma1.1.36
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.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
- 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 R be a commutative semiring, M a finitely generated R-module,
S \subseteq R a submonoid and g \colon M \to M' a localization of M at
S. Then M' is the trivial module if and only if there exists t \in S
such that t \cdot m = 0 for all m \in M.
Lean code for Lemma1.1.36●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/Algebra/Module/LocalizedModule/Finiteness.leancomplete
theorem IsLocalizedModule.subsingleton_iff_exists_mem_smul_eq_zero.{u_1, u_2, u_3} {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] [Module.Finite R M] (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g] : Subsingleton M' ↔ ∃ t ∈ S, ∀ (m : M), t • m = 0
theorem IsLocalizedModule.subsingleton_iff_exists_mem_smul_eq_zero.{u_1, u_2, u_3} {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] [Module.Finite R M] (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g] : Subsingleton M' ↔ ∃ t ∈ S, ∀ (m : M), t • m = 0
For a finitely generated `R`-module `M` and a localization `g : M →ₗ[R] M'` of `M` at a submonoid `S ⊆ R`, `M'` is trivial iff a single element of `S` annihilates all of `M`.
Lemma1.1.37
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
- 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
- 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 A = \colim_i A_i be a filtered colimit of A-algebras and let B be
an étale A-algebra. Then there exists an i and an étale A_i-algebra
B' such that
\begin{CD} A_i @>>> B' \\ @VVV @VVV \\ A @>>> B \end{CD}
is a pushout diagram.
Proof for Lemma 1.1.37
This follows because every étale algebra is of finite presentation and by
possibly enlarging i we can ensure that B' is étale over A_i. The
latter step uses
Lemma 1.1.36 to find a
single index i whose stage trivialises the relevant cotangent / differentials
module.