8.3. The orbit dimension drop
Suppose \mathbb{G}_m acts freely on a quasi-affine variety X of finite
type and a morphism \pi : X \to Y is constant on each orbit. Then
\dim \pi(X) \le \dim X - 1.
(Zheng, 2026, Lemma 6.4)
Lean code for Lemma8.3.1●2 theorems
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Algebra/HomogeneousDenominatorContradiction.leancomplete
theorem RB31E2E.NullCellulePolynomial.homogeneousPrime_height_lt_of_irrelevant_mem_not_mem.{u_1} {k : Type u_1} [Field k] {n : ℕ} (P : Ideal (MvPolynomial (Fin n) k)) [P.IsPrime] (hPhom : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) k) P) (s : MvPolynomial (Fin n) k) (hsIrrelevant : s ∈ RB31E2E.NullCellulePolynomial.finiteIrrelevantIdeal n) (hsP : s ∉ P) : P.height < ↑n
theorem RB31E2E.NullCellulePolynomial.homogeneousPrime_height_lt_of_irrelevant_mem_not_mem.{u_1} {k : Type u_1} [Field k] {n : ℕ} (P : Ideal (MvPolynomial (Fin n) k)) [P.IsPrime] (hPhom : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) k) P) (s : MvPolynomial (Fin n) k) (hsIrrelevant : s ∈ RB31E2E.NullCellulePolynomial.finiteIrrelevantIdeal n) (hsP : s ∉ P) : P.height < ↑n
A homogeneous prime avoiding any specified member of the irrelevant ideal has height strictly below the number of ambient variables.
-
theoremdefined in RB31EndToEnd/Algebra/HomogeneousPrimeChartHeight.leancomplete
theorem RB31E2E.NullCellulePolynomial.finiteIrrelevantIdeal_height.{u_1} {k : Type u_1} [Field k] (n : ℕ) : (RB31E2E.NullCellulePolynomial.finiteIrrelevantIdeal n).height = ↑n
theorem RB31E2E.NullCellulePolynomial.finiteIrrelevantIdeal_height.{u_1} {k : Type u_1} [Field k] (n : ℕ) : (RB31E2E.NullCellulePolynomial.finiteIrrelevantIdeal n).height = ↑n
The height of the irrelevant ideal in `n` variables is exactly `n`. The lower bound is the explicit chain obtained by adjoining the variables one at a time. The upper bound uses that the ideal is generated by the `n` coordinate variables.
The paper proves this from the fibre-dimension theorem: the group is
connected, so it preserves each irreducible component, and every
one-dimensional orbit lies in a fibre of \pi. The formalization proves no
statement of this shape, and the register has the entry. The point-set
content (the common-scaling action is free on every grounded nonzero
assignment, units_commonScale_injective_of_ne_zero)
is proved in a module whose own comment defers the conversion into a
dimension inequality, and nothing reachable from the root theorem uses it.
What stands in for the orbit drop is homogeneity. The compatibility
equations are homogeneous in the twist variables, so the bad locus of a
fixed partition is a homogeneous ideal in the twist coordinates over the pin
coefficients, and a homogeneous prime avoiding any element of the irrelevant
ideal — here a distinctness denominator, a product of twist-difference
coordinates and so of positive degree — has height strictly below the
number of twist variables, by
homogeneousPrime_height_lt_of_irrelevant_mem_not_mem
together with the computation of the irrelevant ideal's height in
finiteIrrelevantIdeal_height.
The strict inequality is the paper's -1.