The finite-free quotient by a prepared polynomial

The exact kernel and surjectivity of analytic Weierstrass remainder identify the quotient by a prepared polynomial with its vector of d coefficients. Transporting the standard function-space basis gives the classes of 1, w, ..., w^(d-1).

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

The principal ideal generated by a fixed prepared polynomial germ.

Equations

• LocalComplexGeometry.WPTBridge.preparedPolynomialIdeal a ha = Ideal.span {LocalComplexGeometry.WPTBridge.preparedPolynomialGerm a ha}

noncomputable def LocalComplexGeometry.WPTBridge.remainderPolynomialGermLinearMap (n d : ℕ) : (Fin d → ↥(HolomorphicGerm n)) →ₗ[↥(HolomorphicGerm n)] ↥(HolomorphicGerm (n + 1))

Assemble a degree-< d polynomial from its coefficient vector, as a base-linear map.

Equations

• LocalComplexGeometry.WPTBridge.remainderPolynomialGermLinearMap n d = { toFun := LocalComplexGeometry.WPTBridge.remainderPolynomialGerm, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def LocalComplexGeometry.WPTBridge.preparedQuotientRemainderLinearMap {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)) ⧸ preparedPolynomialIdeal a ha →ₗ[↥(HolomorphicGerm n)] Fin d → ↥(HolomorphicGerm n)

Remainder descends to the quotient by the prepared polynomial.

Equations

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

@[simp]

theorem LocalComplexGeometry.WPTBridge.preparedQuotientRemainderLinearMap_mk {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))) : (preparedQuotientRemainderLinearMap a ha ha0) ((Ideal.Quotient.mk (preparedPolynomialIdeal a ha)) h) = preparedGermDivisionRemainder a ha ha0 h

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

The inverse map sends a coefficient vector to the class of its remainder polynomial.

Equations

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

@[simp]

theorem LocalComplexGeometry.WPTBridge.preparedQuotientRemainderSection_apply {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (r : Fin d → ↥(HolomorphicGerm n)) : (preparedQuotientRemainderSection a ha) r = (Ideal.Quotient.mk (preparedPolynomialIdeal a ha)) (remainderPolynomialGerm r)

@[simp]

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

theorem LocalComplexGeometry.WPTBridge.preparedQuotientRemainder_rightInverse {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : preparedQuotientRemainderLinearMap a ha ha0 ∘ₗ preparedQuotientRemainderSection a ha = LinearMap.id

theorem LocalComplexGeometry.WPTBridge.preparedQuotientRemainder_leftInverse {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : preparedQuotientRemainderSection a ha ∘ₗ preparedQuotientRemainderLinearMap a ha ha0 = LinearMap.id

noncomputable def LocalComplexGeometry.WPTBridge.preparedQuotientRemainderEquiv {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)) ⧸ preparedPolynomialIdeal a ha) ≃ₗ[↥(HolomorphicGerm n)] Fin d → ↥(HolomorphicGerm n)

The quotient by a prepared polynomial, as a base-linear copy of its degree-< d coefficient vectors.

Equations

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

@[simp]

theorem LocalComplexGeometry.WPTBridge.preparedQuotientRemainderEquiv_mk {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))) : (preparedQuotientRemainderEquiv a ha ha0) ((Ideal.Quotient.mk (preparedPolynomialIdeal a ha)) h) = preparedGermDivisionRemainder a ha ha0 h

@[simp]

theorem LocalComplexGeometry.WPTBridge.preparedQuotientRemainderEquiv_symm_apply {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (r : Fin d → ↥(HolomorphicGerm n)) : (preparedQuotientRemainderEquiv a ha ha0).symm r = (Ideal.Quotient.mk (preparedPolynomialIdeal a ha)) (remainderPolynomialGerm r)

theorem LocalComplexGeometry.WPTBridge.remainderPolynomialGerm_basisFun {n d : ℕ} (i : Fin d) : remainderPolynomialGerm ((Pi.basisFun (↥(HolomorphicGerm n)) (Fin d)) i) = lastCoordinateGerm n ^ ↑i

@[simp]

theorem LocalComplexGeometry.WPTBridge.preparedGermDivisionRemainder_lastCoordinate_pow {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (i : Fin d) : preparedGermDivisionRemainder a ha ha0 (lastCoordinateGerm n ^ ↑i) = (Pi.basisFun (↥(HolomorphicGerm n)) (Fin d)) i

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

The explicit power basis of the prepared quotient.

Equations

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

@[simp]

theorem LocalComplexGeometry.WPTBridge.preparedQuotientBasis_apply {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (i : Fin d) : (preparedQuotientBasis a ha ha0) i = (Ideal.Quotient.mk (preparedPolynomialIdeal a ha)) (lastCoordinateGerm n ^ ↑i)

theorem LocalComplexGeometry.WPTBridge.preparedQuotient_moduleFree {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : Module.Free (↥(HolomorphicGerm n)) (↥(HolomorphicGerm (n + 1)) ⧸ preparedPolynomialIdeal a ha)

The prepared quotient is free over the lower-dimensional holomorphic germ ring.

theorem LocalComplexGeometry.WPTBridge.preparedQuotient_moduleFinite {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : Module.Finite (↥(HolomorphicGerm n)) (↥(HolomorphicGerm (n + 1)) ⧸ preparedPolynomialIdeal a ha)

The prepared quotient is finite over the lower-dimensional holomorphic germ ring.

theorem LocalComplexGeometry.WPTBridge.preparedQuotient_finiteFree {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : Module.Free (↥(HolomorphicGerm n)) (↥(HolomorphicGerm (n + 1)) ⧸ preparedPolynomialIdeal a ha) ∧ Module.Finite (↥(HolomorphicGerm n)) (↥(HolomorphicGerm (n + 1)) ⧸ preparedPolynomialIdeal a ha)

Combined finite-free conclusion for the quotient by a prepared polynomial. The preceding preparedQuotientBasis specifies its rank-d power basis.