noncomputable def
mvPolynomialTensorAlgEquiv
(k : Type u_1)
[CommRing k]
(n m : ℕ)
:
TensorProduct k (MvPolynomial (Fin n) k) (MvPolynomial (Fin m) k) ≃ₐ[k] MvPolynomial (Fin (n + m)) k
The standard algebra isomorphism
k[x₁,…,xₙ] ⊗_k k[y₁,…,yₘ] ≃ k[x₁,…,xₙ, y₁,…,yₘ].
Instances For
Computation dim(k[x]_n ⊗_k k[x]_m) = n + m, reflecting A^n × A^m = A^{n+m}.
theorem
ringKrullDim_tensorProduct_mvPolynomial_eq_add
(k : Type u_1)
[Field k]
(n m : ℕ)
:
ringKrullDim (TensorProduct k (MvPolynomial (Fin n) k) (MvPolynomial (Fin m) k)) = ringKrullDim (MvPolynomial (Fin n) k) + ringKrullDim (MvPolynomial (Fin m) k)
Krull dimension is additive on tensor products of polynomial algebras:
dim(A^n ⊗ A^m) = dim A^n + dim A^m.
theorem
ringKrullDim_eq_of_noetherNormalization
{k : Type u_1}
[Field k]
{R : Type u_2}
[CommRing R]
[Algebra k R]
(s : ℕ)
(g : MvPolynomial (Fin s) k →ₐ[k] R)
(hinj : Function.Injective ⇑g)
(hfin : g.Finite)
:
If R admits a Noether normalization, i.e. an injective finite k-algebra map
k[x₁,…,x_s] → R, then dim R = s.
theorem
ringKrullDim_fg_algebra_eq_nat
(k : Type u_1)
[Field k]
(R : Type u_2)
[CommRing R]
[Nontrivial R]
[Algebra k R]
[Algebra.FiniteType k R]
:
∃ (s : ℕ), ringKrullDim R = ↑s
A nontrivial finitely generated k-algebra has finite Krull dimension equal to some
natural number.
theorem
Algebra.TensorProduct.map_injective_of_field
{k : Type u_1}
[Field k]
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
{D : Type u_5}
[CommRing A]
[CommRing B]
[CommRing C]
[CommRing D]
[Algebra k A]
[Algebra k B]
[Algebra k C]
[Algebra k D]
(f : A →ₐ[k] C)
(g : B →ₐ[k] D)
(hf : Function.Injective ⇑f)
(hg : Function.Injective ⇑g)
:
Function.Injective ⇑(map f g)
Helper: the tensor product of two injective k-algebra maps is injective (using that
every module over a field is flat).
theorem
ringKrullDim_tensorProduct_fg_algebra
(k : Type u_1)
[Field k]
(A : Type u_2)
(B : Type u_3)
[CommRing A]
[CommRing B]
[Algebra k A]
[Algebra k B]
[Algebra.FiniteType k A]
[Algebra.FiniteType k B]
[Nontrivial A]
[Nontrivial B]
[Nontrivial (TensorProduct k A B)]
:
Theorem 7.1: For finitely generated k-algebras A and B,
dim(A ⊗_k B) = dim A + dim B, i.e. dim(X × Y) = dim X + dim Y.