Omitted, will be in mathlib soon.

Let \(R = \operatorname {colim}_i R_i\) with \(R_i\) local rings and \(R_i \to R_j\) a local ring map. Suppose \(x, y \in R_i\) are non-units. Since \(R_i\) is local, their sum is a not a unit. If the image of \(x + y\) in \(\operatorname {colim}_i R_i\) is a unit, their exists a \(j\) such that the image of \(x + y\) is a unit in \(R_j\). But this does not happen because \(R_i \to R_j\) is a local ring map.

Omitted.

Since \(S\) is integral over \(R\), it is the colimit of its finite \(R\)-sub-algebras. Since a subring of an integral domain is still an integral domain, by Lemma 2.2 we may assume that \(S\) is finite over \(R\). By Lemma 2.1, \(S\) is a product of (Henselian) local rings and hence local as an integral domain.

This follows from going-up (use Ideal.IsMaximal.under).

It suffices to show that \(\kappa (S)\) is integral over \(R\). Since \(S\) is integral over \(R\) and \(\kappa (S)\) is integral over \(S\) (the map \(S \to \kappa (S)\) is surjective), the composition \(R \to S \to \kappa (S)\) is integral.

Integral is stable under base change, so \(T \to S' = T \otimes _{R} S\) is integral. Hence by going-up any maximal ideal of \(S'\) lies over \(\mathfrak {m}_T\). We have

Again by going-up and since \(S\) is local, \(\mathrm{Spec}(S / \mathfrak {m}_R S)\) is a single point. Thus \(\mathrm{Spec}(S’ / \mathfrak {m}_T S’) \cong \mathrm{Spec}(\kappa (T) \otimes _{\kappa (R)} \kappa (S))\). The latter is a single point, because purely inseparable extensions induce universal homeomorphisms.

Let \(S\) be an étale \(R\)-algebra. Then \(S\) is \(R\)-flat. Also \(S \otimes _{R} S \cong S × T\) for some ring \(T\), in particular \(\mathrm{Spec}(S \otimes _{R} S) \to \mathrm{Spec}(S)\) is an open immersion, hence flat.

Omitted.

Omitted, see [ Sta18 , Tag 092J ] .

Calculation, see [ Sta18 , Tag 092H ] .

First proof:

