2.6. Weakly étale and ind-étale
Theorem2.6.1
Group: Weakly étale ring maps, weak dimension, and the comparison between weakly étale and ind-étale, following Section 2 of Bhatt–Scholze and the Stacks Project. (45)
- 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
- Theorem 2.4.13
- Lemma 2.5.1
- Proposition 2.5.2
Associated Lean declarations
-
RingHom.WeaklyEtale.exists_indEtale_comp[complete] -
Algebra.WeaklyEtale.exists_indEtale[sorry in proof]
Let R \to S be weakly étale. Then there exists a faithfully flat ind-étale
morphism S \to T such that the composition R \to T is ind-étale.
Lean code for Theorem2.6.1●2 theorems, 1 incomplete
Associated Lean declarations
-
RingHom.WeaklyEtale.exists_indEtale_comp[complete]
-
Algebra.WeaklyEtale.exists_indEtale[sorry in proof]
Associated Lean declarations
-
RingHom.WeaklyEtale.exists_indEtale_comp[complete] -
Algebra.WeaklyEtale.exists_indEtale[sorry in proof]
-
theoremdefined in Proetale/Algebra/IndWeaklyEtale.leancomplete
theorem RingHom.WeaklyEtale.exists_indEtale_comp.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.WeaklyEtale) : ∃ T x g, g.IndEtale ∧ g.FaithfullyFlat ∧ (g.comp f).IndEtale
theorem RingHom.WeaklyEtale.exists_indEtale_comp.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.WeaklyEtale) : ∃ T x g, g.IndEtale ∧ g.FaithfullyFlat ∧ (g.comp f).IndEtale
If `S` is a weakly étale `R`-algebra, there exists a faithfully flat, ind-étale `S`-algebra `T` such that `T` is an ind-étale `R`-algebra.
-
theoremdefined in Proetale/Algebra/IndWeaklyEtale.leancontains sorry
theorem Algebra.WeaklyEtale.exists_indEtale.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.WeaklyEtale R S] : ∃ T x x_1 x_2, ∃ (_ : IsScalarTower R S T), Algebra.IndEtale S T ∧ Module.FaithfullyFlat S T ∧ Algebra.IndEtale R T
theorem Algebra.WeaklyEtale.exists_indEtale.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.WeaklyEtale R S] : ∃ T x x_1 x_2, ∃ (_ : IsScalarTower R S T), Algebra.IndEtale S T ∧ Module.FaithfullyFlat S T ∧ Algebra.IndEtale R T
If `S` is a weakly étale `R`-algebra, there exists a faithfully flat, ind-étale `S`-algebra `T` such that `T` is an ind-étale `R`-algebra.
Proof for Theorem 2.6.1
Proof uses 2
TBA.