Krull dimension of polynomial ring

We show that not all commutative rings R satisfy ringKrullDim R[X] = ringKrullDim R + 1, following the construction in the reference link.

We define the commutative ring A as {f ∈ k(t)⟦Y⟧ | f(0) ∈ k} for a field $k$, and show that ringKrullDim A = 1 but ringKrullDim A[X] = 3.

References

https://math.stackexchange.com/questions/1267419/examples-of-rings-whose-polynomial-rings-have-large-dimension

@[reducible, inline]

noncomputable abbrev Counterexample.DimensionPolynomial.A (k : Type u_1) [Field k] : Subring (PowerSeries (RatFunc k))

We define the commutative ring A as {f ∈ k(t)⟦Y⟧ | f(0) ∈ k} for a field k.

Equations

• Counterexample.DimensionPolynomial.A k = Subring.comap PowerSeries.constantCoeff RatFunc.C.range

theorem Counterexample.DimensionPolynomial.ringKrullDim_A_eq_one (k : Type u_1) [Field k] : ringKrullDim ↥(A k) = 1

theorem Counterexample.DimensionPolynomial.ringKrullDim_polynomial_A_eq_three (k : Type u_1) [Field k] : ringKrullDim (Polynomial ↥(A k)) = 3