Weierstrass preparation and division in holomorphic stalks #
Let E be a complex normed space, xβ : E, and wβ : β. Write πͺ_{E, xβ} and
πͺ_{E Γ β, (xβ, wβ)} for the stalks of holomorphicStructureSheaf at xβ and (xβ, wβ). This
file connects the local analytic Weierstrass preparation and division theorems on E Γ β
(AnalyticAt.exists_weierstrassPreparation, AnalyticAt.exists_weierstrassDivision) with
Mathlib's formal power series Weierstrass API (PowerSeries.IsWeierstrassFactorization,
PowerSeries.IsWeierstrassDivision) and deduces uniqueness, polynomial divisibility reflection,
polynomial quotient isomorphisms, and flatness and finiteness of local hypersurface quotients over
the base stalk. The uniqueness statements are also restated for functions rather than germs.
Main definitions #
TauCeti.holomorphicStructureSheaf.evalVertical: evaluates a polynomial overπͺ_{E, xβ}as a holomorphic germ at(xβ, wβ)by pulling coefficients back alongProd.fstand substituting the centered vertical coordinate germp β¦ p.2 - wβ.TauCeti.holomorphicStructureSheaf.verticalPowerSeries: expands a holomorphic germ at(xβ, wβ)as a formal power series overπͺ_{E, xβ}inw - wβvia iterated vertical derivatives.TauCeti.holomorphicStructureSheaf.quotientEquivOfIsDistinguishedAt: for[FiniteDimensional β E]and a distinguished polynomialP β (πͺ_{E, xβ})[X], the canonical ring isomorphism(πͺ_{E, xβ})[X] β§Έ Ideal.span {P} β+* πͺ_{E Γ β, (xβ, wβ)} β§Έ Ideal.span {evalVertical xβ wβ P}.TauCeti.holomorphicStructureSheaf.weierstrassQuotientEquiv: the induced ring isomorphism(πͺ_{E, xβ})[X] β§Έ Ideal.span {P} β+* πͺ_{E Γ β, (xβ, wβ)} β§Έ Ideal.span {f}for a Weierstrass factorizationf = evalVertical xβ wβ P * u.
Main results #
TauCeti.holomorphicStructureSheaf.verticalPowerSeries_injective: vertical Taylor expansion is injective (with no finite-dimensionality assumption onE).TauCeti.holomorphicStructureSheaf.order_map_residue_verticalPowerSeries: the formal order of the residue-field reduction ofverticalPowerSeries xβ wβ gequals the analytic order of the vertical slicew β¦ G (xβ, w)atwβ.TauCeti.holomorphicStructureSheaf.isWeierstrassFactorization_verticalPowerSeries_iff,TauCeti.holomorphicStructureSheaf.isWeierstrassDivision_verticalPowerSeries_iff: alignment of holomorphic germ factorizations and divisions withPowerSeries.IsWeierstrassFactorizationandPowerSeries.IsWeierstrassDivision.TauCeti.holomorphicStructureSheaf.weierstrassPreparation_unique,TauCeti.holomorphicStructureSheaf.weierstrassDivision_unique: uniqueness of Weierstrass preparation and division inπͺ_{E Γ β, (xβ, wβ)}(withoutFiniteDimensional β E, deduced from maximal-ideal Hausdorffness viaPowerSeries.IsWeierstrassFactorization.elimandPowerSeries.IsWeierstrassDivision.elim).TauCeti.eventuallyEq_of_weierstrassPreparation,TauCeti.eventuallyEq_of_weierstrassDivision: the same uniqueness for functions, stated without stalks: two Weierstrass preparations of a holomorphic function near(xβ, wβ)have the same coefficient and unit germs, and two divisions by the same Weierstrass polynomial have the same quotient and remainder germs. They are deduced fromweierstrassPreparation_uniqueandweierstrassDivision_unique_of_isDistinguishedAt.TauCeti.holomorphicStructureSheaf.evalVertical_dvd_iff_of_isDistinguishedAt: divisibility by a distinguished polynomialPin(πͺ_{E, xβ})[X]agrees with divisibility byevalVertical xβ wβ Pinπͺ_{E Γ β, (xβ, wβ)}.TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassPreparation,TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassPreparation_of_analyticOrderAt,TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassDivision_of_isDistinguishedAt,TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassDivision: existence and uniqueness of Weierstrass preparation and division on finite-dimensional holomorphic stalks.TauCeti.holomorphicStructureSheaf.flat_quotientMk_comp_stalkPrecomp_fst,TauCeti.holomorphicStructureSheaf.finite_quotientMk_comp_stalkPrecomp_fst: any hypersurface germ whose vertical slice does not vanish identically defines a flat and finite algebra over the base stalkπͺ_{E, xβ}.
Attribution #
The alignment with formal power series and polynomial quotient comparison builds on Jz Pan's
formalization of formal Weierstrass preparation and division
(Mathlib.RingTheory.PowerSeries.WeierstrassPreparation), in particular its IsHausdorff
uniqueness theorems and Polynomial.IsDistinguishedAt.algEquivQuotient.
References #
- L. HΓΆrmander, An Introduction to Complex Analysis in Several Variables, Β§6.1.
- H. Grauert, R. Remmert, Coherent Analytic Sheaves, Ch. 2, Β§1.
- R. C. Gunning, H. Rossi, Analytic Functions of Several Complex Variables, Ch. II, Β§B.
Vertical polynomial evaluation #
Evaluates a polynomial over (holomorphicStructureSheaf π(β, E) E).presheaf.stalk xβ as a
holomorphic germ on E Γ β at (xβ, wβ), pulling coefficients back along Prod.fst and
sending X to the centered vertical coordinate germ p β¦ p.2 - wβ.
Instances For
Evaluating evalVertical xβ wβ P at (xβ, wβ) evaluates the constant term of P at xβ.
If C i represents c i near xβ, then (x, w) β¦ β i, C i x * (w - wβ) ^ i represents
evalVertical xβ wβ (β i, monomial i (c i)) near (xβ, wβ).
If C i represents c i near xβ, then (x, w) β¦ (monicOfCoeff (C Β· x)).eval (w - wβ)
represents evalVertical xβ wβ (monicOfCoeff c) near (xβ, wβ).
A monic polynomial monicOfCoeff c over πͺ_{E, xβ} is distinguished at the maximal ideal if
and only if all lower coefficient germs c i vanish at xβ.
Vertical Taylor expansion #
Expands a holomorphic germ at (xβ, wβ) on E Γ β as a formal power series in w - wβ over
the base stalk (holomorphicStructureSheaf π(β, E) E).presheaf.stalk xβ, sending g to
β n, ((n!)β»ΒΉ Β· β_w^n g(Β·, wβ)) X ^ n.
Instances For
If G represents g near (xβ, wβ), then x β¦ (n!)β»ΒΉ * iteratedDeriv n (G (x, Β·)) wβ
represents the n-th coefficient of verticalPowerSeries xβ wβ g near xβ.
Evaluating the constant coefficient of verticalPowerSeries xβ wβ g at xβ recovers the
value of g at (xβ, wβ).
Pulling a base germ back along Prod.fst sends it to a constant vertical power series.
The vertical power series of evalVertical xβ wβ P is P viewed as a power series.
Vertical Taylor expansion at (xβ, wβ) is injective (without assuming finite-dimensionality
of E).
Polynomial evaluation evalVertical xβ wβ is injective.
A holomorphic germ is a unit if and only if its vertical power series is a unit.
The formal order of the residue-field reduction of verticalPowerSeries xβ wβ g equals the
analytic order of the vertical slice w β¦ G (xβ, w) at wβ for any representative G of g.
The residue-field reduction of verticalPowerSeries xβ wβ g is nonzero if and only if the
vertical slice w β¦ G (xβ, w) has finite analytic order at wβ.
Alignment with PowerSeries and uniqueness #
A holomorphic germ factorization g = evalVertical xβ wβ P * u is a Weierstrass factorization
in the formal power series sense if and only if P is distinguished at the maximal ideal of
πͺ_{E, xβ} and u is a unit of πͺ_{E Γ β, (xβ, wβ)}.
A holomorphic germ division g = f * q + evalVertical xβ wβ r is a Weierstrass division in the
formal power series sense if and only if r has degree strictly less than the residue-field order
of verticalPowerSeries xβ wβ f.
Uniqueness of Weierstrass preparation in holomorphic stalks (without assuming
finite-dimensionality of E).
Uniqueness of Weierstrass division in holomorphic stalks (without assuming
finite-dimensionality of E).
For a distinguished polynomial P over πͺ_{E, xβ}, the residue-field reduction of
verticalPowerSeries xβ wβ (evalVertical xβ wβ P) has formal order P.natDegree.
For a distinguished polynomial P over πͺ_{E, xβ}, the residue-field reduction of
verticalPowerSeries xβ wβ (evalVertical xβ wβ P) is nonzero.
Uniqueness of Weierstrass division by evalVertical xβ wβ P for a distinguished polynomial
P (without assuming finite-dimensionality of E).
A distinguished polynomial P over πͺ_{E, xβ} divides a polynomial Q in (πͺ_{E, xβ})[X]
if and only if evalVertical xβ wβ P divides evalVertical xβ wβ Q in πͺ_{E Γ β, (xβ, wβ)}
(without assuming finite-dimensionality of E).
Existence, uniqueness, quotients, and flatness in finite dimension #
Weierstrass preparation in holomorphic stalks (explicit degree form). When a representative
F of f has vertical slice w β¦ F (xβ, w) of analytic order d at wβ, there exist unique
coefficient germs c : Fin d β πͺ_{E, xβ} vanishing at xβ and unit germ u β πͺ_{E Γ β, (xβ, wβ)}
such that f = evalVertical xβ wβ (monicOfCoeff c) * u.
Weierstrass preparation theorem in holomorphic stalks. Every holomorphic germ f at
(xβ, wβ) whose vertical power series has nonzero image in (πͺ_{E, xβ} β§Έ πͺ_{xβ})β¦Xβ§ admits a
unique factorization f = evalVertical xβ wβ P * u into a distinguished polynomial P over
πͺ_{E, xβ} and a unit germ u at (xβ, wβ).
Weierstrass division by a distinguished polynomial in holomorphic stalks. Given a
distinguished polynomial P over πͺ_{E, xβ} and any germ g at (xβ, wβ), there exist unique
q β πͺ_{E Γ β, (xβ, wβ)} and r β (πͺ_{E, xβ})[X] of degree < P.natDegree such that
g = evalVertical xβ wβ P * q + evalVertical xβ wβ r.
Weierstrass division theorem in holomorphic stalks. Given germs f and g at (xβ, wβ)
such that the vertical power series of f has nonzero image in (πͺ_{E, xβ} β§Έ πͺ_{xβ})β¦Xβ§, there
exist unique q β πͺ_{E Γ β, (xβ, wβ)} and r β (πͺ_{E, xβ})[X] forming a Weierstrass division of
g by f.
Polynomial quotient isomorphism, flatness, and finiteness #
For a distinguished polynomial P over πͺ_{E, xβ}, evaluating polynomials vertically induces
a canonical ring isomorphism (πͺ_{E, xβ})[X] β§Έ (P) β+* πͺ_{E Γ β, (xβ, wβ)} β§Έ (evalVertical P).
Instances For
If g = evalVertical xβ wβ P * q + evalVertical xβ wβ r, then the inverse of
quotientEquivOfIsDistinguishedAt maps the residue class of g to the residue class of r.
Composing quotientEquivOfIsDistinguishedAt with the canonical πͺ_{E, xβ}-algebra map into
(πͺ_{E, xβ})[X] β§Έ (P) recovers pullback along Prod.fst followed by the quotient map.
For a Weierstrass factorization f = evalVertical xβ wβ P * u, evaluating polynomials
vertically induces a canonical ring isomorphism
(πͺ_{E, xβ})[X] β§Έ (P) β+* πͺ_{E Γ β, (xβ, wβ)} β§Έ (f).
Instances For
If f = evalVertical xβ wβ P * u is a Weierstrass factorization and
g = f * q + evalVertical xβ wβ r, then the inverse of weierstrassQuotientEquiv maps the residue
class of g to the residue class of r.
Composing weierstrassQuotientEquiv with the canonical πͺ_{E, xβ}-algebra map into
(πͺ_{E, xβ})[X] β§Έ (P) recovers pullback along Prod.fst followed by the quotient map modulo
f.
Pullback along Prod.fst makes the local quotient πͺ_{E Γ β, (xβ, wβ)} β§Έ (evalVertical P)
flat over the base stalk πͺ_{E, xβ} for every distinguished polynomial P.
Pullback along Prod.fst makes the local quotient πͺ_{E Γ β, (xβ, wβ)} β§Έ (evalVertical P)
finite over the base stalk πͺ_{E, xβ} for every distinguished polynomial P.
Local hypersurface flatness via Weierstrass preparation. If f β πͺ_{E Γ β, (xβ, wβ)} has
vertical power series with nonzero residue-field reduction (equivalently, its vertical slice at xβ
does not vanish identically near wβ), then πͺ_{E Γ β, (xβ, wβ)} β§Έ (f) is flat over the base stalk
πͺ_{E, xβ} via pullback along Prod.fst.
Local hypersurface finiteness via Weierstrass preparation. If f β πͺ_{E Γ β, (xβ, wβ)} has
vertical power series with nonzero residue-field reduction, then πͺ_{E Γ β, (xβ, wβ)} β§Έ (f) is a
finite algebra over the base stalk πͺ_{E, xβ} via pullback along Prod.fst.
Uniqueness of the local Weierstrass preparation of a holomorphic function. Two
factorizations P_c (w - wβ) * u = P_{c'} (w - wβ) * u' near (xβ, wβ), where P_c is the monic
polynomial TauCeti.Polynomial.monicOfCoeff with lower coefficients c i x vanishing at xβ
and u, u' do not vanish at (xβ, wβ), have the same coefficient germs at xβ and the same
unit germ at (xβ, wβ).
Uniqueness of the local Weierstrass division of a holomorphic function. Two divisions
P_c (w - wβ) * q + β i, r i x * (w - wβ) ^ i = P_c (w - wβ) * q' + β i, r' i x * (w - wβ) ^ i
near (xβ, wβ) by the Weierstrass polynomial P_c = TauCeti.Polynomial.monicOfCoeff c, with
coefficients c i x vanishing at xβ, have the same quotient germ at (xβ, wβ) and the same
remainder coefficient germs at xβ.