Coordinate germs are prime #
Restriction to the hyperplane {x_k = 0} is a ring homomorphism resAt k from series in n + 1
variables to series in n variables (a coordinate swap, Mathlib's finSuccEquiv, and the
constant coefficient in the split-off variable), and resAt k f = 0 exactly when every monomial
of f free of x_k has zero coefficient (x_k ∣ f, Mathlib's X_dvd_iff). The target is a
domain, so x_k ∣ F G forces x_k ∣ F or x_k ∣ G, with convergent quotients by divX.
Hence x_k, which is not a unit (not_isUnit_convX), is prime in Conv K n. Not in the sources
as such: Bierstone and Milman use the local ring of germs as a domain in which the coordinates
are prime without comment [BM88, proof of Theorem 4.4, pp. 24–25].
The coefficient field K is ℝ or ℂ ([RCLike K]).
theorem
Analytic.coeff_resAt
{K : Type u_1}
[RCLike K]
{n : ℕ}
(k : Fin (n + 1))
(f : MvPowerSeries (Fin (n + 1)) K)
(x : Fin n →₀ ℕ)
:
(MvPowerSeries.coeff x) ((resAt K k) f) = (MvPowerSeries.coeff (Finsupp.embDomain (swapEmb k) (Finsupp.cons 0 x))) f