Ambient order on root sections over connected open bases

The local discriminant-order theorem gives local constancy of ambient polynomial order along a continuous root section. On a preconnected open base, that local result gives a single constant order on the whole section. This global form is useful when assembling local McCallum lifting data over connected base regions.

theorem Polynomial.orderAt_root_eq_of_orderAt_discr_eq {n : ℕ} {ι : Type u_1} [Fintype ι] {p : Polynomial (MvPolynomial (Fin n) ℝ)} {φ : (ι → ℝ) → Fin n → ℝ} {θ : (ι → ℝ) → ℝ} {U : Set (ι → ℝ)} {m : ℕ} (hU : IsOpen U) (hconn : IsPreconnected U) (hφ : AnalyticOnNhd ℝ φ U) (hp : ∀ x ∈ U, map (MvPolynomial.eval (φ x)) p ≠ 0) (hm : ∀ x ∈ U, p.discr.orderAt (φ x) = ↑m) (hθ : ContinuousOn θ U) (hroot : ∀ x ∈ U, (map (MvPolynomial.eval (φ x)) p).IsRoot (θ x)) {x y : ι → ℝ} (hx : x ∈ U) (hy : y ∈ U) : ((MvPolynomial.finSuccEquiv ℝ n).symm p).orderAt (Fin.cons (θ x) (φ x)) = ((MvPolynomial.finSuccEquiv ℝ n).symm p).orderAt (Fin.cons (θ y) (φ y))

Ambient order is constant on a root section. Let a polynomial family have nonzero fibers and discriminant of constant finite ambient order along a real analytic map on an open preconnected set. Every continuous section consisting of roots then has constant ambient order there. The formal leading coefficient may vanish, so the fiber degree may drop.