2.4. Local rings
- 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
- Theorem 2.3.2
- 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.TensorProduct.map_ker[complete]
Let A be a ring, let f \colon R \to R', g : S \to S' be two ring maps
of A-algebras. Then the kernel of R \otimes_A S \to R' \otimes_A S' is
generated by \ker f \otimes_A S and R \otimes_A \ker g.
Lean code for Lemma2.4.1●1 theorem
Associated Lean declarations
-
Algebra.TensorProduct.map_ker[complete]
-
Algebra.TensorProduct.map_ker[complete]
-
theoremdefined in Mathlib/LinearAlgebra/TensorProduct/RightExactness.leancomplete
theorem Algebra.TensorProduct.map_ker.{u_4, u_5, u_6, u_7, u_8, u_9} {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra R S] {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [Algebra S A] [Algebra S B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) (g : C →ₐ[R] D) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) : RingHom.ker (Algebra.TensorProduct.map f g) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔ Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
theorem Algebra.TensorProduct.map_ker.{u_4, u_5, u_6, u_7, u_8, u_9} {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra R S] {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [Algebra S A] [Algebra S B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) (g : C →ₐ[R] D) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) : RingHom.ker (Algebra.TensorProduct.map f g) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔ Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
If `f` and `g` are surjective morphisms of algebras, then the kernel of `Algebra.TensorProduct.map f g` is generated by the kernels of `f` and `g`
- 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
- Theorem 2.3.2
- Lemma 2.4.1
- 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.isLocalRing_tensorProduct_of_krullDimLE_zero[sorry in proof] -
Algebra.krullDimLE_zero_tensorProduct_of_krullDimLE_zero[sorry in proof]
Let k be a field, A be a local k-algebra of dimension zero, i.e. there
is a unique prime ideal in A. Suppose that the residue field of A is
identified with k. Then A \otimes_k A is a local k-algebra of
dimension zero.
Lean code for Lemma2.4.2●2 theorems, 2 incomplete
Associated Lean declarations
-
Algebra.isLocalRing_tensorProduct_of_krullDimLE_zero[sorry in proof]
-
Algebra.krullDimLE_zero_tensorProduct_of_krullDimLE_zero[sorry in proof]
-
Algebra.isLocalRing_tensorProduct_of_krullDimLE_zero[sorry in proof] -
Algebra.krullDimLE_zero_tensorProduct_of_krullDimLE_zero[sorry in proof]
-
theoremdefined in Proetale/Algebra/Bijective.leancontains sorry
theorem Algebra.isLocalRing_tensorProduct_of_krullDimLE_zero.{u_3, u_4} (k : Type u_3) [Field k] (R : Type u_4) [CommRing R] [IsLocalRing R] [Algebra k R] [IsLocalHom (algebraMap k R)] [Ring.KrullDimLE 0 R] (h : Function.Bijective ⇑(algebraMap k (IsLocalRing.ResidueField R))) : IsLocalRing (TensorProduct k R R)
theorem Algebra.isLocalRing_tensorProduct_of_krullDimLE_zero.{u_3, u_4} (k : Type u_3) [Field k] (R : Type u_4) [CommRing R] [IsLocalRing R] [Algebra k R] [IsLocalHom (algebraMap k R)] [Ring.KrullDimLE 0 R] (h : Function.Bijective ⇑(algebraMap k (IsLocalRing.ResidueField R))) : IsLocalRing (TensorProduct k R R)
-
theoremdefined in Proetale/Algebra/Bijective.leancontains sorry
theorem Algebra.krullDimLE_zero_tensorProduct_of_krullDimLE_zero.{u_3, u_4} (k : Type u_3) [Field k] (R : Type u_4) [CommRing R] [IsLocalRing R] [Algebra k R] [IsLocalHom (algebraMap k R)] [Ring.KrullDimLE 0 R] (h : Function.Bijective ⇑(algebraMap k (IsLocalRing.ResidueField R))) : Ring.KrullDimLE 0 (TensorProduct k R R)
theorem Algebra.krullDimLE_zero_tensorProduct_of_krullDimLE_zero.{u_3, u_4} (k : Type u_3) [Field k] (R : Type u_4) [CommRing R] [IsLocalRing R] [Algebra k R] [IsLocalHom (algebraMap k R)] [Ring.KrullDimLE 0 R] (h : Function.Bijective ⇑(algebraMap k (IsLocalRing.ResidueField R))) : Ring.KrullDimLE 0 (TensorProduct k R R)
The unique prime ideal of A is the nilradical N of A. By
Lemma 2.4.1, the kernel of
A \otimes_k A \to k = A/N is generated by N \otimes_k A and
A \otimes_k N, which all consist of nilpotent elements. Thus the nilpotent
ideal of A \otimes_k A is also the maximal ideal. This finishes the proof.
- 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
- Theorem 2.3.2
- Lemma 2.4.1
- Lemma 2.4.2
- 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.bijective_comap_lmul'_of_bijective_of_bijective[sorry in proof]
Let A \to B be a ring map. Suppose 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}). Then B \otimes_A B \to B is
bijective on spectra.
Lean code for Lemma2.4.3●1 theorem, incomplete
Associated Lean declarations
-
Algebra.bijective_comap_lmul'_of_bijective_of_bijective[sorry in proof]
-
Algebra.bijective_comap_lmul'_of_bijective_of_bijective[sorry in proof]
-
theoremdefined in Proetale/Algebra/Bijective.leancontains sorry
theorem Algebra.bijective_comap_lmul'_of_bijective_of_bijective.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (hf : Function.Bijective (PrimeSpectrum.comap (algebraMap R S))) (h : ∀ (p : Ideal R) [inst : p.IsPrime] (q : Ideal S) [inst_1 : q.IsPrime] [inst_2 : q.LiesOver p], Function.Bijective ⇑(IsLocalRing.ResidueField.map (Localization.localRingHom p q (algebraMap R S) ⋯))) : Function.Bijective (PrimeSpectrum.comap (Algebra.TensorProduct.lmul' R).toRingHom)
theorem Algebra.bijective_comap_lmul'_of_bijective_of_bijective.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (hf : Function.Bijective (PrimeSpectrum.comap (algebraMap R S))) (h : ∀ (p : Ideal R) [inst : p.IsPrime] (q : Ideal S) [inst_1 : q.IsPrime] [inst_2 : q.LiesOver p], Function.Bijective ⇑(IsLocalRing.ResidueField.map (Localization.localRingHom p q (algebraMap R S) ⋯))) : Function.Bijective (PrimeSpectrum.comap (Algebra.TensorProduct.lmul' R).toRingHom)
If all residue field extensions are trivial and the map on prime spectra is bijective, the map `Spec S ⟶ Spec (S ⊗[R] S)` is bijective.
It suffices to show that, for every prime \mathfrak{p} of A, there is
exactly one prime ideal q' of B \otimes_A B lying over \mathfrak{p}.
To detect this, we may assume A is a field by replacing A with
\kappa(\mathfrak{p}) and B with \kappa(\mathfrak{p}) \otimes_A B,
which is a local ring. Now the goal follows from
Lemma 2.4.2.
- 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
- Theorem 2.3.2
- Lemma 2.4.1
- Lemma 2.4.2
- Lemma 2.4.3
- 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.bijective_of_bijective_of_flat[sorry in proof]
Let A \to B be a ring map that is bijective on spectra, as well as
surjective and flat, then it is an isomorphism.
Lean code for Lemma2.4.4●1 theorem, incomplete
Associated Lean declarations
-
Algebra.bijective_of_bijective_of_flat[sorry in proof]
-
Algebra.bijective_of_bijective_of_flat[sorry in proof]
-
theoremdefined in Proetale/Algebra/Bijective.leancontains sorry
theorem Algebra.bijective_of_bijective_of_flat.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] (hf : Function.Bijective (PrimeSpectrum.comap (algebraMap R S))) (hf' : Function.Surjective ⇑(algebraMap R S)) : Function.Bijective ⇑(algebraMap R S)
theorem Algebra.bijective_of_bijective_of_flat.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] (hf : Function.Bijective (PrimeSpectrum.comap (algebraMap R S))) (hf' : Function.Surjective ⇑(algebraMap R S)) : Function.Bijective ⇑(algebraMap R S)
A flat surjective map `R → S` that is bijective on prime spectra is an isomorphism.
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 the
zero ideal is also a pure ideal having the same vanishing locus as I, thus
I = 0.
- 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
- Theorem 2.3.2
- Lemma 2.4.1
- Lemma 2.4.2
- Lemma 2.4.3
- Lemma 2.4.4
- 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
- No associated Lean code or declarations.
Let A \to B be a ring map. The following are equivalent:
-
A \to Bis an epimorphism; -
the two ring maps
B \to B \otimes_A Bare equal; -
either of the ring maps
B \to B \otimes_A Bis an isomorphism, and -
the ring map
B \otimes_A B \to Bis an isomorphism.
(Stacks Project, Tag 04VN)
Omitted. Use Algebra.IsEpi.
- 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
- 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.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.bijective_of_faithfullyFlat_of_isEpi[sorry in proof]
Let A \to B be a faithfully flat ring epimorphism. Then A \to B is an
isomorphism.
(Stacks Project, Tag 04VU)
Lean code for Lemma2.4.6●1 theorem, incomplete
Associated Lean declarations
-
Algebra.bijective_of_faithfullyFlat_of_isEpi[sorry in proof]
-
Algebra.bijective_of_faithfullyFlat_of_isEpi[sorry in proof]
-
theoremdefined in Proetale/Algebra/Bijective.leancontains sorry
theorem Algebra.bijective_of_faithfullyFlat_of_isEpi.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] [Algebra.IsEpi R S] : Function.Bijective ⇑(algebraMap R S)
theorem Algebra.bijective_of_faithfullyFlat_of_isEpi.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] [Algebra.IsEpi R S] : Function.Bijective ⇑(algebraMap R S)
A faithfully flat epimorphism `R → S` is an isomorphism.
By Lemma 2.4.5, the map B \to B \otimes_A B, which is a
base change of A \to B, is an isomorphism. So is A \to B by faithful
flatness.
- 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
- 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.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
Let A \to B be a weakly étale local homomorphism of local rings. Suppose
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}). Then A \to B is an
isomorphism.
Lean code for Lemma2.4.7●1 theorem, incomplete
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/Bijective.leancontains sorry
theorem Algebra.WeaklyEtale.bijective_algebraMap_of_bijective_residueFieldMap.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [Algebra.WeaklyEtale R S] (h : Function.Bijective (PrimeSpectrum.comap (algebraMap R S))) (hres : ∀ (p : Ideal R) [inst : p.IsPrime] (q : Ideal S) [inst_1 : q.IsPrime] [inst_2 : q.LiesOver p], Function.Bijective ⇑(IsLocalRing.ResidueField.map (Localization.localRingHom p q (algebraMap R S) ⋯))) : Function.Bijective ⇑(algebraMap R S)
theorem Algebra.WeaklyEtale.bijective_algebraMap_of_bijective_residueFieldMap.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [Algebra.WeaklyEtale R S] (h : Function.Bijective (PrimeSpectrum.comap (algebraMap R S))) (hres : ∀ (p : Ideal R) [inst : p.IsPrime] (q : Ideal S) [inst_1 : q.IsPrime] [inst_2 : q.LiesOver p], Function.Bijective ⇑(IsLocalRing.ResidueField.map (Localization.localRingHom p q (algebraMap R S) ⋯))) : Function.Bijective ⇑(algebraMap R S)
Let `R → S` be a weakly étale local homomorphism of local rings. If for every prime `p ⊂ R` there is a unique prime `q ⊂ S` lying over `p` and `κ(p) = κ(q)`, then `R → S` is an isomorphism.
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.4.3, as
well as surjective and flat (immediately by
Definition 2.1.1). Hence it is an isomorphism by
Lemma 2.4.4. Together with the
fact that A \to B is faithfully flat (by surjectivity on spectra), we can
apply Lemma 2.4.6 to conclude A = B.
- 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
- 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.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
Let I be a directed set. Let T_i, i \in I be a family of totally
disconnected topological spaces. Then
T = \varprojlim_{i \in I} T_i
is also totally disconnected.
Lean code for Lemma2.4.8●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/Topology/Connected/TotallyDisconnected.leancomplete
theorem TopCat.limitCone_pt_totallyDisconnectedSpace.{v, u} {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) [∀ (j : J), TotallyDisconnectedSpace ↑(F.obj j)] : TotallyDisconnectedSpace ↑(TopCat.limitCone F).pt
theorem TopCat.limitCone_pt_totallyDisconnectedSpace.{v, u} {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) [∀ (j : J), TotallyDisconnectedSpace ↑(F.obj j)] : TotallyDisconnectedSpace ↑(TopCat.limitCone F).pt
The inverse limit of a system of totally disconnected topological spaces is totally disconnected.
Suppose x, y are two distinct points that live in the same connected
component. Then the projections of x, y will always fall in the same
connected components, thus be equal. This is a contradiction.
- 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
- 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.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.IndEtale.exists_isIdempotentElem_of_two_primes[sorry in proof]
Let B be an ind-étale algebra over some field K. If there are two
different prime ideals q_1 and q_2 in B, then B has a nontrivial
idempotent element e (i.e. e^2 = e).
Lean code for Lemma2.4.9●1 theorem, incomplete
Associated Lean declarations
-
Algebra.IndEtale.exists_isIdempotentElem_of_two_primes[sorry in proof]
-
Algebra.IndEtale.exists_isIdempotentElem_of_two_primes[sorry in proof]
-
theoremdefined in Proetale/Algebra/IndEtale.leancontains sorry
theorem Algebra.IndEtale.exists_isIdempotentElem_of_two_primes.{u} {K B : Type u} [Field K] [CommRing B] [Algebra K B] [Algebra.IndEtale K B] {q₁ q₂ : Ideal B} [q₁.IsPrime] [q₂.IsPrime] (h : q₁ ≠ q₂) : ∃ e, IsIdempotentElem e ∧ e ≠ 0 ∧ e ≠ 1
theorem Algebra.IndEtale.exists_isIdempotentElem_of_two_primes.{u} {K B : Type u} [Field K] [CommRing B] [Algebra K B] [Algebra.IndEtale K B] {q₁ q₂ : Ideal B} [q₁.IsPrime] [q₂.IsPrime] (h : q₁ ≠ q₂) : ∃ e, IsIdempotentElem e ∧ e ≠ 0 ∧ e ≠ 1
If `B` is an ind-étale algebra over a field `K` and `B` has at least two distinct prime ideals, then `B` has a nontrivial idempotent element.
Write B as a filtered colimit \colim B_i of étale algebras over K.
Each B_i is a product of separable field extensions of K. In particular,
the spectra of the B_i are totally disconnected. By
Lemma 2.4.8, the spectrum of B is
again totally disconnected. Thus the different prime ideals q_1 and q_2
live in different connected components. This gives the desired nontrivial
idempotent element.
- 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
- 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.11
- Theorem 2.4.12
- Theorem 2.4.13
- Lemma 2.5.1
- Proposition 2.5.2
- Theorem 2.6.1
Let B be an ind-étale algebra over some field K. If there exists a prime
ideal q of B, such that the residue field of q is not K, then
\kappa(q) \otimes_K B has a nontrivial idempotent element.
Lean code for Lemma2.4.10●1 theorem, incomplete
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/IndEtale.leancontains sorry
theorem Algebra.IndEtale.exists_isIdempotentElem_tensorProduct_of_residueField_ne.{u} {K B : Type u} [Field K] [CommRing B] [Algebra K B] [Algebra.IndEtale K B] (q : Ideal B) [q.IsPrime] (h : ¬Function.Bijective ⇑(algebraMap K q.ResidueField)) : ∃ e, IsIdempotentElem e ∧ e ≠ 0 ∧ e ≠ 1
theorem Algebra.IndEtale.exists_isIdempotentElem_tensorProduct_of_residueField_ne.{u} {K B : Type u} [Field K] [CommRing B] [Algebra K B] [Algebra.IndEtale K B] (q : Ideal B) [q.IsPrime] (h : ¬Function.Bijective ⇑(algebraMap K q.ResidueField)) : ∃ e, IsIdempotentElem e ∧ e ≠ 0 ∧ e ≠ 1
If `B` is an ind-étale algebra over a field `K` and `q` is a prime ideal of `B` whose residue field is strictly larger than `K`, then the tensor product `κ(q) ⊗[K] B` has a nontrivial idempotent element.
Write B as a filtered colimit \colim B_i of étale algebras 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 and \kappa(q_i) be the residue field of
q_i, then \kappa(q_i) is a separable field extension of K. Now
\kappa(q) = \colim \kappa(q_i) is again a separable extension of K. Then
\kappa(q) \otimes_K B \supseteq \kappa(q) \otimes_K \kappa(q) splits. The
conclusion follows.
- 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
- 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
- Theorem 2.4.12
- Theorem 2.4.13
- Lemma 2.5.1
- Proposition 2.5.2
- Theorem 2.6.1
-
Algebra.WeaklyEtale.eq_of_isIdempotentElem[sorry in proof]
Let R be a Henselian local ring with separably closed residue field and
S a weakly étale local R-algebra with R \to S a local homomorphism.
Let \mathfrak{p} be a prime ideal of R and L an algebraic field
extension of \kappa(\mathfrak{p}). Then L \otimes_{R} S has no
non-trivial idempotents.
Lean code for Lemma2.4.11●1 theorem, incomplete
Associated Lean declarations
-
Algebra.WeaklyEtale.eq_of_isIdempotentElem[sorry in proof]
-
Algebra.WeaklyEtale.eq_of_isIdempotentElem[sorry in proof]
-
theoremdefined in Proetale/Algebra/HenselianLocalRing.leancontains sorry
theorem Algebra.WeaklyEtale.eq_of_isIdempotentElem.{u, u_1} {R S : Type u} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)] [Algebra.WeaklyEtale R S] (p : Ideal R) [p.IsPrime] (L : Type u_1) [Field L] [Algebra (IsLocalRing.ResidueField R) L] [Algebra R L] [Algebra.IsAlgebraic (IsLocalRing.ResidueField R) L] [IsScalarTower R (IsLocalRing.ResidueField R) L] {e : TensorProduct R L S} (he : IsIdempotentElem e) : e = 0 ∨ e = 1
theorem Algebra.WeaklyEtale.eq_of_isIdempotentElem.{u, u_1} {R S : Type u} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)] [Algebra.WeaklyEtale R S] (p : Ideal R) [p.IsPrime] (L : Type u_1) [Field L] [Algebra (IsLocalRing.ResidueField R) L] [Algebra R L] [Algebra.IsAlgebraic (IsLocalRing.ResidueField R) L] [IsScalarTower R (IsLocalRing.ResidueField R) L] {e : TensorProduct R L S} (he : IsIdempotentElem e) : e = 0 ∨ e = 1
If `R → S` is a local homomorphism of local rings, `R` is strictly henselian and `S` is weakly-étale over `R`, then for any algebraic field extension `L` of `κ(p)` the tensorproduct `L ⊗[R] S` has no nontrivial idempotent elements.
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.2.9 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 idempotent elements.
- 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
- 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.13
- Lemma 2.5.1
- Proposition 2.5.2
- Theorem 2.6.1
-
Algebra.WeaklyEtale.bijective_of_henselianLocalRing[sorry in proof]
Let A \to B be a local homomorphism of local rings. If A is henselian,
the residue field of A is separably closed, and A \to B is weakly étale,
then A = B.
(Stacks Project, Tag 097Z (Olivier))
Lean code for Theorem2.4.12●1 theorem, incomplete
Associated Lean declarations
-
Algebra.WeaklyEtale.bijective_of_henselianLocalRing[sorry in proof]
-
Algebra.WeaklyEtale.bijective_of_henselianLocalRing[sorry in proof]
-
theoremdefined in Proetale/Algebra/HenselianLocalRing.leancontains sorry
theorem Algebra.WeaklyEtale.bijective_of_henselianLocalRing.{u} {R S : Type u} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)] [Algebra.WeaklyEtale R S] : Function.Bijective ⇑(algebraMap R S)
theorem Algebra.WeaklyEtale.bijective_of_henselianLocalRing.{u} {R S : Type u} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)] [Algebra.WeaklyEtale R S] : Function.Bijective ⇑(algebraMap R S)
If `R → S` is a local homomorphism of local rings, `R` is strictly henselian and `S` is weakly-étale over `R`, then `R → S` is an isomorphism.
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.4.7.
Note that the fibre ring \kappa(\mathfrak{p}) \otimes_A B is weakly étale
over \kappa(\mathfrak{p}) by Lemma 2.1.7, thus
it is a colimit of étale extensions of \kappa(\mathfrak{p}) by
Theorem 2.3.2. If the conclusion
does not hold, at least one of the following cases is true:
-
there exists more than one prime
\mathfrak{q}_1, \mathfrak{q}_2lying over\mathfrak{p}; -
\kappa(\mathfrak{p}) \neq \kappa(\mathfrak{q})for some\mathfrak{q}.
In the first case, by Lemma 2.4.9; in the
second case, by Lemma 2.4.10, we can
always find some (separable) algebraic field extension
L/\kappa(\mathfrak{p}) such that L \otimes_A B has a nontrivial
idempotent.
Now the statement follows from Lemma 2.4.11.
- 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
- 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
- Lemma 2.5.1
- Proposition 2.5.2
- Theorem 2.6.1
Let A \to B be a local homomorphism of local rings. If A is strictly
henselian, and A \to B is weakly étale, then A = B.
Lean code for Theorem2.4.13●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/HenselianLocalRing.leancomplete
theorem Algebra.WeaklyEtale.bijective_of_isStrictlyHenselianLocalRing.{u} {R S : Type u} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [IsStrictlyHenselianLocalRing R] [Algebra.WeaklyEtale R S] : Function.Bijective ⇑(algebraMap R S)
theorem Algebra.WeaklyEtale.bijective_of_isStrictlyHenselianLocalRing.{u} {R S : Type u} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [IsStrictlyHenselianLocalRing R] [Algebra.WeaklyEtale R S] : Function.Bijective ⇑(algebraMap R S)
If `R → S` is a local homomorphism of local rings, `R` is strictly henselian and `S` is weakly étale over `R`, then `R → S` is an isomorphism.
This is simply Theorem 2.4.12 plus Lemma 1.3.4.