1.2. ind-Zariski maps
Definition1.2.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
- 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
- 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
Used by 11
Associated Lean declarations
-
Algebra.IndZariski[complete]
An R-algebra S is called ind-Zariski if S can be written as a
filtered colimit S \simeq \colim S_i with each R \to S_i a local
isomorphism. A ring homomorphism f : R \to S is called ind-Zariski if S
is ind-Zariski as an R-algebra via f.
(Stacks Project, Tag 096N)
Lean code for Definition1.2.1●1 definition
Associated Lean declarations
-
Algebra.IndZariski[complete]
Associated Lean declarations
-
Algebra.IndZariski[complete]
-
classdefined in Proetale/Algebra/IndZariski.leancomplete
class Algebra.IndZariski.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : Prop
class Algebra.IndZariski.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : Prop
An algebra is ind-Zariski if it can be written as the filtered colimit of locally isomorphic algebras.
Methods
exists_colimitPresentation : ∃ ι x, ∃ (_ : CategoryTheory.IsFiltered ι), ∃ P, ∀ (i : ι), Algebra.IsLocalIso R ↑(P.diag.obj i)
The definition of ind-Zariski is slightly more general than (Bhatt–Scholze, Definition 2.2.1(iv)), where it is defined as a filtered colimit of finite products of principal localizations.
Lemma1.2.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.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
- 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
Statement uses 2
Used by 5
Associated Lean declarations
-
Algebra.IndZariski.bijectiveOnStalks_algebraMap[sorry in proof] -
RingHom.IndZariski.bijectiveOnStalks[complete]
Let A \to B be an ind-Zariski ring map. Then it identifies local rings, i.e.
for every prime \mathfrak{q} \subset B the canonical map
A_{\varphi^{-1}(\mathfrak{q})} \to B_{\mathfrak{q}} is an isomorphism.
(Stacks Project, Tag 096T)
Lean code for Lemma1.2.2●2 theorems, 1 incomplete
Associated Lean declarations
-
Algebra.IndZariski.bijectiveOnStalks_algebraMap[sorry in proof]
-
RingHom.IndZariski.bijectiveOnStalks[complete]
Associated Lean declarations
-
Algebra.IndZariski.bijectiveOnStalks_algebraMap[sorry in proof] -
RingHom.IndZariski.bijectiveOnStalks[complete]
-
theoremdefined in Proetale/Algebra/IndZariski.leancontains sorry
theorem Algebra.IndZariski.bijectiveOnStalks_algebraMap.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IndZariski R S] : (algebraMap R S).BijectiveOnStalks
theorem Algebra.IndZariski.bijectiveOnStalks_algebraMap.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IndZariski R S] : (algebraMap R S).BijectiveOnStalks
[Stacks Tag 096T](https://stacks.math.columbia.edu/tag/096T)
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem RingHom.IndZariski.bijectiveOnStalks.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (h : f.IndZariski) : f.BijectiveOnStalks
theorem RingHom.IndZariski.bijectiveOnStalks.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (h : f.IndZariski) : f.BijectiveOnStalks
[Stacks Tag 096T](https://stacks.math.columbia.edu/tag/096T)
Lemma1.2.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.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
- 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
-
Module.Flat.of_indZariski[complete] -
RingHom.IndZariski.flat[complete]
Let A \to B be an ind-Zariski ring map. Then A \to B is flat.
Lean code for Lemma1.2.3●2 theorems
Associated Lean declarations
-
Module.Flat.of_indZariski[complete]
-
RingHom.IndZariski.flat[complete]
Associated Lean declarations
-
Module.Flat.of_indZariski[complete] -
RingHom.IndZariski.flat[complete]
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem Module.Flat.of_indZariski.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IndZariski R S] : Module.Flat R S
theorem Module.Flat.of_indZariski.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.IndZariski R S] : Module.Flat R S
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem RingHom.IndZariski.flat.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (h : f.IndZariski) : f.Flat
theorem RingHom.IndZariski.flat.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (h : f.IndZariski) : f.Flat
Proof for Lemma 1.2.3
uses 0
An ind-Zariski ring map is a filtered colimit of local isomorphisms. A local isomorphism is flat.
Lemma1.2.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.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
- 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
Used by 2
Associated Lean declarations
-
Algebra.IndZariski.of_colimitPresentation[sorry in proof] -
RingHom.IndZariski.of_isColimit[complete] -
Algebra.IndZariski.iff_ind_indZariksi[sorry in proof] -
RingHom.IndZariski.iff_ind_indZariski[sorry in proof]
A filtered colimit of ind-Zariski algebras is ind-Zariski.
Lean code for Lemma1.2.4●4 theorems, 3 incomplete
Associated Lean declarations
-
Algebra.IndZariski.of_colimitPresentation[sorry in proof]
-
RingHom.IndZariski.of_isColimit[complete]
-
Algebra.IndZariski.iff_ind_indZariksi[sorry in proof]
-
RingHom.IndZariski.iff_ind_indZariski[sorry in proof]
Associated Lean declarations
-
Algebra.IndZariski.of_colimitPresentation[sorry in proof] -
RingHom.IndZariski.of_isColimit[complete] -
Algebra.IndZariski.iff_ind_indZariksi[sorry in proof] -
RingHom.IndZariski.iff_ind_indZariski[sorry in proof]
-
theoremdefined in Proetale/Algebra/IndZariski.leancontains sorry
theorem Algebra.IndZariski.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.IndZariski R ↑(P.diag.obj i)) : Algebra.IndZariski R S
theorem Algebra.IndZariski.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.IndZariski R ↑(P.diag.obj i)) : Algebra.IndZariski R S
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem RingHom.IndZariski.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)).IndZariski ∧ CategoryTheory.CategoryStruct.comp (t.app i) (c.app i) = f) : (CommRingCat.Hom.hom f).IndZariski
theorem RingHom.IndZariski.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)).IndZariski ∧ CategoryTheory.CategoryStruct.comp (t.app i) (c.app i) = f) : (CommRingCat.Hom.hom f).IndZariski
A ring hom is ind-Zariski if it can be written as a filtered colimit of ind-Zariski maps.
-
theoremdefined in Proetale/Algebra/IndZariski.leancontains sorry
theorem Algebra.IndZariski.iff_ind_indZariksi.{u} {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] : Algebra.IndZariski R S ↔ (RingHom.toObjectProperty (fun {R S} [CommRing R] [CommRing S] => RingHom.IndZariski) R).ind (CommAlgCat.of R S)
theorem Algebra.IndZariski.iff_ind_indZariksi.{u} {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] : Algebra.IndZariski R S ↔ (RingHom.toObjectProperty (fun {R S} [CommRing R] [CommRing S] => RingHom.IndZariski) R).ind (CommAlgCat.of R S)
-
theoremdefined in Proetale/Algebra/IndZariski.leancontains sorry
theorem RingHom.IndZariski.iff_ind_indZariski.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : f.IndZariski ↔ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => RingHom.IndZariski).ind (CommRingCat.ofHom f)
theorem RingHom.IndZariski.iff_ind_indZariski.{u} {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : f.IndZariski ↔ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => RingHom.IndZariski).ind (CommRingCat.ofHom f)
Ind-Zariski is equivalent to ind-ind-Zariski.
Proof for Lemma 1.2.4
uses 0
This follows from general theory, because local isomorphisms are of finite presentation.
Lemma1.2.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.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
- 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
Used by 2
Associated Lean declarations
-
Algebra.IndZariski.prod[complete] -
RingHom.IndZariski.prod[complete] -
Algebra.IndZariski.pi[complete] -
RingHom.IndZariski.pi[complete]
A finite product of ind-Zariski algebras is ind-Zariski.
Lean code for Lemma1.2.5●4 theorems
Associated Lean declarations
-
Algebra.IndZariski.prod[complete]
-
RingHom.IndZariski.prod[complete]
-
Algebra.IndZariski.pi[complete]
-
RingHom.IndZariski.pi[complete]
Associated Lean declarations
-
Algebra.IndZariski.prod[complete] -
RingHom.IndZariski.prod[complete] -
Algebra.IndZariski.pi[complete] -
RingHom.IndZariski.pi[complete]
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem Algebra.IndZariski.prod.{u} (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra.IndZariski R S] [Algebra.IndZariski R T] : Algebra.IndZariski R (S × T)
theorem Algebra.IndZariski.prod.{u} (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra.IndZariski R S] [Algebra.IndZariski R T] : Algebra.IndZariski R (S × T)
The product of two ind-Zariski algebras is ind-Zariski.
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem RingHom.IndZariski.prod.{u} {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : R →+* T} (hf : f.IndZariski) (hg : g.IndZariski) : (f.prod g).IndZariski
theorem RingHom.IndZariski.prod.{u} {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : R →+* T} (hf : f.IndZariski) (hg : g.IndZariski) : (f.prod g).IndZariski
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem Algebra.IndZariski.pi.{u} (R : Type u) [CommRing R] {ι : Type u} [Finite ι] (S : ι → Type u) [(i : ι) → CommRing (S i)] [(i : ι) → Algebra R (S i)] [∀ (i : ι), Algebra.IndZariski R (S i)] : Algebra.IndZariski R ((i : ι) → S i)
theorem Algebra.IndZariski.pi.{u} (R : Type u) [CommRing R] {ι : Type u} [Finite ι] (S : ι → Type u) [(i : ι) → CommRing (S i)] [(i : ι) → Algebra R (S i)] [∀ (i : ι), Algebra.IndZariski R (S i)] : Algebra.IndZariski R ((i : ι) → S i)
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem RingHom.IndZariski.pi.{u} {R : Type u} [CommRing R] {ι : Type u} [Finite ι] (S : ι → Type u) [(i : ι) → CommRing (S i)] (f : (i : ι) → R →+* S i) (hf : ∀ (i : ι), (f i).IndZariski) : (Pi.ringHom f).IndZariski
theorem RingHom.IndZariski.pi.{u} {R : Type u} [CommRing R] {ι : Type u} [Finite ι] (S : ι → Type u) [(i : ι) → CommRing (S i)] (f : (i : ι) → R →+* S i) (hf : ∀ (i : ι), (f i).IndZariski) : (Pi.ringHom f).IndZariski
Proof for Lemma 1.2.5
uses 0
This is a consequence of the more general fact that if a property p of ring
maps is stable under finite products, then Ind-p is also stable under finite
products, since a finite product of filtered index categories is again filtered.
It suffices to show that being a local isomorphism is stable under finite
products. Suppose A \to B_i is a local isomorphism for each i for finitely
many i's. Every prime \q in \prod_i B_i is an extension prime ideal of
one of the factors, say B_0. Since there exists f_0 \in B_0,
f_0 \notin \q such that A \to (B_0)_{f_0} induces an open immersion,
localize \prod_i B_i at the corresponding idempotent times this element
f_0 to obtain the desired result.
Lemma1.2.6
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.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
- 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
Used by 2
Associated Lean declarations
-
Algebra.IndZariski.trans[sorry in proof] -
RingHom.IndZariski.comp[complete]
Let A \to B and B \to C be ind-Zariski ring maps. Then the composition
A \to C is also ind-Zariski.
Lean code for Lemma1.2.6●2 theorems, 1 incomplete
Associated Lean declarations
-
Algebra.IndZariski.trans[sorry in proof]
-
RingHom.IndZariski.comp[complete]
Associated Lean declarations
-
Algebra.IndZariski.trans[sorry in proof] -
RingHom.IndZariski.comp[complete]
-
theoremdefined in Proetale/Algebra/IndZariski.leancontains sorry
theorem Algebra.IndZariski.trans.{u} (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.IndZariski R S] [Algebra.IndZariski S T] : Algebra.IndZariski R T
theorem Algebra.IndZariski.trans.{u} (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.IndZariski R S] [Algebra.IndZariski S T] : Algebra.IndZariski R T
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem RingHom.IndZariski.comp.{u} {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T} (hg : g.IndZariski) (hf : f.IndZariski) : (g.comp f).IndZariski
theorem RingHom.IndZariski.comp.{u} {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T} (hg : g.IndZariski) (hf : f.IndZariski) : (g.comp f).IndZariski
Lemma1.2.7
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
- 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
- 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.IndZariski.of_isLocalization[complete]
Let A be a ring and S \subseteq A a multiplicative subset. Then
S^{-1}A is ind-Zariski over A.
Lean code for Lemma1.2.7●1 theorem
Associated Lean declarations
-
Algebra.IndZariski.of_isLocalization[complete]
Associated Lean declarations
-
Algebra.IndZariski.of_isLocalization[complete]
-
theoremdefined in Proetale/Algebra/IndZariski.leancomplete
theorem Algebra.IndZariski.of_isLocalization.{u} {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Algebra.IndZariski R S
theorem Algebra.IndZariski.of_isLocalization.{u} {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Algebra.IndZariski R S
Proof for Lemma 1.2.7
uses 0
S^{-1} A = \colim_{f \in S} A_f and A \to A_f is a local isomorphism.