2.3. Fields
- Lemma 2.1
- Lemma 2.2
- Lemma 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.6
- Lemma 2.7
- Definition 2.1.1
- Definition 2.1.2
- Lemma 2.1.3
- Lemma 2.1.4
- Lemma 2.1.5
- Lemma 2.1.6
- Lemma 2.1.7
- Lemma 2.1.8
- Lemma 2.1.9
- Lemma 2.1.10
- Lemma 2.1.11
- Lemma 2.1.12
- Definition 2.2.1
- Lemma 2.2.2
- Corollary 2.2.3
- Lemma 2.2.4
- Lemma 2.2.5
- Lemma 2.2.6
- Lemma 2.2.7
- Lemma 2.2.8
- Lemma 2.2.9
- Theorem 2.3.2
- Lemma 2.4.1
- Lemma 2.4.2
- Lemma 2.4.3
- Lemma 2.4.4
- Lemma 2.4.5
- Lemma 2.4.6
- Lemma 2.4.7
- Lemma 2.4.8
- Lemma 2.4.9
- Lemma 2.4.10
- Lemma 2.4.11
- Theorem 2.4.12
- Theorem 2.4.13
- Lemma 2.5.1
- Proposition 2.5.2
- Theorem 2.6.1
-
Algebra.WeaklyEtale.isAlgebraic[sorry in proof]
Let L/K be an extension of fields. If L \otimes_K L \to L is flat, then
L is an algebraic separable extension of K.
(Stacks Project, Tag 092P)
Lean code for Lemma2.3.1●1 theorem, incomplete
Associated Lean declarations
-
Algebra.WeaklyEtale.isAlgebraic[sorry in proof]
-
Algebra.WeaklyEtale.isAlgebraic[sorry in proof]
-
theoremdefined in Proetale/Algebra/WeaklyEtaleField.leancontains sorry
theorem Algebra.WeaklyEtale.isAlgebraic.{u, u_1} {k : Type u} [Field k] {L : Type u_1} [Field L] [Algebra k L] [Algebra.WeaklyEtale k L] : Algebra.IsSeparable k L
theorem Algebra.WeaklyEtale.isAlgebraic.{u, u_1} {k : Type u} [Field k] {L : Type u_1} [Field L] [Algebra k L] [Algebra.WeaklyEtale k L] : Algebra.IsSeparable k L
Any weakly étale extension of fields is algebraic separable
- Lemma 2.1
- Lemma 2.2
- Lemma 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.6
- Lemma 2.7
- Definition 2.1.1
- Definition 2.1.2
- Lemma 2.1.3
- Lemma 2.1.4
- Lemma 2.1.5
- Lemma 2.1.6
- Lemma 2.1.7
- Lemma 2.1.8
- Lemma 2.1.9
- Lemma 2.1.10
- Lemma 2.1.11
- Lemma 2.1.12
- Definition 2.2.1
- Lemma 2.2.2
- Corollary 2.2.3
- Lemma 2.2.4
- Lemma 2.2.5
- Lemma 2.2.6
- Lemma 2.2.7
- Lemma 2.2.8
- Lemma 2.2.9
- Lemma 2.3.1
- Lemma 2.4.1
- Lemma 2.4.2
- Lemma 2.4.3
- Lemma 2.4.4
- Lemma 2.4.5
- Lemma 2.4.6
- Lemma 2.4.7
- Lemma 2.4.8
- Lemma 2.4.9
- Lemma 2.4.10
- Lemma 2.4.11
- Theorem 2.4.12
- Theorem 2.4.13
- Lemma 2.5.1
- Proposition 2.5.2
- Theorem 2.6.1
-
Algebra.WeaklyEtale.indEtale_field[sorry in proof] -
Algebra.WeaklyEtale.etale_of_fg[sorry in proof]
Let K be a field. Suppose that K \to B is weakly étale, then
-
every finitely generated
K-subalgebra ofBis étale overK, -
Bis a filtered colimit of étaleK-algebras, i.e.Bis ind-étale.
(Stacks Project, Tag 092Q, (2) ⟹ (3) and last part)
Lean code for Theorem2.3.2●2 theorems, 2 incomplete
Associated Lean declarations
-
Algebra.WeaklyEtale.indEtale_field[sorry in proof]
-
Algebra.WeaklyEtale.etale_of_fg[sorry in proof]
-
Algebra.WeaklyEtale.indEtale_field[sorry in proof] -
Algebra.WeaklyEtale.etale_of_fg[sorry in proof]
-
theoremdefined in Proetale/Algebra/WeaklyEtaleField.leancontains sorry
theorem Algebra.WeaklyEtale.indEtale_field.{u} (k : Type u) [Field k] (R : Type u) [CommRing R] [Algebra k R] [Algebra.WeaklyEtale k R] : Algebra.IndEtale k R
theorem Algebra.WeaklyEtale.indEtale_field.{u} (k : Type u) [Field k] (R : Type u) [CommRing R] [Algebra k R] [Algebra.WeaklyEtale k R] : Algebra.IndEtale k R
Any weakly étale algebra over a field is ind-étale.
-
theoremdefined in Proetale/Algebra/WeaklyEtaleField.leancontains sorry
theorem Algebra.WeaklyEtale.etale_of_fg.{u} {k : Type u} [Field k] {R : Type u} [CommRing R] [Algebra k R] [Algebra.WeaklyEtale k R] (A : Subalgebra k R) (hA : A.FG) : Algebra.Etale k ↥A
theorem Algebra.WeaklyEtale.etale_of_fg.{u} {k : Type u} [Field k] {R : Type u} [CommRing R] [Algebra k R] [Algebra.WeaklyEtale k R] (A : Subalgebra k R) (hA : A.FG) : Algebra.Etale k ↥A
Any finitely-generated subalgebra of a weakly étale algebra is étale.
It suffices to show the first statement. A field is an absolutely flat ring by
Lemma 2.1.4, hence B is an absolutely flat ring by
Lemma 2.1.9. And B is reduced and
every local ring is a field, by
Lemma 2.1.11 and
Lemma 2.1.12.
Let q \subset B be a prime. The ring map B \to B_q is weakly étale by
Lemma 2.1.6, hence B_q is weakly étale over
K (Lemma 2.1.5). Thus B_q is a separable algebraic
extension of K by Lemma 2.3.1.
Let K \subset A \subset B be a finitely generated K-subalgebra. 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.
Thus \kappa(p) as a subfield of B_q = \kappa(q) is separable algebraic
over K. Hence every generic point of \mathrm{Spec}(A) is closed. Thus
\dim(A) = 0. Then A is the product of its local rings. 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 and
finishes the proof.