1.4. Ind-étale ring maps
Definition1.4.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
- 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
- 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[complete] -
RingHom.IndEtale[complete]
An R-algebra S is ind-étale if it is a filtered colimit of étale
R-algebras. We say a ring homomorphism f \colon R \to S is ind-étale if
S is ind-étale as an R-algebra via f.
(Stacks Project, Tag 097I)
Lean code for Definition1.4.1●2 definitions
Associated Lean declarations
-
Algebra.IndEtale[complete]
-
RingHom.IndEtale[complete]
Associated Lean declarations
-
Algebra.IndEtale[complete] -
RingHom.IndEtale[complete]
-
classdefined in Proetale/Algebra/IndEtale.leancomplete
class Algebra.IndEtale.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : Prop
class Algebra.IndEtale.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : Prop
An algebra is ind-étale if it can be written as the filtered colimit of étale algebras.
Methods
exists_colimitPresentation : ∃ ι x, ∃ (_ : CategoryTheory.IsFiltered ι), ∃ P, ∀ (i : ι), Algebra.Etale R ↑(P.diag.obj i)
-
defdefined in Proetale/Algebra/IndEtale.leancomplete
def RingHom.IndEtale.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : Prop
def RingHom.IndEtale.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : Prop
A ring hom is ind-étale if and only if it is an ind-étale algebra.
Lemma1.4.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.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
- 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.trans[complete] -
RingHom.IndEtale.comp[complete]
Let A \to B and B \to C be ring maps. If A \to B and B \to C are
ind-étale, then A \to C is ind-étale.
(Stacks Project, Tag 0BSI)
Lean code for Lemma1.4.2●2 theorems
Associated Lean declarations
-
Algebra.IndEtale.trans[complete]
-
RingHom.IndEtale.comp[complete]
Associated Lean declarations
-
Algebra.IndEtale.trans[complete] -
RingHom.IndEtale.comp[complete]
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem Algebra.IndEtale.trans.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (T : Type u) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.IndEtale R S] [Algebra.IndEtale S T] : Algebra.IndEtale R T
theorem Algebra.IndEtale.trans.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (T : Type u) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.IndEtale R S] [Algebra.IndEtale S T] : Algebra.IndEtale R T
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem RingHom.IndEtale.comp.{u} {R S : Type u} [CommRing R] [CommRing S] {T : Type u} [CommRing T] {g : S →+* T} {f : R →+* S} (hg : g.IndEtale) (hf : f.IndEtale) : (g.comp f).IndEtale
theorem RingHom.IndEtale.comp.{u} {R S : Type u} [CommRing R] [CommRing S] {T : Type u} [CommRing T] {g : S →+* T} {f : R →+* S} (hg : g.IndEtale) (hf : f.IndEtale) : (g.comp f).IndEtale
Lemma1.4.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.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
- 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
-
RingHom.IndEtale.isStableUnderBaseChange[complete]
Let A \to B be an ind-étale ring map. For any ring map A \to C, the base
change C \to B \otimes_A C is ind-étale.
(Stacks Project, Tag 0BSH)
Lean code for Lemma1.4.3●1 theorem
Associated Lean declarations
-
RingHom.IndEtale.isStableUnderBaseChange[complete]
Associated Lean declarations
-
RingHom.IndEtale.isStableUnderBaseChange[complete]
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem RingHom.IndEtale.isStableUnderBaseChange.{u_1} : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.IndEtale
theorem RingHom.IndEtale.isStableUnderBaseChange.{u_1} : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.IndEtale
Ind-étale ring homomorphisms are stable under base change.
Lemma1.4.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.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
- 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.of_colimitPresentation[complete] -
RingHom.IndEtale.iff_ind_indEtale[complete] -
RingHom.IndEtale.of_isColimit[complete] -
Algebra.IndEtale.iff_ind_indEtale[complete]
Let B = \colim_i B_i be a filtered colimit of ind-étale A-algebras. Then
B is an ind-étale A-algebra.
Lean code for Lemma1.4.4●4 theorems
Associated Lean declarations
-
Algebra.IndEtale.of_colimitPresentation[complete]
-
RingHom.IndEtale.iff_ind_indEtale[complete]
-
RingHom.IndEtale.of_isColimit[complete]
-
Algebra.IndEtale.iff_ind_indEtale[complete]
Associated Lean declarations
-
Algebra.IndEtale.of_colimitPresentation[complete] -
RingHom.IndEtale.iff_ind_indEtale[complete] -
RingHom.IndEtale.of_isColimit[complete] -
Algebra.IndEtale.iff_ind_indEtale[complete]
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem Algebra.IndEtale.of_colimitPresentation.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] {ι : Type u} [CategoryTheory.SmallCategory ι] [CategoryTheory.IsFiltered ι] (P : CategoryTheory.Limits.ColimitPresentation ι (CommAlgCat.of R S)) (h : ∀ (i : ι), Algebra.IndEtale R ↑(P.diag.obj i)) : Algebra.IndEtale R S
theorem Algebra.IndEtale.of_colimitPresentation.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] {ι : Type u} [CategoryTheory.SmallCategory ι] [CategoryTheory.IsFiltered ι] (P : CategoryTheory.Limits.ColimitPresentation ι (CommAlgCat.of R S)) (h : ∀ (i : ι), Algebra.IndEtale R ↑(P.diag.obj i)) : Algebra.IndEtale R S
If every stage of a filtered colimit presentation of `S` over `R` is ind-étale, then `S` is ind-étale over `R`.
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem RingHom.IndEtale.iff_ind_indEtale.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : f.IndEtale ↔ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => RingHom.IndEtale).ind (CommRingCat.ofHom f)
theorem RingHom.IndEtale.iff_ind_indEtale.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : f.IndEtale ↔ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => RingHom.IndEtale).ind (CommRingCat.ofHom f)
Ind-étale is equivalent to ind-ind-étale.
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem RingHom.IndEtale.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)).IndEtale ∧ CategoryTheory.CategoryStruct.comp (t.app i) (c.app i) = f) : (CommRingCat.Hom.hom f).IndEtale
theorem RingHom.IndEtale.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)).IndEtale ∧ CategoryTheory.CategoryStruct.comp (t.app i) (c.app i) = f) : (CommRingCat.Hom.hom f).IndEtale
A ring hom is ind-étale if it can be written as a filtered colimit of ind-étale maps.
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem Algebra.IndEtale.iff_ind_indEtale.{u} {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] : Algebra.IndEtale R S ↔ (RingHom.toObjectProperty (fun {R S} [CommRing R] [CommRing S] => RingHom.IndEtale) R).ind (CommAlgCat.of R S)
theorem Algebra.IndEtale.iff_ind_indEtale.{u} {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] : Algebra.IndEtale R S ↔ (RingHom.toObjectProperty (fun {R S} [CommRing R] [CommRing S] => RingHom.IndEtale) R).ind (CommAlgCat.of R S)
Ind-étale algebras are equivalent to ind-ind-étale algebras.
Proof for Lemma 1.4.4
uses 0
This follows from general theory, because étale maps are of finite presentation.
Lemma1.4.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
- 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
- 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
-
Algebra.IndEtale.of_indZariski[complete] -
RingHom.IndZariski.indEtale[complete]
Let A \to B be an ind-Zariski ring map. Then A \to B is ind-étale.
Lean code for Lemma1.4.5●2 theorems
Associated Lean declarations
-
Algebra.IndEtale.of_indZariski[complete]
-
RingHom.IndZariski.indEtale[complete]
Associated Lean declarations
-
Algebra.IndEtale.of_indZariski[complete] -
RingHom.IndZariski.indEtale[complete]
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem Algebra.IndEtale.of_indZariski.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IndZariski R S] : Algebra.IndEtale R S
theorem Algebra.IndEtale.of_indZariski.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IndZariski R S] : Algebra.IndEtale R S
An ind-Zariski algebra is ind-étale, since localizations are étale.
-
theoremdefined in Proetale/Algebra/IndEtale.leancomplete
theorem RingHom.IndZariski.indEtale.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IndZariski) : f.IndEtale
theorem RingHom.IndZariski.indEtale.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IndZariski) : f.IndEtale
Proof for Lemma 1.4.5
uses 0
An ind-Zariski ring map is a filtered colimit of local isomorphisms. A local isomorphism is étale.