Weierstrass division on holomorphic germs

This file packages the function-level division and uniqueness theorems as a canonical operation on the standard germ ring. A fixed family a represents the coefficients of the prepared divisor; its coefficients are analytic and vanish at the origin.

noncomputable def LocalComplexGeometry.WPTBridge.preparedPolynomialFunction {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) : ComplexEuclidean (n + 1) → ℂ

The prepared polynomial, written in the standard Fin (n + 1) -> C coordinate model used by HolomorphicGerm.

Equations

• LocalComplexGeometry.WPTBridge.preparedPolynomialFunction a x = ClassicalComplexWPT.preparedPolynomial d a ((LocalComplexGeometry.wptAmbientEquiv n) x)

theorem LocalComplexGeometry.WPTBridge.analyticAt_preparedPolynomialFunction {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) : AnalyticAt ℂ (preparedPolynomialFunction a) 0

noncomputable def LocalComplexGeometry.WPTBridge.preparedPolynomialGerm {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) : ↥(HolomorphicGerm (n + 1))

The germ of a fixed prepared polynomial.

Equations

• LocalComplexGeometry.WPTBridge.preparedPolynomialGerm a ha = LocalComplexGeometry.HolomorphicGerm.ofFunction (LocalComplexGeometry.WPTBridge.preparedPolynomialFunction a) ⋯

