def IsCatenary (α : Type u_1) [Preorder α] : Prop

A preorder is catenary when any two unrefinable (covering) chains with the same endpoints have the same length.

def IsRingCatenary (R : Type u_1) [CommRing R] : Prop

A commutative ring is catenary when its prime spectrum is catenary as a preorder.

theorem algebraicVariety_isCatenary (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [Algebra k R] [Algebra.FiniteType k R] : IsCatenary (PrimeSpectrum R)

Any finitely generated k-algebra (in particular, any coordinate ring of an algebraic variety) has a catenary prime spectrum (Prop 10, Lec 8).

theorem finiteType_isRingCatenary (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [Algebra k R] [Algebra.FiniteType k R] : IsRingCatenary R

A finitely generated k-algebra is a catenary ring.

theorem MvPolynomial_isRingCatenary (k : Type u_1) [Field k] (n : ℕ) : IsRingCatenary (MvPolynomial (Fin n) k)

The multivariate polynomial ring k[x₁, …, xₙ] is a catenary ring.

theorem Polynomial_isRingCatenary (k : Type u_1) [Field k] : IsRingCatenary (Polynomial k)

The univariate polynomial ring k[x] is a catenary ring.

theorem algebraicVariety_catenary_chain (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [Algebra k R] [Algebra.FiniteType k R] {n : ℕ} (Z : Fin (n + 1) → TopologicalSpace.IrreducibleCloseds (PrimeSpectrum R)) (hcov : ∀ (i : Fin n), Z i.castSucc ⋖ Z i.succ) (hmin : IsMin (Z 0)) (hmax : IsMax (Z (Fin.last n))) (i : Fin (n + 1)) : topologicalKrullDim ↥(Z i) = ↑↑i

In an unrefinable chain of closed irreducibles X = Zₙ ⊋ … ⊋ Z₀ on an algebraic variety, each Z_i has dimension i (Prop 10, Lec 8).

theorem catenary_chain_dim_zero (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [Algebra k R] [Algebra.FiniteType k R] {n : ℕ} (Z : Fin (n + 1) → TopologicalSpace.IrreducibleCloseds (PrimeSpectrum R)) (hcov : ∀ (i : Fin n), Z i.castSucc ⋖ Z i.succ) (hmin : IsMin (Z 0)) (hmax : IsMax (Z (Fin.last n))) : topologicalKrullDim ↥(Z 0) = 0

The bottom element Z₀ of an unrefinable chain of closed irreducibles is zero-dimensional.

theorem catenary_chain_dim_top (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [Algebra k R] [Algebra.FiniteType k R] {n : ℕ} (Z : Fin (n + 1) → TopologicalSpace.IrreducibleCloseds (PrimeSpectrum R)) (hcov : ∀ (i : Fin n), Z i.castSucc ⋖ Z i.succ) (hmin : IsMin (Z 0)) (hmax : IsMax (Z (Fin.last n))) : topologicalKrullDim ↥(Z (Fin.last n)) = ↑n

The top element Zₙ of an unrefinable chain of closed irreducibles has dimension n.

theorem catenary_chain_dim_step (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [Algebra k R] [Algebra.FiniteType k R] {n : ℕ} (Z : Fin (n + 1) → TopologicalSpace.IrreducibleCloseds (PrimeSpectrum R)) (hcov : ∀ (i : Fin n), Z i.castSucc ⋖ Z i.succ) (hmin : IsMin (Z 0)) (hmax : IsMax (Z (Fin.last n))) (i : Fin n) : topologicalKrullDim ↥(Z i.succ) = topologicalKrullDim ↥(Z i.castSucc) + 1

Each step in an unrefinable chain of closed irreducibles increments the dimension by one.