Body-Pin Rigidity

7.4. The dimension formula🔗

Lemma7.4.1
Group: The paper's algebraic argument: the form, the ideal, the shear, the dimension formula, and the height theorem. (5)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 0used by 1✓L∃∀N
Tagspaper

Let A = k[x_1, \dots, x_N] and let P \subset A be a prime ideal. Then \operatorname{ht} P + \trdeg_k \operatorname{Frac}(A/P) = N. (Zheng, 2026, Lemma 5.3)

Lean code for Lemma7.4.1●1 theorem
  • theoremdefined in RB31EndToEnd/Algebra/PolynomialPrimeTrdegHeight.lean
    complete
    theorem RB31E2E.PolynomialPrimeTrdegHeight.polynomialPrime_height_add_fractionTrdeg_eq_natCard.{u_1,
    u_2}
  {k : Type u_1} {ι : Type u_2} [Field k] [Finite ι]
  (P : Ideal (MvPolynomial ι k)) [P.IsPrime] :
  P.height +
      ↑(Cardinal.toNat
          (Algebra.trdeg k (FractionRing (MvPolynomial ι k ⧸ P)))) =
    ↑(Nat.card ι)
    theorem RB31E2E.PolynomialPrimeTrdegHeight.polynomialPrime_height_add_fractionTrdeg_eq_natCard.{u_1,
    u_2}
  {k : Type u_1} {ι : Type u_2} [Field k]
  [Finite ι]
  (P : Ideal (MvPolynomial ι k))
  [P.IsPrime] :
  P.height +
      ↑(Cardinal.toNat
          (Algebra.trdeg k
            (FractionRing
              (MvPolynomial ι k ⧸ P)))) =
    ↑(Nat.card ι)
    The affine dimension formula for an arbitrary prime of a polynomial ring
in finitely many variables over a field.  The transcendence degree is taken
in the quotient function field; `Cardinal.toNat` is harmless here because a
coordinate transcendence basis is finite.

The paper's proof is a citation, to the dimension theory of Eisenbud (1995) via Noether normalization. The formalization proves the formula from scratch, since Mathlib does not currently carry it: a transcendence basis is extracted from the coordinates themselves, the height of a maximal ideal is computed from the Jacobson property of finite polynomial rings, and no catenarity assumption enters. The companion lemmas of FiniteCoordinateTrdeg give the coordinate-generation bound \trdeg_k K \le 3|V| that the semismallness statements of the flags chapter are phrased with.