1.8. w-contractible rings
Definition1.8.1
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.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
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 4
Associated Lean declarations
-
IsWContractibleRing[complete]
A ring A is w-contractible if it is w-strictly local and
\pi_0(\spec{A}) is extremally disconnected.
(Bhatt–Scholze, Definition 2.4.1)
Lean code for Definition1.8.1●1 definition
Associated Lean declarations
-
IsWContractibleRing[complete]
Associated Lean declarations
-
IsWContractibleRing[complete]
-
classdefined in Proetale/Algebra/WContractible.leancomplete
class IsWContractibleRing.{u_1} (R : Type u_1) [CommRing R] : Prop
class IsWContractibleRing.{u_1} (R : Type u_1) [CommRing R] : Prop
A ring `R` is w-contractible if it is w-strictly-local and the space of connected components of `Spec R` is extremally disconnected.
Extends
-
IsWStrictlyLocalRing R
Methods
wLocalSpace_primeSepectrum : WLocalSpace (PrimeSpectrum R)
Inherited from-
IsWStrictlyLocalRing -
IsWLocalRing
isStrictlyHenselianLocalRing_localization : ∀ (m : Ideal R) [inst : m.IsMaximal], IsStrictlyHenselianLocalRing (Localization.AtPrime m)
Inherited from-
IsWStrictlyLocalRing
extremallyDisconnected_connectedComponents : ExtremallyDisconnected (ConnectedComponents (PrimeSpectrum R))
-
We will see that if a ring A is w-contractible, every faithfully flat,
ind-étale map A \to B has a retraction. To show this we will perform a series
of reductions.
Lemma1.8.2
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.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
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Statement uses 3
Associated Lean declarations
Let A be w-contractible and I \subseteq A an ideal cutting out the set
X^c of closed points in X = \spec{A}. Then every faithfully flat
ind-étale map A \to B with B w-local and whose closed points of
\Spec (B) are exactly V(IB) has a retraction.
Lean code for Lemma1.8.2●1 theorem, incomplete
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/WContractible.leancontains sorry
theorem IsWContractibleRing.exists_retraction_of_zeroLocus_map_eq_closedPoints.{u} {R : Type u} [CommRing R] [IsWContractibleRing R] {I : Ideal R} (hI : PrimeSpectrum.zeroLocus ↑I = closedPoints (PrimeSpectrum R)) {S : Type u} [CommRing S] [Algebra R S] [Algebra.IndEtale R S] [Module.FaithfullyFlat R S] [IsWLocalRing S] (hS : PrimeSpectrum.zeroLocus ↑(Ideal.map (algebraMap R S) I) = closedPoints (PrimeSpectrum S)) : ∃ f, f.comp (algebraMap R S) = RingHom.id R
theorem IsWContractibleRing.exists_retraction_of_zeroLocus_map_eq_closedPoints.{u} {R : Type u} [CommRing R] [IsWContractibleRing R] {I : Ideal R} (hI : PrimeSpectrum.zeroLocus ↑I = closedPoints (PrimeSpectrum R)) {S : Type u} [CommRing S] [Algebra R S] [Algebra.IndEtale R S] [Module.FaithfullyFlat R S] [IsWLocalRing S] (hS : PrimeSpectrum.zeroLocus ↑(Ideal.map (algebraMap R S) I) = closedPoints (PrimeSpectrum S)) : ∃ f, f.comp (algebraMap R S) = RingHom.id R
Let `R` be a w-contractible ring and `I` an ideal of `R` cutting out the set `X^c` of closed points in `Spec R`. Then every faithfully flat ind-étale map `R →+* S` with `S` w-local and whose closed points of `Spec S` are exactly `V(IB)` has a retraction.
Proof for Lemma 1.8.2
Proof uses 3
Let A \to B be a faithfully flat ind-étale map with B w-local and such
that the closed points of \Spec(B) are exactly V(IB). In this case,
A \to B identifies local rings. To justify this, it suffices to check the
condition at the maximal ideals of B, which lie over maximal ideals of A
since they map to V(I) = (\Spec(A))^c. Since A is w-strictly local, the
local rings of A at its maximal ideals are strictly Henselian.
Now fix a maximal ideal \mathfrak{n} of B and let
\mathfrak{m} = \mathfrak{n} \cap A be its preimage in A, which is a
maximal ideal. By base change to A_{\mathfrak{m}} and applying
Lemma 1.4.3, we reduce to the case where B is
ind-étale over a strictly Henselian local ring A, with a maximal ideal
\mathfrak{n} lying over the maximal ideal \mathfrak{m} of A. We then
want to show B_{\mathfrak{n}} \cong A. This follows from
Lemma 1.7.2.
Having established that A \to B identifies local rings, we conclude by
Lemma 1.7.24 that it
admits a retraction.
Proposition1.8.3
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- 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
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Statement uses 3
Associated Lean declarations
-
IsWContractibleRing.exists_retraction[complete]
If A is w-contractible, every ind-étale, faithfully flat map A \to B has
a retraction.
(Stacks Project, Tag 0982, (3) ⟹ (2))
Lean code for Proposition1.8.3●1 theorem
Associated Lean declarations
-
IsWContractibleRing.exists_retraction[complete]
Associated Lean declarations
-
IsWContractibleRing.exists_retraction[complete]
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem IsWContractibleRing.exists_retraction.{u} (R : Type u) [CommRing R] [IsWContractibleRing R] (S : Type u) [CommRing S] [Algebra R S] [Algebra.IndEtale R S] [Module.FaithfullyFlat R S] : ∃ f, f.comp (algebraMap R S) = RingHom.id R
theorem IsWContractibleRing.exists_retraction.{u} (R : Type u) [CommRing R] [IsWContractibleRing R] (S : Type u) [CommRing S] [Algebra R S] [Algebra.IndEtale R S] [Module.FaithfullyFlat R S] : ∃ f, f.comp (algebraMap R S) = RingHom.id R
If `R` is w-contractible, every faithfully flat, ind-étale map `R →+* S` has a retraction.
Proof for Proposition 1.8.3
Proof uses 7
With Lemma 1.8.2, it
suffices to reduce to the case that B is furthermore w-local and the closed
points of \Spec (B) are exactly V(IB).
Let A \to B be faithfully flat and ind-étale. We may replace B by the
ring C = B_{w, IB} (see Definition 1.6.30). To justify
this, note that the map A \to C is faithfully flat by
Lemma 1.6.35 and B \to C is
ind-Zariski by Lemma 1.6.32, thus ind-étale
by Lemma 1.4.5. Therefore, by
Lemma 1.4.2, the composition A \to C is also ind-étale.
Hence, we may assume \Spec (B) is w-local such that the set of closed points
of \Spec (B) is V(IB) by parts (2) and (4) of
Lemma 1.6.34.
Lemma1.8.4
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.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
- Theorem 1.8.5
- Corollary 1.8.6
Statement uses 3
Associated Lean declarations
-
exists_isWContractibleRing_of_isWStrictlyLocal[sorry in proof]
If a ring C is w-strictly local, then there exists an ind-Zariski faithfully
flat C-algebra D with D w-contractible.
Lean code for Lemma1.8.4●1 theorem, incomplete
Associated Lean declarations
-
exists_isWContractibleRing_of_isWStrictlyLocal[sorry in proof]
Associated Lean declarations
-
exists_isWContractibleRing_of_isWStrictlyLocal[sorry in proof]
-
theoremdefined in Proetale/Algebra/WContractible.leancontains sorry
theorem exists_isWContractibleRing_of_isWStrictlyLocal.{u} (R : Type u) [CommRing R] [IsWStrictlyLocalRing R] : ∃ S x x_1, Algebra.IndZariski R S ∧ Module.FaithfullyFlat R S ∧ IsWContractibleRing S
theorem exists_isWContractibleRing_of_isWStrictlyLocal.{u} (R : Type u) [CommRing R] [IsWStrictlyLocalRing R] : ∃ S x x_1, Algebra.IndZariski R S ∧ Module.FaithfullyFlat R S ∧ IsWContractibleRing S
Any w-strictly-local ring has an ind-Zariski, faithfully flat cover that is w-contractible.
Proof for Lemma 1.8.4
Proof uses 5
Choose an extremally disconnected space T and a surjective continuous map
T \to \pi_0(\operatorname{Spec}(C)) by
Proposition 1.1.5. (T can be chosen as
\beta((\pi_0(\operatorname{Spec}(C)))^{\mathrm{disc}}).) Note that T is
profinite. By Lemma 1.7.23,
Definition 1.7.22 gives an ind-Zariski ring map C \to D
such that \pi_0(\Spec (D)) \to \pi_0(\Spec (C)) realizes
T \to \pi_0(\Spec (C)) and such that
\begin{CD} \operatorname{Spec}(D) @>>> \pi_0(\operatorname{Spec}(D)) \\ @VVV @VVV \\ \operatorname{Spec}(C) @>>> \pi_0(\operatorname{Spec}(C)) \end{CD}
is cartesian in the category of topological spaces.
Following Lemma 1.5.17, we note that
\Spec (D) is w-local, that \Spec (D) \to \Spec (C) is w-local, and that
the set of closed points of \Spec (D) is the inverse image of the set of
closed points of \Spec (C).
Thus it is still true that the local rings of D at its maximal ideals are
strictly henselian (as they are isomorphic to the local rings at the
corresponding maximal ideals of C by
Lemma 1.2.2). Hence D is
w-contractible.
Theorem1.8.5
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.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
- Corollary 1.8.6
Statement uses 2
Associated Lean declarations
-
exists_isWContractibleRing[complete]
For any ring A, there exists an ind-étale faithfully flat A-algebra D
with D w-contractible.
(Bhatt–Scholze, Theorem 2.4.9; Stacks Project,
Tag 0983)
Lean code for Theorem1.8.5●1 theorem
Associated Lean declarations
-
exists_isWContractibleRing[complete]
Associated Lean declarations
-
exists_isWContractibleRing[complete]
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem exists_isWContractibleRing.{u} (R : Type u) [CommRing R] : ∃ S x x_1, Algebra.IndEtale R S ∧ Module.FaithfullyFlat R S ∧ IsWContractibleRing S
theorem exists_isWContractibleRing.{u} (R : Type u) [CommRing R] : ∃ S x x_1, Algebra.IndEtale R S ∧ Module.FaithfullyFlat R S ∧ IsWContractibleRing S
Any ring has an ind-étale, faithfully flat cover that is w-contractible.
Proof for Theorem 1.8.5
Proof uses 2
This is a combination of Proposition 1.7.15 and Lemma 1.8.4.
Corollary1.8.6
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.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
Associated Lean declarations
-
exists_forall_exists_retraction[complete]
For any ring A, there exists an ind-étale faithfully flat A-algebra B
such that every ind-étale faithfully flat map B \to C has a retraction.
Lean code for Corollary1.8.6●1 theorem
Associated Lean declarations
-
exists_forall_exists_retraction[complete]
Associated Lean declarations
-
exists_forall_exists_retraction[complete]
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem exists_forall_exists_retraction.{u} (R : Type u) [CommRing R] : ∃ S x x_1, Algebra.IndEtale R S ∧ Module.FaithfullyFlat R S ∧ ∀ (T : Type u) [inst : CommRing T] [inst_1 : Algebra S T] [Algebra.IndEtale S T] [Module.FaithfullyFlat S T], ∃ f, f.comp (algebraMap S T) = RingHom.id S
theorem exists_forall_exists_retraction.{u} (R : Type u) [CommRing R] : ∃ S x x_1, Algebra.IndEtale R S ∧ Module.FaithfullyFlat R S ∧ ∀ (T : Type u) [inst : CommRing T] [inst_1 : Algebra S T] [Algebra.IndEtale S T] [Module.FaithfullyFlat S T], ∃ f, f.comp (algebraMap S T) = RingHom.id S
Any ring has an ind-étale, faithfully flat cover for which every ind-étale faithfully flat cover splits.
Proof for Corollary 1.8.6
Proof uses 2
This follows from Theorem 1.8.5 and Proposition 1.8.3.