If \(N'\) is a second \(B\)-module, then

Hence this follows from the definitions.

Second proof by element chasing (which is the proof we actually formalized):

To prove that \(M\) is flat as a \(B\)-module, we will use the equational criterion for flatness: we must show that for any finite relation \(\sum _{i=1}^n b_i m_i = 0\) in \(M\) (where \(b_i \in B\) and \(m_i \in M\)), there exist elements \(m'_s \in M\) and \(d_{is} \in B\) such that \(m_i = \sum _{s=1}^S d_{is} m'_s\) for all \(i\), and \(\sum _{i=1}^n b_i d_{is} = 0\) for all \(s\).

Step 1: The flat epimorphism property.
Let \(I = \ker (\mu )\). Since \(B\) is a flat \(B \otimes _A B\)-module, \(I\) is a pure ideal. Consider the elements \(z_i = 1 \otimes b_i - b_i \otimes 1 \in B \otimes _A B\). Clearly, \(\mu (z_i) = b_i - b_i = 0\), so \(z_i \in I\) for all \(i = 1, \dots , n\).

By the pureness of \(I\), there exists an element \(t = \sum _{k=1}^K u_k \otimes v_k \in B \otimes _A B\) such that \(\mu (t) = 1\) and \(t z_i = 0\) for all \(i\). The condition \(\mu (t) = 1\) means \(\sum _{k=1}^K u_k v_k = 1\). The condition \(t z_i = 0\) implies \(t(1 \otimes b_i) = t(b_i \otimes 1)\), which expands to:

Step 2: Constructing a relation in \(B \otimes _A M\).
Define the elements \(y_i \in B \otimes _A M\) for \(i = 1, \dots , n\) by:

Let us evaluate the sum \(\sum _{i=1}^n b_i y_i\) in the \(B\)-module \(B \otimes _A M\) (where \(B\) acts on the left factor):

Because the map \(x \otimes y \mapsto x \otimes ym_i\) from \(B \otimes _A B \to B \otimes _A M\) is a well-defined \(A\)-linear homomorphism, we can apply it to equation (1) to shift the \(b_i\) factor:

Summing this over all \(i\) yields:

By our initial assumption, \(\sum _{i=1}^n b_i m_i = 0\) in \(M\). Therefore:

Step 3: Utilizing the \(A\)-flatness of \(M\).
We now leverage a standard element-theoretic property of flat modules: because \(M\) is flat over \(A\), any relation of the form \(\sum e_l \otimes x_l = 0\) in \(E \otimes _A M\) (for any \(A\)-module \(E\)) implies there exist \(x'_s \in M\) and \(a_{ls} \in A\) such that \(x_l = \sum _s a_{ls} x'_s\) and \(\sum _l e_l a_{ls} = 0\).

Applying this principle to equation (??) with \(E = B\), where the terms are indexed by pairs \((i, k)\), there exist elements \(m'_s \in M\) (for \(s = 1, \dots , S\)) and scalars \(a_{iks} \in A\) such that:

Step 4: Reconstructing the \(B\)-trivialization.
Consider the evaluation map \(\mu _M: B \otimes _A M \to M\) given by \(b \otimes m \mapsto bm\). Applying \(\mu _M\) to \(y_i\) gives:

Substitute equation (3) into this expansion of \(m_i\):

Define \(d_{is} = \sum _{k=1}^K u_k a_{iks} \in B\). This immediately gives our required reconstruction:

Finally, we must verify that these coefficients annihilate \(b_i\). We compute:

By equation (4), this sum is exactly \(0\) in \(B\) for every \(s\).

Thus, we have successfully trivialized the arbitrary relation \(\sum _{i=1}^n b_i m_i = 0\) over \(B\). By the equational criterion, \(M\) is a flat \(B\)-module.

First proof (the formalized version):

It follows from Lemma 2.14 immediately.

Second proof by element chasing:

Let \(A = B \otimes _k B\). The multiplication map \(\mu : A \to B\) is a surjective ring homomorphism. Because \(B\) is assumed to be a flat \(A\)-module, \(\mu \) is a flat epimorphism. A fundamental property of flat epimorphisms is that their kernel, \(J = \ker (\mu )\), is a pure ideal. The equational criterion for flatness dictates that for any element \(z \in J\), there exists a "localizing" element \(t \in A\) such that \(\mu (t) = 1\) and \(t z = 0\).

Let \(\mathfrak {m}\) be the unique maximal ideal of the local ring \(B\). We wish to show that \(\mathfrak {m} = 0\). Suppose for the sake of contradiction that there exists a non-zero element \(x \in \mathfrak {m}\).

Consider the element \(z = x \otimes 1 - 1 \otimes x \in A\). Clearly, \(\mu (z) = x - x = 0\), so \(z \in J\). By the pureness of \(J\), there exists \(t \in B \otimes _k B\) such that \(\mu (t) = 1\) and

Let \(K = B/\mathfrak {m}\) be the residue field of \(B\), and let \(\pi : B \to K\) be the natural quotient map. We base-change our equation along the homomorphism \(1 \otimes \pi : B \otimes _k B \to B \otimes _k K\). Because \(x \in \mathfrak {m}\), we have \(\pi (x) = 0\), which means \((1 \otimes \pi )(1 \otimes x) = 1 \otimes 0 = 0\).

Let \(\bar{t} = (1 \otimes \pi )(t) \in B \otimes _k K\). Applying \(1 \otimes \pi \) to our annihilator equation isolates the \(x \otimes 1\) term:

Since \(K\) is a field extension of \(k\), it is a free \(k\)-module. Because tensor products preserve freeness, \(N = B \otimes _k K\) is a free left \(B\)-module. The element \(x \otimes 1\) represents scalar multiplication by \(x\) on \(N\). Thus, the relation \(x \bar{t} = 0\) implies that \(x\) annihilates the content ideal \(c(\bar{t})\) of \(\bar{t}\) in \(B\) (the ideal generated by the coordinates of \(\bar{t}\) with respect to a basis), meaning \(x \cdot c(\bar{t}) = 0\).

Now, consider the evaluation map \(\mu _K: B \otimes _k K \to K\) given by \(b \otimes v \mapsto \pi (b)v\). This evaluates \(\bar{t}\) at the central point of the local ring:

Since \(\mu _K(\bar{t}) = 1 \neq 0\), the coordinates of \(\bar{t}\) cannot all map to zero under \(\pi \). Thus, they cannot all lie in \(\mathfrak {m}\). This implies the content ideal \(c(\bar{t})\) is not contained in \(\mathfrak {m}\).

Because \(B\) is a local ring, the only ideal not contained in the unique maximal ideal is the unit ideal itself. Therefore, \(c(\bar{t}) = B\).

Substituting this into our annihilator relation yields \(x \cdot B = 0\), which forces \(x = 0\). This directly contradicts our initial assumption that \(x \neq 0\). We conclude that \(\mathfrak {m} = 0\), meaning the local ring \(B\) has only the trivial maximal ideal. Therefore, \(B\) is a field.

It suffices to show that \(X\) is Hausdorff and totally disconnected. Let \(x \neq y\) be in \(X\). Since \(X\) is quasi-sober and pre-spectral, we may assume that there exists a quasi-compact open \(U\) with \(x \in U\) and \(y \not\in U\). By assumption, its complement is open and \(X\) is Hausdorff. This argument also shows that \(x\) and \(y\) lie in distinct connected components, so \(X\) is totally disconnected.

It suffices to show that for every \(f \in A\), there exists an idempotent element \(e \in A\) such that \((f) = (e)\). Indeed, if \(f ^n = 0\) for some \(n\), then \(e = e ^n \in (f ^n) = 0\). Hence \(f = 0\). For the second claim observe that every quasi-compact open \(D(f) = D(e)\) is closed. Hence the claim follows from 2.16 and the fact that every quasi-compact open of \(\mathrm{Spec}(A)\) is a finite union of basic opens.

Now let \(f \in A\) be any element. Since \((f)\) is pure by assumption it is nilpotent by Ideal.isIdempotentElem_of_pure and every idempotent finitely generated ideal is generated by an idempotent element by Ideal.isIdempotentElem_iff_of_fg.

Localizations of reduced rings are reduced and reduced, local rings of Krull dimension \(\le 0\) are fields.

It suffices to show that for any finitely generated ideal \(I\), the linear map \(I \otimes _{R} N \to N\) is injective. For this, consider the following commutative diagram:

The left vertical map is injective, because \(I\) is flat by assumption on \(R\). The bottom horizontal map is injective, because \(M\) is flat. Hence \(I \otimes _{R} N \to N \to M\) is injective, from which the claim follows.

Immediate consequence of Lemma 2.20.

Let \(M\) be a flat \(B\)-module and \(N \subseteq M\) a submodule. By Lemma 2.14 it suffices to show that \(N\) is \(A\)-flat. Since \(B\) is \(A\)-flat, \(M\) is also \(A\)-flat and hence its submodule \(N\) is \(A\)-flat by Lemma 2.20.

TBA.

Let \(I \subseteq \prod _{i \in I} A_i\) be a finitely generated ideal. Let \(I_i \subseteq A_i\) be the image of \(I\) in \(A_i\). By Lemma 2.23, \(I\) is the product of the \(I_i\). Since each \(A_i\) is a valuation ring, there exists \(f_i \in A_i\) such that \(I_i = (f_i)\). Hence \(I = (f)\) where \(f = (f_i)\). Let \(e \in A\) be the idempotent element defined by

and let \(g\) be the element defined by

Since every \(A_i\) is a domain, \(g\) is a non-zerodivisor and \(f = g e\). In particular, the \(A\)-linear map \((e) \to (ge) = (f)\) is an isomorphism: It is surjective by construction and injective because \(g\) is a nonzerodivisor. Since \(e\) is idempotent, we have \(A = (e) \oplus (1 - e)\) as \(A\)-modules, so \((e)\) is projective.

Let \(x \in B\) be integral over \(A\) and \(A' = A[x]\). The map \(A \to A'\) is injective and finite, so to show \(A = A'\) it suffices to check that \(A \to A'\) is an epimorphism. By Lemma 2.20, \(A'\) is flat over \(A\). Hence the composition

is injective.

TBA.

TBA.

It suffices to show the first statement. A field is absolutely flat ring by Lemma 2.11, hence \(B\) is a absolutely flat ring by Lemma 2.15. And \(B\) is reduced and every local ring is a field, by Lemma 2.17 and Lemma 2.18.

Let \(q \subset B\) be a prime. The ring map \(B \to B_q\) is weakly étale by Lemma 2.10, hence \(B_q\) is weakly étale over \(K\) (Lemma 2.12). Thus \(B_q\) is a separable algebraic extension of \(K\) by Lemma 2.28.

Let \(K \subset A \subset B\) be a finitely generated \(K\)-sub algebra. We will show that \(A\) is étale over \(K\) which will finish the proof of the lemma.

TBA.

Then every minimal prime \(p \subset A\) is the image of a prime \(q\) of \(B\), see Algebra, Lemma 00FK. Thus κ(p) as a subfield of Bq=κ(q) is separable algebraic over K. Hence every generic point of Spec(A) is closed (Algebra, Lemma 00GA). Thus dim(A)=0. Then A is the product of its local rings, e.g., by Algebra, Proposition 00KJ. Moreover, since A is reduced, all local rings are equal to their residue fields which are finite separable over K. This means that A is étale over K by Algebra, Lemma 00U3 and finishes the proof.

Omitted.

The unique prime ideal of \(A\) is the nilradical \(N\) of \(A\). By Lemma 2.30, the kernel of \(A \otimes _k A \to k = A/N\) is generated by \(N \otimes _k A\) and \(A \otimes _k N\), which are all consisiting of nilpotent elements. Thus the nilpotent ideal of \(A \otimes _k A\) is also the maximal ideal. This finishes the proof.

It suffices to show that, for every prime \(p\) of \(A\), there is exactly one prime ideal \(q'\) of \(B \otimes _A B\) lying over \(p\). To detect this, we may assume \(A\) is a field by replacing \(A\) with \(\kappa (\mathfrak {p})\), \(B\) with \(\kappa (\mathfrak {p}) \otimes _A B\) which is a local ring. Now the goal follows from Lemma 2.31.

Recall that a pure ideal \(I\) in \(A\) is an ideal such that \(A/I\) is flat. (Use Ideal.Pure.) In our case, let \(I\) be the kernel of the map \(A \to B\). Then \(I\) is pure and has empty vanishing locus. But we know that pure ideals are determined by their vanishing locus (Ideal.zeroLocus_inj_of_pure) and zero ideal is also a pure ideal having the same vanishing locus with \(I\), thus \(I = 0\).

Omitted. Use Algebra.IsEpi.

By ??, the map \(B \to B \otimes _A B\), which is a base change of \(A \to B\), is isomorphism. So is \(A \to B\) by faithfully flatness.

To see this, suppose that we are under the above hypothesis. This implies that \(\mu : B \otimes _A B \to B\) is bijective on spectra by Lemma 2.32, as well as surjective and flat (immediately by Definition 2.8). Hence it is an isomorphism by Lemma 2.33. Together with the fact that \(A \to B\) is a faithfully (by surjectivity on spectrum) flat, we can apply Lemma 2.35 to conclude \(A = B\).

Suppose \(x, y\) are two distinct points that lives in the same connected component. Then the projection of \(x, y\) will be always fall in the same connected components, thus equal. This is a contradiction.

Writing \(B\) as a filtered colimit \(\operatorname {colim}B_i\) of étale algebra over \(K\). Each \(B_i\) is a product of separable field extensions of \(K\). In particular, the spectrum of \(B_i\)’s are totally disconnected. By Lemma 2.37, the spectrum of \(B\) is again totally disconnected. Thus different prime ideals \(q_1\) and \(q_2\) livs in different connected components. This giving the desire nontrivial idempotent element.

Writing \(B\) as a filtered colimit \(\operatorname {colim}B_i\) of étale algebra over \(K\). (Each \(B_i\) is a product of separable field extensions of \(K\).) Let \(q_i\) be the inverse image of \(q\) in \(B_i\), \(\kappa (q_i)\) be the residue field of \(q_i\), then \(K_i\) is a separable field extensions of \(K\). Now \(\kappa (q) = \operatorname {colim}\kappa (q_i)\) is again a separable extension of \(K\). Then \(\kappa (q) \otimes _A B = \kappa (q) \otimes _K \kappa (q)\) splits. The conclusion follows.

Let \(R'\) be the integral closure of \(R / \mathfrak {p}\) in \(L\). Since \(R \to R / \mathfrak {p} \to R'\) is integral, \(R'\) is local by Lemma 2.4. Moreover, the residue field \(\kappa (R')\) is an algebraic extension of \(\kappa (R)\) by Lemma 2.6. Since \(\kappa (R)\) is separably closed, the extension is purely inseparable. Hence \(R' \otimes _{R} S\) is local by Lemma 2.7. By Lemma 2.27 and since \(R'\) is integrally closed in \(L\), the tensor product \(R' \otimes _{R} S\) is integrally closed in \(L \otimes _{R} S\). Since \(R' \otimes _{R} S\) is local and any idempotent of \(L \otimes _{R} S\) is integral over \(R' \otimes _{R} S\), the latter can not have any non-trivial idemponent elements.

It suffices to show that for all \(\mathfrak {p} \subset A\) there is a unique prime \(\mathfrak {q} \subset B\) lying over \(\mathfrak {p}\) and \(\kappa (\mathfrak {p}) = \kappa (\mathfrak {q})\) by Lemma 2.36

Note that the fibre ring \(\kappa (\mathfrak {p}) \otimes _A B\) is weakly etale over \(\kappa (\mathfrak {p})\) by Lemma 2.13, thus it is a colimit of étale extensions of \(\kappa (\mathfrak {p})\) by Theorem 2.29. If the conclusion does not hold, at least one of the following cases is true:

1. there exists more than one prime \(\mathfrak {q}\_ 1, \mathfrak {q}\_ 2\) lying over \(\mathfrak {p}\);

2. if \(\kappa (\mathfrak {p}) \neq \kappa (\mathfrak {q})\) for some \(\mathfrak {q}\).

In the first case, by Lemma 2.38; in the second case, by Lemma 2.39, we can always find some \(L\) then \(L \otimes _A B\) has a nontrivial idempotent for some (separable) algebraic field extension \(L/\kappa (\mathfrak {p})\).

Now the statement follows from Lemma 2.40.

This is simply Theorem 2.41 plus Lemma 1.48.

TBA.

By Lemma 1.32, the induced map \(A_w \to B_w\) is again bijective on stalks and hence ind-Zariski by Lemma 2.43. Since \(B \to B_w\) is ind-Zariski and faithfully flat and the composition \(A \to B \to B_w\) is ind-Zariski, the claim follows.

TBA.