1.7. w-strictly-local rings
Definition1.7.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
- 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 3
Associated Lean declarations
-
IsWStrictlyLocalRing[complete]
A ring A is w-strictly local if A is w-local, and every local ring of
A at a maximal ideal is strictly henselian.
(Bhatt–Scholze, Definition 2.2.1(ii))
Lean code for Definition1.7.1●1 definition
Associated Lean declarations
-
IsWStrictlyLocalRing[complete]
Associated Lean declarations
-
IsWStrictlyLocalRing[complete]
-
classdefined in Proetale/Algebra/WLocal.leancomplete
class IsWStrictlyLocalRing.{u_3} (R : Type u_3) [CommRing R] : Prop
class IsWStrictlyLocalRing.{u_3} (R : Type u_3) [CommRing R] : Prop
A w-strictly-local ring is a w-local ring whose stalks at maximal ideals are strictly Henselian local rings.
Extends
-
IsWLocalRing R
Methods
wLocalSpace_primeSepectrum : WLocalSpace (PrimeSpectrum R)
Inherited from-
IsWLocalRing
isStrictlyHenselianLocalRing_localization : ∀ (m : Ideal R) [inst : m.IsMaximal], IsStrictlyHenselianLocalRing (Localization.AtPrime m)
-
The goal of this section is to show that every ring A admits a faithfully
flat, ind-étale algebra B that is w-strictly-local.
Lemma1.7.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.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 3
Lean status
- No associated Lean code or declarations.
Let A be a strictly henselian local ring. Let A \to B be an ind-étale
ring map. Let \n be a maximal ideal of B lying over the maximal ideal
\m of A. Then the map A \to B_\n is an isomorphism.
Proof for Lemma 1.7.2
Write B = \colim_i B_i as a filtered colimit of étale A-algebras B_i.
Since localization commutes with colimits, we have
B_\n = \colim_i (B_i)_{\n_i} where \n_i is the restriction of \n to
B_i. Then use Proposition 1.3.6
to conclude each (B_i)_{\n_i} is isomorphic to A.
Lemma1.7.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
- 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 such that every faithfully flat étale ring map A \to B
has a retraction. Then every local ring of A at a maximal ideal is strictly
henselian.
Proof for Lemma 1.7.3
uses 0
Let \mathfrak{m} be a maximal ideal of A, denote by \kappa the residue
field \kappa(\mathfrak{m}) and by \kappa^{\mathrm{sep}} a separable
closure of \kappa. Let
A_{\mathfrak{m}} \to B \to \kappa^{\mathrm{sep}} be a factorisation of
A_{\mathfrak{m}} \to \kappa^{\mathrm{sep}} where A_{\mathfrak{m}} \to B is
étale. Since A_{\mathfrak{m}} = \colim_{f \not\in \mathfrak{m}} A_f, by
Lemma 1.1.37 there exists f \not\in \mathfrak{m} and
an étale A_f-algebra B' such that
B = A_{\mathfrak{m}} \otimes_{A_f} B'. Because A \to A_f \to B' is étale,
there are finitely many prime ideals \mathfrak{q}_1, \ldots, \mathfrak{q}_n
of B' lying over \mathfrak{m}. Since the kernel of the composition
B' \to B \to \kappa^{\mathrm{sep}} lies over \mathfrak{m} (the kernel of
A \to \kappa^{\mathrm{sep}} is \mathfrak{m}), we have n \ge 1. Set
\mathfrak{q} = \mathfrak{q}_1. By prime avoidance, there exists g \in B'
such that g \in \mathfrak{q}_i for all i \ge 2 and
g \not\in \mathfrak{q}. Hence \mathfrak{q} is the unique prime ideal of
B'_g lying over \mathfrak{m}.
Let U be the image of the induced map \spec{B'_g} \to \spec{A}. Since
A \to B' is étale, U is open. Since \{\mathfrak{m}\} is closed in
\spec{A}, there exist a_i such that
\spec{A} - \{\mathfrak{m}\} = \bigcup_{i} D(a_i).
The complement of U is closed and quasicompact, and contained in
\spec{A} - \{\mathfrak{m}\}, hence there exist a_1, \ldots, a_r such that
\spec{A} = U \cup \bigcup_{i=1}^r D(a_i).
Hence the map A \to B'_g \times \prod_{i=1}^{r} A_{a_i} is étale and
faithfully flat. By assumption, it therefore has a retraction \sigma. Since
\mathfrak{q} is the unique prime ideal of
B'_g \times \prod_{i=1}^{r} A_{a_i} lying over \mathfrak{m}, we have
\sigma^{-1}(\mathfrak{m}) = \mathfrak{q}. In particular, we obtain a
retraction
B'_{\mathfrak{q}} = \left(B'_g \times \prod_{i=1}^{r} A_{a_i}\right)_{\mathfrak{q}} \to A_{\mathfrak{m}}
of the map A_{\mathfrak{m}} \to B'_{\mathfrak{q}}. Precomposing with
B' \to B'_{\mathfrak{q}} we obtain a map B' \to A_{\mathfrak{m}} and
hence a map B = B' \otimes_{A_f} A_{\mathfrak{m}} \to A_{\mathfrak{m}} that
is a retraction of A_{\mathfrak{m}} \to B.
Definition1.7.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
- Lemma 1.7.5
- Lemma 1.7.6
- Lemma 1.7.7
- Lemma 1.7.8
- Definition 1.7.9
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 3
Associated Lean declarations
Let A be a ring. Denote by S(A) the set of finite subsets of faithfully
flat étale A-algebras. We call the A-algebra
T(A) = \colim_{E \in S(A)} \bigotimes_{B \in E} B the étale precontraction
of A.
Lean code for Definition1.7.4●1 definition
Associated Lean declarations
Associated Lean declarations
-
defdefined in Proetale/Algebra/Contraction/Covers.leancomplete
def CategoryTheory.MorphismProperty.precontraction.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (X : C) [CategoryTheory.EssentiallySmall.{w, v, max u v} (P.Over ⊤ X)] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [CategoryTheory.Limits.HasLimit (CategoryTheory.FiniteFamilies.diag P X)] : CategoryTheory.Over X
def CategoryTheory.MorphismProperty.precontraction.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (X : C) [CategoryTheory.EssentiallySmall.{w, v, max u v} (P.Over ⊤ X)] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [CategoryTheory.Limits.HasLimit (CategoryTheory.FiniteFamilies.diag P X)] : CategoryTheory.Over X
Lemma1.7.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.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
For every faithfully flat étale ring map A \to B, there exists an
A-algebra map B \to T(A).
Lean code for Lemma1.7.5●1 definition
Associated Lean declarations
Associated Lean declarations
-
defdefined in Proetale/Algebra/Contraction/Covers.leancomplete
def CategoryTheory.MorphismProperty.Precontraction.π.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (X : C) [CategoryTheory.EssentiallySmall.{w, v, max u v} (P.Over ⊤ X)] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [CategoryTheory.Limits.HasLimit (CategoryTheory.FiniteFamilies.diag P X)] {Y : C} (f : Y ⟶ X) (hf : P f) : P.precontraction X ⟶ CategoryTheory.Over.mk f
def CategoryTheory.MorphismProperty.Precontraction.π.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (X : C) [CategoryTheory.EssentiallySmall.{w, v, max u v} (P.Over ⊤ X)] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [CategoryTheory.Limits.HasLimit (CategoryTheory.FiniteFamilies.diag P X)] {Y : C} (f : Y ⟶ X) (hf : P f) : P.precontraction X ⟶ CategoryTheory.Over.mk f
Proof for Lemma 1.7.5
uses 0
\{B\} is an element of S(A), hence B itself is part of the diagram
defining T(A).
Lemma1.7.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.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 ring.
-
The forgetful functors from commutative
R-algebras toR-algebras and fromR-algebras toR-modules preserve filtered colimits. -
The forgetful functor from commutative
R-algebras to commutative rings preserves filtered colimits. -
Tensoring on the left with an
R-algebra preserves colimits on the category of commutativeR-algebras.
Lean code for Lemma1.7.6●4 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/Algebra/Category/CommAlgCat/Limits.leancomplete
theorem CommAlgCat.preservesColimitsOfShape_tensorLeft.{u, u_1, u_2} {R : Type u} [CommRing R] {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.IsFiltered J] (M : CommAlgCat R) : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MonoidalCategory.tensorLeft M)
theorem CommAlgCat.preservesColimitsOfShape_tensorLeft.{u, u_1, u_2} {R : Type u} [CommRing R] {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.IsFiltered J] (M : CommAlgCat R) : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MonoidalCategory.tensorLeft M)
-
theoremdefined in Proetale/Mathlib/Algebra/Category/CommAlgCat/Limits.leancomplete
theorem CommAlgCat.preservesFilteredColimitsOfSize_forget_commRingCat.{u} {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget₂ (CommAlgCat R) CommRingCat)
theorem CommAlgCat.preservesFilteredColimitsOfSize_forget_commRingCat.{u} {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget₂ (CommAlgCat R) CommRingCat)
-
theoremdefined in Proetale/Mathlib/Algebra/Category/CommAlgCat/Limits.leancomplete
theorem CommAlgCat.preservesFilteredColimitsOfSize_forget_algCat.{u} (R : Type u) [CommRing R] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget₂ (CommAlgCat R) (AlgCat R))
theorem CommAlgCat.preservesFilteredColimitsOfSize_forget_algCat.{u} (R : Type u) [CommRing R] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget₂ (CommAlgCat R) (AlgCat R))
-
theoremdefined in Proetale/Mathlib/Algebra/Category/CommAlgCat/Limits.leancomplete
theorem AlgCat.preservesFilteredColimitsOfSize_forget_moduleCat.{u} (R : Type u) [CommRing R] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R))
theorem AlgCat.preservesFilteredColimitsOfSize_forget_moduleCat.{u} (R : Type u) [CommRing R] : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R))
Lemma1.7.7
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.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.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
-
Module.Flat.of_colimitPresentation[complete] -
Module.FaithfullyFlat.of_colimitPresentation[complete] -
Module.Flat.iff_ind_flat[complete] -
Module.FaithfullyFlat.iff_ind_faithfullyFlat[complete] -
RingHom.Flat.iff_ind_flat[complete] -
RingHom.FaithfullyFlat.iff_ind_faithfullyFlat[complete] -
RingHom.Flat.of_isColimit[complete] -
RingHom.FaithfullyFlat.of_isColimit[complete]
Let B = \colim_i B_i be a filtered colimit of (faithfully) flat
A-algebras. Then B is (faithfully) flat over A.
Lean code for Lemma1.7.7●8 theorems
Associated Lean declarations
-
Module.Flat.of_colimitPresentation[complete]
-
Module.FaithfullyFlat.of_colimitPresentation[complete]
-
Module.Flat.iff_ind_flat[complete]
-
Module.FaithfullyFlat.iff_ind_faithfullyFlat[complete]
-
RingHom.Flat.iff_ind_flat[complete]
-
RingHom.FaithfullyFlat.iff_ind_faithfullyFlat[complete]
-
RingHom.Flat.of_isColimit[complete]
-
RingHom.FaithfullyFlat.of_isColimit[complete]
Associated Lean declarations
-
Module.Flat.of_colimitPresentation[complete] -
Module.FaithfullyFlat.of_colimitPresentation[complete] -
Module.Flat.iff_ind_flat[complete] -
Module.FaithfullyFlat.iff_ind_faithfullyFlat[complete] -
RingHom.Flat.iff_ind_flat[complete] -
RingHom.FaithfullyFlat.iff_ind_faithfullyFlat[complete] -
RingHom.Flat.of_isColimit[complete] -
RingHom.FaithfullyFlat.of_isColimit[complete]
-
theoremdefined in Proetale/Algebra/FaithfullyFlat.leancomplete
theorem Module.Flat.of_colimitPresentation.{u} {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u} [CategoryTheory.SmallCategory ι] [CategoryTheory.IsFiltered ι] (P : CategoryTheory.Limits.ColimitPresentation ι (ModuleCat.of R M)) (h : ∀ (i : ι), Module.Flat R ↑(P.diag.obj i)) : Module.Flat R M
theorem Module.Flat.of_colimitPresentation.{u} {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u} [CategoryTheory.SmallCategory ι] [CategoryTheory.IsFiltered ι] (P : CategoryTheory.Limits.ColimitPresentation ι (ModuleCat.of R M)) (h : ∀ (i : ι), Module.Flat R ↑(P.diag.obj i)) : Module.Flat R M
A module is flat if it can be written as a filtered colimit of flat modules.
-
theoremdefined in Proetale/Algebra/FaithfullyFlat.leancomplete
theorem Module.FaithfullyFlat.of_colimitPresentation.{u} {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S] {ι : Type u} [CategoryTheory.SmallCategory ι] [CategoryTheory.IsFiltered ι] (P : CategoryTheory.Limits.ColimitPresentation ι (CommAlgCat.of R S)) (h : ∀ (i : ι), Module.FaithfullyFlat R ↑(P.diag.obj i)) : Module.FaithfullyFlat R S
theorem Module.FaithfullyFlat.of_colimitPresentation.{u} {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S] {ι : Type u} [CategoryTheory.SmallCategory ι] [CategoryTheory.IsFiltered ι] (P : CategoryTheory.Limits.ColimitPresentation ι (CommAlgCat.of R S)) (h : ∀ (i : ι), Module.FaithfullyFlat R ↑(P.diag.obj i)) : Module.FaithfullyFlat R S
-
theoremdefined in Proetale/Algebra/FaithfullyFlat.leancomplete
theorem Module.Flat.iff_ind_flat.{u} {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S] : Module.Flat R S ↔ (CommAlgCat.flat R).ind (CommAlgCat.of R S)
theorem Module.Flat.iff_ind_flat.{u} {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S] : Module.Flat R S ↔ (CommAlgCat.flat R).ind (CommAlgCat.of R S)
Flat is equivalent to ind-flat.
-
theoremdefined in Proetale/Algebra/FaithfullyFlat.leancomplete
theorem Module.FaithfullyFlat.iff_ind_faithfullyFlat.{u} {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S] : Module.FaithfullyFlat R S ↔ (CommAlgCat.faithfullyFlat R).ind (CommAlgCat.of R S)
theorem Module.FaithfullyFlat.iff_ind_faithfullyFlat.{u} {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S] : Module.FaithfullyFlat R S ↔ (CommAlgCat.faithfullyFlat R).ind (CommAlgCat.of R S)
-
theoremdefined in Proetale/Algebra/FaithfullyFlat.leancomplete
theorem RingHom.Flat.iff_ind_flat.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : f.Flat ↔ CommRingCat.flat.ind (CommRingCat.ofHom f)
theorem RingHom.Flat.iff_ind_flat.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : f.Flat ↔ CommRingCat.flat.ind (CommRingCat.ofHom f)
Flat is equivalent to ind-flat.
-
theoremdefined in Proetale/Algebra/FaithfullyFlat.leancomplete
theorem RingHom.FaithfullyFlat.iff_ind_faithfullyFlat.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : f.FaithfullyFlat ↔ CommRingCat.faithfullyFlat.ind (CommRingCat.ofHom f)
theorem RingHom.FaithfullyFlat.iff_ind_faithfullyFlat.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : f.FaithfullyFlat ↔ CommRingCat.faithfullyFlat.ind (CommRingCat.ofHom f)
Faithfully flat is equivalent to ind-(faithfully flat).
-
theoremdefined in Proetale/Algebra/FaithfullyFlat.leancomplete
theorem RingHom.Flat.of_isColimit.{u} {R S : CommRingCat} (f : R ⟶ S) (J : Type u) [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (D : CategoryTheory.Functor J CommRingCat) {t : (CategoryTheory.Functor.const J).obj R ⟶ D} {c : D ⟶ (CategoryTheory.Functor.const J).obj S} (hc : CategoryTheory.Limits.IsColimit { pt := S, ι := c }) (htc : ∀ (i : J), (CommRingCat.Hom.hom (t.app i)).Flat ∧ CategoryTheory.CategoryStruct.comp (t.app i) (c.app i) = f) : (CommRingCat.Hom.hom f).Flat
theorem RingHom.Flat.of_isColimit.{u} {R S : CommRingCat} (f : R ⟶ S) (J : Type u) [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (D : CategoryTheory.Functor J CommRingCat) {t : (CategoryTheory.Functor.const J).obj R ⟶ D} {c : D ⟶ (CategoryTheory.Functor.const J).obj S} (hc : CategoryTheory.Limits.IsColimit { pt := S, ι := c }) (htc : ∀ (i : J), (CommRingCat.Hom.hom (t.app i)).Flat ∧ CategoryTheory.CategoryStruct.comp (t.app i) (c.app i) = f) : (CommRingCat.Hom.hom f).Flat
A ring map is flat if it can be written as a filtered colimit of flat ring maps.
-
theoremdefined in Proetale/Algebra/FaithfullyFlat.leancomplete
theorem RingHom.FaithfullyFlat.of_isColimit.{u} {R S : CommRingCat} (f : R ⟶ S) (J : Type u) [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (D : CategoryTheory.Functor J CommRingCat) {t : (CategoryTheory.Functor.const J).obj R ⟶ D} {c : D ⟶ (CategoryTheory.Functor.const J).obj S} (hc : CategoryTheory.Limits.IsColimit { pt := S, ι := c }) (htc : ∀ (i : J), (CommRingCat.Hom.hom (t.app i)).FaithfullyFlat ∧ CategoryTheory.CategoryStruct.comp (t.app i) (c.app i) = f) : (CommRingCat.Hom.hom f).FaithfullyFlat
theorem RingHom.FaithfullyFlat.of_isColimit.{u} {R S : CommRingCat} (f : R ⟶ S) (J : Type u) [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (D : CategoryTheory.Functor J CommRingCat) {t : (CategoryTheory.Functor.const J).obj R ⟶ D} {c : D ⟶ (CategoryTheory.Functor.const J).obj S} (hc : CategoryTheory.Limits.IsColimit { pt := S, ι := c }) (htc : ∀ (i : J), (CommRingCat.Hom.hom (t.app i)).FaithfullyFlat ∧ CategoryTheory.CategoryStruct.comp (t.app i) (c.app i) = f) : (CommRingCat.Hom.hom f).FaithfullyFlat
A ring hom is faithfully flat if it can be written as a colimit of faithfully flat ring maps.
Proof for Lemma 1.7.7
Because colimits commute with tensor products, ind-flat is flat. One also checks that pro-surjective is surjective, hence the claim.
Lemma1.7.8
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.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
- 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
T(A) is ind-étale and faithfully flat over A.
Lean code for Lemma1.7.8●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/Contraction/Covers.leancomplete
theorem CategoryTheory.MorphismProperty.pro_precontraction_hom.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (X : C) [CategoryTheory.EssentiallySmall.{w, v, max u v} (P.Over ⊤ X)] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [CategoryTheory.Limits.HasLimit (CategoryTheory.FiniteFamilies.diag P X)] [P.IsMultiplicative] [P.IsStableUnderBaseChange] : P.pro (P.precontraction X).hom
theorem CategoryTheory.MorphismProperty.pro_precontraction_hom.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (X : C) [CategoryTheory.EssentiallySmall.{w, v, max u v} (P.Over ⊤ X)] [CategoryTheory.Limits.HasFiniteWidePullbacks C] [CategoryTheory.Limits.HasLimit (CategoryTheory.FiniteFamilies.diag P X)] [P.IsMultiplicative] [P.IsStableUnderBaseChange] : P.pro (P.precontraction X).hom
Proof for Lemma 1.7.8
For every E \in S(A), the A-algebra \bigotimes_{B \in E} B is étale
and faithfully flat. Hence the result follows from the definition of ind-étale
and Lemma 1.7.7.
Definition1.7.9
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.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
- Lemma 1.7.10
- Proposition 1.7.11
- Corollary 1.7.12
- Lemma 1.7.13
- Proposition 1.7.14
- Proposition 1.7.15
- Definition 1.7.16
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 3
Associated Lean declarations
-
IndEtaleContraction[complete]
Let A be a ring. Set T^0(A) = A and for n \in \N set
T^{n+1}(A) = T(T^n(A)). We call the A-algebra
T^{\infty}(A) = \colim_{n \in \N} T^n(A) the étale contraction of A.
Lean code for Definition1.7.9●1 definition
Associated Lean declarations
-
IndEtaleContraction[complete]
Associated Lean declarations
-
IndEtaleContraction[complete]
-
defdefined in Proetale/Algebra/ProEtaleContraction.leancomplete
def IndEtaleContraction.{u} (R : Type u) [CommRing R] : Type u
def IndEtaleContraction.{u} (R : Type u) [CommRing R] : Type u
The étale ind-contraction of a ring. This is defined to be the contraction wrt. to the morphism property of étale ring homomorphisms.
Lemma1.7.10
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.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
- 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
-
faithfullyFlat_indEtaleContraction[complete] -
indEtale_indEtaleContraction[complete]
T^{\infty}(A) is ind-étale and faithfully flat over A.
Lean code for Lemma1.7.10●2 theorems
Associated Lean declarations
-
faithfullyFlat_indEtaleContraction[complete]
-
indEtale_indEtaleContraction[complete]
Associated Lean declarations
-
faithfullyFlat_indEtaleContraction[complete] -
indEtale_indEtaleContraction[complete]
-
theoremdefined in Proetale/Algebra/ProEtaleContraction.leancomplete
theorem faithfullyFlat_indEtaleContraction.{u} {R : Type u} [CommRing R] : Module.FaithfullyFlat R (IndEtaleContraction R)
theorem faithfullyFlat_indEtaleContraction.{u} {R : Type u} [CommRing R] : Module.FaithfullyFlat R (IndEtaleContraction R)
-
theoremdefined in Proetale/Algebra/ProEtaleContraction.leancomplete
theorem indEtale_indEtaleContraction.{u} {R : Type u} [CommRing R] : Algebra.IndEtale R (IndEtaleContraction R)
theorem indEtale_indEtaleContraction.{u} {R : Type u} [CommRing R] : Algebra.IndEtale R (IndEtaleContraction R)
The ind-contraction of `R` is ind-étale over `R`.
Proof for Lemma 1.7.10
Proof uses 3
This follows from Lemma 1.7.8, Lemma 1.7.7 and Lemma 1.4.4.
Proposition1.7.11
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- 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
- 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 T^{\infty}(A) \to B be a faithfully flat and étale ring map. Then it has
a retraction.
(Stacks Project, Tag 097R)
Lean code for Proposition1.7.11●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/ProEtaleContraction.leancomplete
theorem RingHom.Etale.exists_comp_eq_id_indContraction.{u} {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : IndEtaleContraction R →+* S) (hf : f.Etale) (hf' : Function.Surjective (PrimeSpectrum.comap f)) : ∃ g, g.comp f = RingHom.id (IndEtaleContraction R)
theorem RingHom.Etale.exists_comp_eq_id_indContraction.{u} {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : IndEtaleContraction R →+* S) (hf : f.Etale) (hf' : Function.Surjective (PrimeSpectrum.comap f)) : ∃ g, g.comp f = RingHom.id (IndEtaleContraction R)
Any étale ring homomorphism `IndEtaleContraction R →+* S` has a retraction.
Proof for Proposition 1.7.11
Proof uses 2
By Lemma 1.1.37 there exists n \in \N and a faithfully
flat, étale T^n(A)-algebra B' such that
B = T^{\infty}(A) \otimes_{T^n(A)} B'. By
Lemma 1.7.5, there exists a map
B' \to T^{n+1}(A). The identity of T^{\infty}(A) and the composition
B' \to T^{n+1}(A) \to T^{\infty}(A) now induce a retraction
B = T^{\infty}(A) \otimes_{T^n(A)} B' \to T^{\infty}(A).
Corollary1.7.12
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- 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
- 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 \mathfrak{m} be a maximal ideal of T^{\infty}(A). Then
T^{\infty}(A)_{\mathfrak{m}} is strictly Henselian.
Proof for Corollary 1.7.12
Proof uses 2
This follows from Proposition 1.7.11 and Lemma 1.7.3.
Lemma1.7.13
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.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
- 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.IndEtale.isSeparable[complete]
Let k be a field and A an ind-étale, local k-algebra. Then A is a
separable algebraic field extension of k.
Lean code for Lemma1.7.13●1 theorem
Associated Lean declarations
-
Algebra.IndEtale.isSeparable[complete]
Associated Lean declarations
-
Algebra.IndEtale.isSeparable[complete]
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem Algebra.IndEtale.isSeparable.{u} (R : Type u) [CommRing R] (k : Type u) [Field k] [Algebra k R] [Algebra.IndEtale k R] [IsLocalRing R] : Algebra.IsSeparable k R
theorem Algebra.IndEtale.isSeparable.{u} (R : Type u) [CommRing R] (k : Type u) [Field k] [Algebra k R] [Algebra.IndEtale k R] [IsLocalRing R] : Algebra.IsSeparable k R
Proof for Lemma 1.7.13
uses 0
Let A = \colim_i A_i such that A_i is an étale k-algebra for all i.
Let \mathfrak{m} be the maximal ideal of A. Since localization commutes
with colimits, we obtain
A = A_{\mathfrak{m}} = \colim_i (A_i)_{\mathfrak{m}_i} where
\mathfrak{m}_i is the restriction of \mathfrak{m} to A_i. Since A_i
is étale over k, it is a finite product of finite separable extensions of
k, hence (A_i)_{\mathfrak{m}_i} is a finite separable extension of k.
Since a filtered colimit of finite separable extensions is an algebraic
separable extension, we conclude.
Proposition1.7.14
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.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.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 f \colon A \to B be ind-étale. Then f induces separable algebraic
extensions on residue fields.
Lean code for Proposition1.7.14●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem Algebra.IndEtale.isSeparable_residueField.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IndEtale R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [p.IsPrime] [q.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [Localization.AtPrime.IsLiesOverAlgebra p q] : Algebra.IsSeparable p.ResidueField q.ResidueField
theorem Algebra.IndEtale.isSeparable_residueField.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IndEtale R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [p.IsPrime] [q.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [Localization.AtPrime.IsLiesOverAlgebra p q] : Algebra.IsSeparable p.ResidueField q.ResidueField
An ind-étale ring extension `R → S` induces a separable extension `κ(p) → κ(q)` on residue fields, for any pair of primes `q ∈ Spec S` lying over `p ∈ Spec R`.
Proof for Proposition 1.7.14
Let \mathfrak{q} be a prime ideal of B lying over
\mathfrak{p} \subseteq A. Write B = \colim_i B_i as a filtered colimit of
étale A-algebras. Every element s \in B lifts to some s_i \in B_i, and
the composition
\kappa(\mathfrak{p}) \otimes_A B_i \to \kappa(\mathfrak{q})
is an algebra homomorphism from the étale \kappa(\mathfrak{p})-algebra
\kappa(\mathfrak{p}) \otimes_A B_i to the local ring
\kappa(\mathfrak{q}), so by Lemma 1.7.13 the image
of s in \kappa(\mathfrak{q}) is separable over \kappa(\mathfrak{p}). A
general element of \kappa(\mathfrak{q}) is a ratio of two such images, and
separability passes to ratios via the separable closure.
Proposition1.7.15
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.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
- 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.
For any ring A, there exists an ind-étale faithfully flat A-algebra B
with B w-strictly local.
(Stacks Project, Tag 097X)
Proof for Proposition 1.7.15
Proof uses 8
By Lemma 1.6.21, the ring A_w is w-local,
so the set of closed points of \spec{A_w} is closed. Let I be the radical
ideal of A_w such that V(I) is the set of closed points of
\spec{A_w}. Set B' = T^{\infty}(A_w). By
Corollary 1.7.12, the local ring
B'_{\mathfrak{m}} is strictly henselian for every maximal ideal
\mathfrak{m} of B'. The map A_w \to B' induces algebraic extensions on
residue fields at primes by Lemma 1.7.10 and
Proposition 1.7.14, so applying
Definition 1.6.30 and
Lemma 1.6.34 to A_w \to B', we obtain an
ind-Zariski ring map B' \to B such that B'/IB' \to B/IB is an
isomorphism, V(IB) is the set of closed points of \spec{B}, B is
w-local and A_w \to B' \to B is faithfully flat by
Lemma 1.6.35. Since ind-Zariski
maps identify local rings by
Lemma 1.2.2 and every closed point of
\spec{B} maps to a closed point of \spec{B'}, the local rings at maximal
ideals of B are strictly Henselian. Hence B is w-strictly local.
It remains to verify that the composition A \to A_w \to B' \to B is
ind-étale and faithfully flat. This follows because both ind-étale and
faithfully flat are stable under composition.
By following all constructions, we may choose B as
((T^{\infty}(A_w))_w)_{\widetilde{V(I ((T^{\infty}(A_w))_w))}} where I is
the radical ideal of A_w defining the closed points of \spec{A_w}.
One may ask why T^\infty(A)_w does not work. The reason for this is that the
map \spec{T^{\infty}(A)_w} \to \spec{T^{\infty}(A)} does not necessarily map
closed points to closed points. If A is already w-local, we can eliminate the
points mapping to non-closed points by taking I to be the ideal defining the
closed points of \spec{A}. Then V(I T^{\infty}(A)) only contains closed
points and by passing to the generalization of the preimage of
V(I T^{\infty}(A)) in \spec{T^{\infty}(A)_w}, we obtain the desired affine
scheme. If A is not w-local, we may replace A by A_w in this process
and obtain the result.
Definition1.7.16
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.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
- Lemma 1.7.17
- Definition 1.7.18
- Lemma 1.7.19
- Definition 1.7.20
- Lemma 1.7.21
- Definition 1.7.22
- Lemma 1.7.23
- Lemma 1.7.24
- Definition 1.8.1
- Lemma 1.8.2
- Proposition 1.8.3
- Lemma 1.8.4
- Theorem 1.8.5
- Corollary 1.8.6
Used by 3
Associated Lean declarations
-
WContractification.RestrictClopen.map[complete] -
WContractification.Restriction.diag[complete] -
WContractification.Restriction[complete]
Let A be a ring, X = \Spec(A), and T \subset \pi_0(X). Define the ring
A_T by
A_T := \colim_{W} A_W,
where W runs over all open and closed subsets of X containing the inverse
image Z of T, and A \to A_W is the localization of A at W.
(Stacks Project, Tag 097C)
Lean code for Definition1.7.16●3 definitions
Associated Lean declarations
-
WContractification.RestrictClopen.map[complete]
-
WContractification.Restriction.diag[complete]
-
WContractification.Restriction[complete]
Associated Lean declarations
-
WContractification.RestrictClopen.map[complete] -
WContractification.Restriction.diag[complete] -
WContractification.Restriction[complete]
-
defdefined in Proetale/Algebra/WContractible.leancomplete
def WContractification.RestrictClopen.map.{u} {A : Type u} [CommRing A] {W₁ W₂ : TopologicalSpace.Clopens (PrimeSpectrum A)} (h : W₁ ≤ W₂) : WContractification.RestrictClopen W₂ →ₐ[A] WContractification.RestrictClopen W₁
def WContractification.RestrictClopen.map.{u} {A : Type u} [CommRing A] {W₁ W₂ : TopologicalSpace.Clopens (PrimeSpectrum A)} (h : W₁ ≤ W₂) : WContractification.RestrictClopen W₂ →ₐ[A] WContractification.RestrictClopen W₁
-
defdefined in Proetale/Algebra/WContractible.leancomplete
def WContractification.Restriction.diag.{u} {A : Type u} [CommRing A] (T : Set (ConnectedComponents (PrimeSpectrum A))) : CategoryTheory.Functor { W // ConnectedComponents.mk ⁻¹' T ≤ ↑W }ᵒᵖ (CommAlgCat A)
def WContractification.Restriction.diag.{u} {A : Type u} [CommRing A] (T : Set (ConnectedComponents (PrimeSpectrum A))) : CategoryTheory.Functor { W // ConnectedComponents.mk ⁻¹' T ≤ ↑W }ᵒᵖ (CommAlgCat A)
-
defdefined in Proetale/Algebra/WContractible.leancomplete
def WContractification.Restriction.{u} {A : Type u} [CommRing A] (T : Set (ConnectedComponents (PrimeSpectrum A))) : Type u
def WContractification.Restriction.{u} {A : Type u} [CommRing A] (T : Set (ConnectedComponents (PrimeSpectrum A))) : Type u
Lemma1.7.17
Group: Topological and ring-theoretic preliminaries on w-local spaces and w-local, w-strictly local and w-contractible rings, following Section 2 of Bhatt–Scholze and the Stacks Project. (136)
- Definition 1.1.1
- Theorem 1.1.2
- Definition 1.1.3
- Theorem 1.1.4
- Proposition 1.1.5
- Lemma 1.1.6
- Lemma 1.1.7
- Lemma 1.1.8
- Lemma 1.1.9
- Lemma 1.1.10
- Definition 1.1.11
- Lemma 1.1.12
- Definition 1.1.13
- Lemma 1.1.14
- Lemma 1.1.15
- Lemma 1.1.16
- Lemma 1.1.17
- Lemma 1.1.18
- Lemma 1.1.19
- Lemma 1.1.20
- Lemma 1.1.21
- Lemma 1.1.22
- Lemma 1.1.23
- Lemma 1.1.24
- Lemma 1.1.25
- Lemma 1.1.26
- Lemma 1.1.27
- Definition 1.1.28
- Definition 1.1.29
- Lemma 1.1.30
- Lemma 1.1.31
- Lemma 1.1.32
- Definition 1.1.33
- Lemma 1.1.34
- Definition 1.1.35
- Lemma 1.1.36
- Lemma 1.1.37
- Definition 1.2.1
- Lemma 1.2.2
- Lemma 1.2.3
- Lemma 1.2.4
- Lemma 1.2.5
- Lemma 1.2.6
- Lemma 1.2.7
- Definition 1.3.1
- Lemma 1.3.2
- Definition 1.3.3
- Lemma 1.3.4
- Proposition 1.3.5
- Proposition 1.3.6
- Definition 1.4.1
- Lemma 1.4.2
- Lemma 1.4.3
- Lemma 1.4.4
- Lemma 1.4.5
- Definition 1.5.1
- Definition 1.5.2
- Definition 1.5.3
- Lemma 1.5.4
- Lemma 1.5.5
- Lemma 1.5.6
- Lemma 1.5.7
- Lemma 1.5.8
- Lemma 1.5.9
- Lemma 1.5.10
- Lemma 1.5.11
- Definition 1.5.12
- Lemma 1.5.13
- Lemma 1.5.14
- Lemma 1.5.15
- Lemma 1.5.16
- 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
- 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
Associated Lean declarations
Let A be a ring, X = \Spec(A), and T \subset \pi_0(X) a closed subset.
Then the map A \to A_T from
Definition 1.7.16 is a surjective ind-Zariski
ring map, and the induced morphism \Spec(A_T) \to \Spec(A) restricts to a
homeomorphism of \Spec(A_T) onto the inverse image of T in X.
(Stacks Project, Tag 097C)
Lean code for Lemma1.7.17●4 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem WContractification.Restriction.indZariski.{u} {A : Type u} [CommRing A] (T : Set (ConnectedComponents (PrimeSpectrum A))) : Algebra.IndZariski A (WContractification.Restriction T)
theorem WContractification.Restriction.indZariski.{u} {A : Type u} [CommRing A] (T : Set (ConnectedComponents (PrimeSpectrum A))) : Algebra.IndZariski A (WContractification.Restriction T)
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem WContractification.Restriction.algebraMap_surjective.{u} {A : Type u} [CommRing A] (T : Set (ConnectedComponents (PrimeSpectrum A))) : Function.Surjective ⇑(algebraMap A (WContractification.Restriction T))
theorem WContractification.Restriction.algebraMap_surjective.{u} {A : Type u} [CommRing A] (T : Set (ConnectedComponents (PrimeSpectrum A))) : Function.Surjective ⇑(algebraMap A (WContractification.Restriction T))
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem WContractification.Restriction.range_algebraMap_specComap.{u} {A : Type u} [CommRing A] {T : Set (ConnectedComponents (PrimeSpectrum A))} (h : IsClosed T) : Set.range (PrimeSpectrum.comap (algebraMap A (WContractification.Restriction T))) = ConnectedComponents.mk ⁻¹' T
theorem WContractification.Restriction.range_algebraMap_specComap.{u} {A : Type u} [CommRing A] {T : Set (ConnectedComponents (PrimeSpectrum A))} (h : IsClosed T) : Set.range (PrimeSpectrum.comap (algebraMap A (WContractification.Restriction T))) = ConnectedComponents.mk ⁻¹' T
The image of `Spec(Restriction T) → Spec A` is the preimage of `T` under the projection `Spec A → π₀(Spec A)`, whenever `T` is closed.
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem WContractification.Restriction.isClosedEmbedding_algebraMap_specComap.{u} {A : Type u} [CommRing A] {T : Set (ConnectedComponents (PrimeSpectrum A))} : Topology.IsClosedEmbedding (PrimeSpectrum.comap (algebraMap A (WContractification.Restriction T)))
theorem WContractification.Restriction.isClosedEmbedding_algebraMap_specComap.{u} {A : Type u} [CommRing A] {T : Set (ConnectedComponents (PrimeSpectrum A))} : Topology.IsClosedEmbedding (PrimeSpectrum.comap (algebraMap A (WContractification.Restriction T)))
The map `Spec(Restriction T) → Spec A` is a closed embedding.
Proof for Lemma 1.7.17
Each A \to A_W is a localization at an idempotent. Passing to filtered
colimits, A \to A_T is surjective and ind-Zariski.
When T is closed, its inverse image Z is a closed union of connected
components. By Lemma 1.1.16, we have
Z = \bigcap_{Z \subseteq W,\ W \text{ open and closed}} W.
Thus, \Spec(A_T) = \varprojlim_W W is homeomorphic to Z via the natural
map.
In the following series of constructions, we will modify the connected components of a spectrum to match a given profinite space as in (Stacks Project, Tag 097D).
Definition1.7.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.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
- 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 3
Used by 3
Associated Lean declarations
-
WContractification.Pullback[complete]
Let A be a ring and let X = \Spec (A). Let T be a profinite space and
let f : T \to \pi_0(X) be a continuous map. Let S be a finite discrete
quotient of T with quotient map q : T \to S. Define the ring A^f_{q} as
follows: let Z = \operatorname{Im} (T \to \pi_0(X) \times S = \pi_0(\Spec (A^{S}))),
where A^{S} = \prod_{s \in S} A, and let
A^f_{q} := (A^{S})_{Z}
be the A^S-algebra as in Definition 1.7.16.
Lean code for Definition1.7.18●1 definition
Associated Lean declarations
-
WContractification.Pullback[complete]
Associated Lean declarations
-
WContractification.Pullback[complete]
-
defdefined in Proetale/Algebra/WContractible.leancomplete
def WContractification.Pullback.{u, u_1} {A : Type u} [CommRing A] {T : Type u_1} [TopologicalSpace T] [CompactSpace T] (S : DiscreteQuotient T) (f : C(T, ConnectedComponents (PrimeSpectrum A))) : Type (max u u_1)
def WContractification.Pullback.{u, u_1} {A : Type u} [CommRing A] {T : Type u_1} [TopologicalSpace T] [CompactSpace T] (S : DiscreteQuotient T) (f : C(T, ConnectedComponents (PrimeSpectrum A))) : Type (max u u_1)
Lemma1.7.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.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
- 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 3
Used by 2
Associated Lean declarations
Let A be a ring and let X = \Spec (A). Let T be a profinite space and
let f : T \to \pi_0(X) be a continuous map. Let S be a finite discrete
quotient of T with quotient map q : T \to S. Then the A^S-algebra
defined in Definition 1.7.18 viewed as A-algebra through
A \to A^S \to A^f_{q} is ind-Zariski. In particular, it identifies local
rings. The map A^S \to A^f_{q} induces a homeomorphism of
\Spec (A^f_{q}) onto
(X \times S) \times_{\pi_0(X) \times S} Z = X \times_{\pi_0(X)} Z.
Lean code for Lemma1.7.19●2 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem WContractification.Pullback.indZariski.{u} {A : Type u} [CommRing A] {T : Type u} [TopologicalSpace T] [CompactSpace T] (S : DiscreteQuotient T) (f : C(T, ConnectedComponents (PrimeSpectrum A))) : Algebra.IndZariski A (WContractification.Pullback S f)
theorem WContractification.Pullback.indZariski.{u} {A : Type u} [CommRing A] {T : Type u} [TopologicalSpace T] [CompactSpace T] (S : DiscreteQuotient T) (f : C(T, ConnectedComponents (PrimeSpectrum A))) : Algebra.IndZariski A (WContractification.Pullback S f)
-
theoremdefined in Proetale/Algebra/WContractible.leancomplete
theorem WContractification.Pullback.bijectiveOnStalks_algebraMap.{u} {A : Type u} [CommRing A] {T : Type u} [TopologicalSpace T] [CompactSpace T] (S : DiscreteQuotient T) (f : C(T, ConnectedComponents (PrimeSpectrum A))) : (algebraMap A (WContractification.Pullback S f)).BijectiveOnStalks
theorem WContractification.Pullback.bijectiveOnStalks_algebraMap.{u} {A : Type u} [CommRing A] {T : Type u} [TopologicalSpace T] [CompactSpace T] (S : DiscreteQuotient T) (f : C(T, ConnectedComponents (PrimeSpectrum A))) : (algebraMap A (WContractification.Pullback S f)).BijectiveOnStalks
Proof for Lemma 1.7.19
Proof uses 4
The map A \to A^S is ind-Zariski by
Lemma 1.2.5 and A^S \to A^f_{q} is also
ind-Zariski by
Lemma 1.7.17. The
composition A \to A^f_{q} is therefore ind-Zariski as well by
Lemma 1.2.6. By
Lemma 1.2.2, A \to A^f_{q} identifies
local rings. The last sentence is a direct consequence of
Lemma 1.7.17.
Definition1.7.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.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
- 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 3
Used by 2
Lean status
- No associated Lean code or declarations.
Let A be a ring and let X = \Spec (A). Let T be a profinite space and
let f : T \to \pi_0(X) be a continuous map. Let S and S' be finite
discrete spaces and let q : T \to S and q' : T \to S' be quotient maps.
Let g : S' \to S be a map such that q = g \circ q'. Let
Z \subseteq \pi_0(\Spec (A^{S})) \times S and
Z' \subseteq \pi_0(\Spec (A^{S'})) \times S' be the images of T under the
maps induced by q and q' respectively. Then g induces a map
Z' \to Z and a map
\tilde{g} : \Spec (A^{f}_{q'}) \cong X \times_{\pi_0(X)} Z' \to X \times_{\pi_0(X)} Z \cong \Spec (A^{f}_{q}).
Since both maps A \to A^f_{q} and A \to A^{f}_{q'} identify local rings,
by the bijection in Definition 1.1.35 we
can find a transition ring map
t_{g}: A^f_{q} \to A^{f}_{q'}
that induces the topological map \tilde{g} between the spectra.
Lemma1.7.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.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
- 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 and let X = \Spec (A). Let T be a profinite space and
let f : T \to \pi_0(X) be a continuous map. Let S, S' and S'' be
finite discrete spaces and let q : T \to S, q' : T \to S' and
q'' : T \to S'' be quotient maps. Let g : S' \to S and g' : S'' \to S'
be maps such that q = g \circ q' and q' = g' \circ q''. Then the
transition maps defined in Definition 1.7.20 satisfy
t_{g'} \circ t_{g} = t_{g \circ g'}.
Proof for Lemma 1.7.21
Proof uses 2
Both maps t_{g'} \circ t_{g} and t_{g \circ g'} induce the same
topological map between the spectra by construction. Since all maps involved
identify local rings by Lemma 1.7.19, by fully
faithfulness in Definition 1.1.35 we
conclude that they are equal.
Definition1.7.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.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
- 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 3
Used by 2
Lean status
- No associated Lean code or declarations.
Let A be a ring and let X = \Spec (A). Let T be a profinite space and
let T \to \pi_0(X) be a continuous map. Write T = \lim T_i as the limit of
an inverse system of finite discrete spaces over a directed set. Define the ring
A^f_{\pi_0} as follows:
A^f_{\pi_0} := \colim_{(T \to T_i)} A^f_{q_i},
where q_i : T \to T_i are the quotient maps and A^f_{q_i} are the rings
defined in Definition 1.7.18 and the transition maps are those
defined in Definition 1.7.20. By
Lemma 1.7.21 the transition maps are
compatible, thus the colimit is well-defined.
(Stacks Project, Tag 097D)
Lemma1.7.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.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.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 let X = \Spec (A). Let T be a profinite space and
let T \to \pi_0(X) be a continuous map. Then the A-algebra
A^f_{\pi_0} defined in Definition 1.7.22 is ind-Zariski.
Let Y = \Spec (A^f_{\pi_0}). Then \pi_0(Y) \cong T and the diagram
\begin{CD} Y @>>> T \\ @VVV @VVV \\ X @>>> \pi_0(X) \end{CD}
is cartesian in the category of topological spaces.
(Stacks Project, Tag 097D)
Proof for Lemma 1.7.23
Proof uses 3
By Lemma 1.7.19 we see that each
A \to A^f_{q_i} is ind-Zariski, thus A^f_{\pi_0} is ind-Zariski by
Lemma 1.2.4. We have a canonical cartesian diagram
\begin{CD} \Spec (A^f_{q_i}) @>>> Z_i \\ @VVV @VVV \\ X @>>> \pi_0(X) \end{CD}
for every i. Because T = \lim Z_i and
Y = \Spec (A^f_{\pi_0}) = \lim \Spec (A^f_{q_i}), the space Y fits into
the cartesian diagram
\begin{CD} Y @>>> T \\ @VVV @VVV \\ X @>>> \pi_0(X) \end{CD}
of topological spaces. By Lemma 1.1.26 we conclude that
T = \pi_0(Y).
Lemma1.7.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.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
- 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 3
Lean status
- No associated Lean code or declarations.
Let A be a ring. If the following two conditions hold:
-
Ais w-local, and -
\pi_0(\operatorname{Spec}(A))is extremally disconnected.
Then every faithfully flat ring map A \to B identifying local rings with
B w-local and whose closed points of \Spec (B) are exactly V(IB) has a
retraction.
(Stacks Project, Tag 09AZ, second
part in the proof of (3) ⟹ (1))
Proof for Lemma 1.7.24
Proof uses 9
Let A \to B be faithfully flat and identifying local rings, with B
w-local and whose closed points of \Spec (B) are exactly V(IB). We will
show that A \to B has a retraction.
Choose a continuous section to the surjective continuous map
V(IB) \to V(I). This is possible because
V(I) = \Spec(A)^c \cong \pi_0(\Spec(A)) (by
Lemma 1.5.16) is extremally disconnected, see
Theorem 1.1.2. The image is a closed
subspace T \subset \pi_0(\Spec(B)) \cong V(IB) (being the continuous image of
the quasi-compact space V(I)) that maps homeomorphically onto
\pi_0(\Spec(A)).
Let B \to B_T be the ring map from
Definition 1.7.16, which is surjective and
ind-Zariski by
Lemma 1.7.17. It also
induces a homeomorphism \pi_0(\Spec(B_T)) \cong T \cong \pi_0(\Spec(A)).
Moreover, by Lemma 1.6.3, B_T is w-local and
B \to B_T is w-local. Since ind-Zariski maps identify local rings
(Lemma 1.2.2), the composition
A \to B \to B_T remains w-local (Lemma 1.5.4)
and identifies local rings
(Lemma 1.1.31). Therefore, by
Lemma 1.6.6, A \to B_T
is an isomorphism.