2.2. Weak dimension
Currently, mathlib does not have \mathrm{Tor} so we give a non-standard, but
equivalent definition which suffices for our purposes.
- 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
- 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
- Theorem 2.6.1
-
Ring.WeakDimensionLEOne[complete]
Let A be a ring. We say it is of weak dimension \le 1 if every finitely
generated ideal of A is flat over A.
Lean code for Definition2.2.1●1 definition
Associated Lean declarations
-
Ring.WeakDimensionLEOne[complete]
-
Ring.WeakDimensionLEOne[complete]
-
classdefined in Proetale/Algebra/WeakDimension.leancomplete
class Ring.WeakDimensionLEOne.{u_1} (R : Type u_1) [CommRing R] : Prop
class Ring.WeakDimensionLEOne.{u_1} (R : Type u_1) [CommRing R] : Prop
A ring `R` is of weak dimension `≤ 1` if any finitely generated ideal is flat.
Methods
flat_of_fg : ∀ (I : Ideal R), I.FG → Module.Flat R ↥I
- 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
- 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
- Theorem 2.6.1
-
Ring.WeakDimensionLEOne.flat_submodule[complete]
Let A be a ring of weak dimension \le 1 and M a flat A-module.
Then any submodule of M is flat.
(Stacks Project, Tag 092S, (2) ⟹ (4))
Lean code for Lemma2.2.2●1 theorem
Associated Lean declarations
-
Ring.WeakDimensionLEOne.flat_submodule[complete]
-
Ring.WeakDimensionLEOne.flat_submodule[complete]
-
theoremdefined in Proetale/Algebra/WeakDimension.leancomplete
theorem Ring.WeakDimensionLEOne.flat_submodule.{u_1, u_3} (R : Type u_1) [CommRing R] [Ring.WeakDimensionLEOne R] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) [Module.Flat R M] : Module.Flat R ↥N
theorem Ring.WeakDimensionLEOne.flat_submodule.{u_1, u_3} (R : Type u_1) [CommRing R] [Ring.WeakDimensionLEOne R] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) [Module.Flat R M] : Module.Flat R ↥N
If `R` is of weak dimension `≤ 1`, then any submodule of a flat module is flat.
Let N \subseteq M be a submodule. It suffices to show that for any finitely
generated ideal I, the linear map I \otimes_{A} N \to N is injective. For
this, consider the commutative diagram
\begin{CD} I \otimes_{A} N @>>> N \\ @VVV @VVV \\ I \otimes_{A} M @>>> M \end{CD}
The left vertical map is injective, because I is flat by assumption on
A. The bottom horizontal map is injective, because M is flat. Hence
I \otimes_{A} N \to N \to M is injective, from which the claim 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
- 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
- Theorem 2.6.1
-
Ring.WeakDimensionLEOne.flat_ideal[complete]
If A is of weak dimension \le 1, then every ideal I \subseteq A is
flat.
(Stacks Project, Tag 092S, (1) ⟹ (2))
Lean code for Corollary2.2.3●1 theorem
Associated Lean declarations
-
Ring.WeakDimensionLEOne.flat_ideal[complete]
-
Ring.WeakDimensionLEOne.flat_ideal[complete]
-
theoremdefined in Proetale/Algebra/WeakDimension.leancomplete
theorem Ring.WeakDimensionLEOne.flat_ideal.{u_1} (R : Type u_1) [CommRing R] [Ring.WeakDimensionLEOne R] (I : Ideal R) : Module.Flat R ↥I
theorem Ring.WeakDimensionLEOne.flat_ideal.{u_1} (R : Type u_1) [CommRing R] [Ring.WeakDimensionLEOne R] (I : Ideal R) : Module.Flat R ↥I
Immediate consequence of Lemma 2.2.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.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
- Theorem 2.6.1
-
Ring.WeakDimensionLEOne.of_weaklyEtale[complete]
Let A be of weak dimension \le 1 and B a weakly étale A-algebra.
Then B is of weak dimension \le 1.
(Stacks Project, Tag 092E)
Lean code for Lemma2.2.4●1 theorem
Associated Lean declarations
-
Ring.WeakDimensionLEOne.of_weaklyEtale[complete]
-
Ring.WeakDimensionLEOne.of_weaklyEtale[complete]
-
theoremdefined in Proetale/Algebra/WeakDimension.leancomplete
theorem Ring.WeakDimensionLEOne.of_weaklyEtale.{u_1, u_2} (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Ring.WeakDimensionLEOne R] [Algebra.WeaklyEtale R S] : Ring.WeakDimensionLEOne S
theorem Ring.WeakDimensionLEOne.of_weaklyEtale.{u_1, u_2} (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Ring.WeakDimensionLEOne R] [Algebra.WeaklyEtale R S] : Ring.WeakDimensionLEOne S
If `R` is of weak dimension `≤ 1` and `S` is weakly étale over `R`, then the same holds for `S`.
Let M be a flat B-module and N \subseteq M a submodule. By
Lemma 2.1.8 it suffices to show that N is A-flat.
Since B is A-flat, M is also A-flat and hence its submodule N is
A-flat by Lemma 2.2.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.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
- Theorem 2.6.1
-
Submodule.FG.mem_pi[complete]
Let (A_i)_{i \in I} be a family of rings and for every i an
A_i-module M_i. Let N be a \prod_{i \in I} A_i-submodule of
\prod_{i \in I} M_i and let N_i be the image of N in M_i. Then
N \subseteq \prod_{i \in I} N_i. If N is finitely generated, equality
holds.
Lean code for Lemma2.2.5●1 theorem
Associated Lean declarations
-
Submodule.FG.mem_pi[complete]
-
Submodule.FG.mem_pi[complete]
-
theoremdefined in Proetale/Algebra/WeakDimension.leancomplete
theorem Submodule.FG.mem_pi.{u_1, u_2, u_3} {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → Semiring (A i)] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module (A i) (M i)] {N : Submodule ((i : ι) → A i) ((i : ι) → M i)} (hN : N.FG) {y : (i : ι) → M i} (hy : ∀ (i : ι), ∃ z ∈ N, z i = y i) : y ∈ N
theorem Submodule.FG.mem_pi.{u_1, u_2, u_3} {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → Semiring (A i)] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module (A i) (M i)] {N : Submodule ((i : ι) → A i) ((i : ι) → M i)} (hN : N.FG) {y : (i : ι) → M i} (hy : ∀ (i : ι), ∃ z ∈ N, z i = y i) : y ∈ N
A finitely generated `Π i, A i`-submodule `N` of a product `Π i, M i` is the product of its componentwise images: if every component `y i` of `y` lies in the image of `N` under the `i`-th projection, then `y ∈ N`.
- 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.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
- Theorem 2.6.1
Let (A_i)_{i \in I} be a family of valuation rings. Then
\prod_{i \in I} A_i is of weak dimension \le 1.
(Stacks Project, Tag 092T)
Lean code for Lemma2.2.6●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/WeakDimension.leancomplete
theorem Ring.WeakDimensionLEOne.pi_of_isValuationRing.{u_3, u_4} {ι : Type u_3} (R : ι → Type u_4) [(i : ι) → CommRing (R i)] [∀ (i : ι), IsDomain (R i)] [∀ (i : ι), ValuationRing (R i)] : Ring.WeakDimensionLEOne ((i : ι) → R i)
theorem Ring.WeakDimensionLEOne.pi_of_isValuationRing.{u_3, u_4} {ι : Type u_3} (R : ι → Type u_4) [(i : ι) → CommRing (R i)] [∀ (i : ι), IsDomain (R i)] [∀ (i : ι), ValuationRing (R i)] : Ring.WeakDimensionLEOne ((i : ι) → R i)
The product of valuation rings is of weak dimension `≤ 1`.
Let I \subseteq \prod_{i \in I} A_i be a finitely generated ideal. Let
I_i \subseteq A_i be the image of I in A_i. By
Lemma 2.2.5, I is the product of the I_i. Since
each A_i is a valuation ring, there exists f_i \in A_i such that
I_i = (f_i). Hence I = (f) where f = (f_i). Let e \in A be the
idempotent element defined by
e_i = \begin{cases} 0 & f_i = 0 \\ 1 & f_i \neq 0 \end{cases}
and let g be the element defined by
g_i = \begin{cases} 1 & f_i = 0 \\ f_i & f_i \neq 0 \end{cases}.
Since every A_i is a domain, g is a non-zerodivisor and f = g e. In
particular, the A-linear map (e) \to (ge) = (f) is an isomorphism: It is
surjective by construction and injective because g is a nonzerodivisor.
Since e is idempotent, we have A = (e) \oplus (1 - e) as A-modules, so
(e) is projective.
- 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.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
- Theorem 2.6.1
Let A be of weak dimension \le 1. Let B be a flat A-algebra such
that A \to B is injective and an epimorphism of rings. Then A is
integrally closed in B.
(Stacks Project, Tag 092V)
Lean code for Lemma2.2.7●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/WeakDimension.leancomplete
theorem Ring.WeakDimensionLEOne.isIntegrallyClosedIn_of_isEpi.{u_1, u_2} (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Ring.WeakDimensionLEOne R] [Module.Flat R S] [FaithfulSMul R S] [Algebra.IsEpi R S] : IsIntegrallyClosedIn R S
theorem Ring.WeakDimensionLEOne.isIntegrallyClosedIn_of_isEpi.{u_1, u_2} (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Ring.WeakDimensionLEOne R] [Module.Flat R S] [FaithfulSMul R S] [Algebra.IsEpi R S] : IsIntegrallyClosedIn R S
If `R` is of weak dimension `≤ 1`, it is integrally closed in any flat extension `S` such that `R → S` is an epi.
Let x \in B be integral over A and A' = A[x]. The map A \to A' is
injective and finite, so to show A = A' it suffices to check that
A \to A' is an epimorphism. By Lemma 2.2.2,
A' is flat over A. Hence the composition
A' \otimes_{A} A' \to B \otimes_{A} B \to B
is injective.
- 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.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
- Theorem 2.6.1
- No associated Lean code or declarations.
Let A be a domain and L an algebraic extension of \mathrm{Frac}(A).
If A is integrally closed in L, then there exists a cartesian diagram of
rings
\begin{CD} A @>>> L \\ @VVV @VVV \\ S @>>> T \end{CD}
with S of weak dimension \le 1 and S \to T a flat, injective
epimorphism of rings.
(Stacks Project, Tag 092U)
TBA.
- 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.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
- Theorem 2.6.1
- No associated Lean code or declarations.
Let A be a domain and B a weakly étale A-algebra. Let L be an
algebraic extension of \mathrm{Frac}(A) and assume that A is integrally
closed in L. Then B is integrally closed in B \otimes_{A} L.
(Stacks Project, Tag 092W)
TBA.