noncomputable def LocalComplexGeometry.WPTBridge.remainderPolynomialGerm {n d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : ↥(HolomorphicGerm (n + 1))

The degree-< d polynomial germ with a prescribed coefficient vector.

Equations

• LocalComplexGeometry.WPTBridge.remainderPolynomialGerm r = ∑ i : Fin d, (LocalComplexGeometry.lowerDimensionalInclusion n) (r i) * LocalComplexGeometry.lastCoordinateGerm n ^ ↑i

def LocalComplexGeometry.WPTBridge.IsPreparedGermDivision {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (h q : ↥(HolomorphicGerm (n + 1))) (r : Fin d → ↥(HolomorphicGerm n)) : Prop

A quotient and coefficient vector satisfy Weierstrass division at the level of germs.

Equations

• One or more equations did not get rendered due to their size.

theorem LocalComplexGeometry.WPTBridge.coe_remainderPolynomialGerm_ofFunction {n d : ℕ} (r : Fin d → ClassicalComplexWPT.Base n → ℂ) (hr : ∀ (i : Fin d), AnalyticAt ℂ (r i) 0) : ↑(remainderPolynomialGerm fun (i : Fin d) => HolomorphicGerm.ofFunction (r i) ⋯) = ↑fun (x : ComplexEuclidean (n + 1)) => ∑ i : Fin d, r i ((baseProjectionCLM n) x) * (lastCoordinateCLM n) x ^ ↑i

Coercion of a polynomial assembled from analytic coefficient representatives agrees with its pointwise polynomial function.

theorem LocalComplexGeometry.WPTBridge.coe_preparedDivisionExpression_ofFunction {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (q : ComplexEuclidean (n + 1) → ℂ) (hq : AnalyticAt ℂ q 0) (r : Fin d → ClassicalComplexWPT.Base n → ℂ) (hr : ∀ (i : Fin d), AnalyticAt ℂ (r i) 0) : ↑(HolomorphicGerm.ofFunction q hq * preparedPolynomialGerm a ha + remainderPolynomialGerm fun (i : Fin d) => HolomorphicGerm.ofFunction (r i) ⋯) = ↑fun (x : ComplexEuclidean (n + 1)) => q x * preparedPolynomialFunction a x + ∑ i : Fin d, r i ((baseProjectionCLM n) x) * (lastCoordinateCLM n) x ^ ↑i

Coercion of the full quotient-plus-remainder expression assembled from analytic representatives.

theorem LocalComplexGeometry.WPTBridge.exists_preparedGermDivision {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h : ↥(HolomorphicGerm (n + 1))) : ∃ (q : ↥(HolomorphicGerm (n + 1))) (r : Fin d → ↥(HolomorphicGerm n)), IsPreparedGermDivision a ha h q r

Every holomorphic germ admits a quotient and degree-< d remainder by a fixed prepared polynomial.

theorem LocalComplexGeometry.WPTBridge.preparedGermDivision_unique {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h q q' : ↥(HolomorphicGerm (n + 1))) (r r' : Fin d → ↥(HolomorphicGerm n)) (hdivision : IsPreparedGermDivision a ha h q r) (hdivision' : IsPreparedGermDivision a ha h q' r') : q = q' ∧ r = r'

Germ-level uniqueness. In particular, the quotient and coefficient germs do not depend on any analytic representatives used to construct them.

Canonical quotient and remainder

noncomputable def LocalComplexGeometry.WPTBridge.preparedGermDivisionQuotient {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h : ↥(HolomorphicGerm (n + 1))) : ↥(HolomorphicGerm (n + 1))

The canonical quotient, chosen from existence and made intrinsic by preparedGermDivision_unique.

Equations

• LocalComplexGeometry.WPTBridge.preparedGermDivisionQuotient a ha ha0 h = Classical.choose ⋯

noncomputable def LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h : ↥(HolomorphicGerm (n + 1))) : Fin d → ↥(HolomorphicGerm n)

The canonical coefficient vector of the degree-< d remainder.

Equations

• LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder a ha ha0 h = Classical.choose ⋯

theorem LocalComplexGeometry.WPTBridge.preparedGermDivision_spec {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h : ↥(HolomorphicGerm (n + 1))) : IsPreparedGermDivision a ha h (preparedGermDivisionQuotient a ha ha0 h) (preparedGermDivisionRemainder a ha ha0 h)

theorem LocalComplexGeometry.WPTBridge.preparedGermDivision_eq_of_isDivision {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h q : ↥(HolomorphicGerm (n + 1))) (r : Fin d → ↥(HolomorphicGerm n)) (hdivision : IsPreparedGermDivision a ha h q r) : preparedGermDivisionQuotient a ha ha0 h = q ∧ preparedGermDivisionRemainder a ha ha0 h = r

@[simp]

theorem LocalComplexGeometry.WPTBridge.remainderPolynomialGerm_zero {n d : ℕ} : remainderPolynomialGerm 0 = 0

theorem LocalComplexGeometry.WPTBridge.remainderPolynomialGerm_add {n d : ℕ} (r s : Fin d → ↥(HolomorphicGerm n)) : remainderPolynomialGerm (r + s) = remainderPolynomialGerm r + remainderPolynomialGerm s

theorem LocalComplexGeometry.WPTBridge.remainderPolynomialGerm_smul {n d : ℕ} (c : ↥(HolomorphicGerm n)) (r : Fin d → ↥(HolomorphicGerm n)) : remainderPolynomialGerm (c • r) = c • remainderPolynomialGerm r

@[simp]

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder_zero {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : preparedGermDivisionRemainder a ha ha0 0 = 0

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder_add {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h k : ↥(HolomorphicGerm (n + 1))) : preparedGermDivisionRemainder a ha ha0 (h + k) = preparedGermDivisionRemainder a ha ha0 h + preparedGermDivisionRemainder a ha ha0 k

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder_smul {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (c : ↥(HolomorphicGerm n)) (h : ↥(HolomorphicGerm (n + 1))) : preparedGermDivisionRemainder a ha ha0 (c • h) = c • preparedGermDivisionRemainder a ha ha0 h

noncomputable def LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainderLinearMap {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : ↥(HolomorphicGerm (n + 1)) →ₗ[↥(HolomorphicGerm n)] Fin d → ↥(HolomorphicGerm n)

The base-linear coefficient-remainder map supplied by analytic Weierstrass division.

Equations

• LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainderLinearMap a ha ha0 = { toFun := LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder a ha ha0, map_add' := ⋯, map_smul' := ⋯ }

Kernel and principal divisibility

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder_eq_zero_iff {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h : ↥(HolomorphicGerm (n + 1))) : preparedGermDivisionRemainder a ha ha0 h = 0 ↔ ∃ (q : ↥(HolomorphicGerm (n + 1))), h = q * preparedPolynomialGerm a ha

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder_eq_zero_iff_mem_span {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h : ↥(HolomorphicGerm (n + 1))) : preparedGermDivisionRemainder a ha ha0 h = 0 ↔ h ∈ Ideal.span {preparedPolynomialGerm a ha}

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainderLinearMap_ker {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : (preparedGermDivisionRemainderLinearMap a ha ha0).ker = Submodule.restrictScalars (↥(HolomorphicGerm n)) (Ideal.span {preparedPolynomialGerm a ha})

The exact kernel statement needed by Rückert's remainder-module induction: the kernel is the principal ideal generated by the prepared polynomial, viewed as a module over lower-dimensional germs.

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainderLinearMap_ker_le {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : (preparedGermDivisionRemainderLinearMap a ha ha0).ker ≤ Submodule.restrictScalars (↥(HolomorphicGerm n)) (Ideal.span {preparedPolynomialGerm a ha})

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainderLinearMap_surjective {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : Function.Surjective ⇑(preparedGermDivisionRemainderLinearMap a ha ha0)

Every coefficient vector already is the remainder of its degree-< d polynomial germ.