The generic fibre of a prepared prime quotient

This file isolates the commutative-algebra layer used in the prime case of the local analytic Nullstellensatz. A prime ideal of the ambient germ ring which contains a prepared monic equation gives a finite integral extension of its contracted quotient. Passing to fraction fields therefore gives a finite extension, in which the last-coordinate class has a nonzero separable minimal polynomial. The last section clears all coefficients of that minimal polynomial back to the contracted quotient.

Contraction and quotient rings

@[reducible, inline]

noncomputable abbrev LocalComplexGeometry.lowerDimensionalContraction {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : Ideal ↥(HolomorphicGerm n)

Contraction of an ambient ideal along the lower-dimensional germ inclusion.

Equations

• LocalComplexGeometry.lowerDimensionalContraction P = Ideal.under (↥(LocalComplexGeometry.HolomorphicGerm n)) P

@[reducible, inline]

abbrev LocalComplexGeometry.ContractedGermQuotient {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : Type

The quotient of the lower-dimensional germ ring by the contraction of P.

Equations

• LocalComplexGeometry.ContractedGermQuotient P = (↥(LocalComplexGeometry.HolomorphicGerm n) ⧸ LocalComplexGeometry.lowerDimensionalContraction P)

@[reducible, inline]

abbrev LocalComplexGeometry.AmbientGermQuotient {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : Type

The ambient germ quotient by P.

Equations

• LocalComplexGeometry.AmbientGermQuotient P = (↥(LocalComplexGeometry.HolomorphicGerm (n + 1)) ⧸ P)

noncomputable def LocalComplexGeometry.contractedQuotientMap {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : ContractedGermQuotient P →+* AmbientGermQuotient P

The canonical quotient-base map induced by lowerDimensionalInclusion.

Equations

• LocalComplexGeometry.contractedQuotientMap P = algebraMap (LocalComplexGeometry.ContractedGermQuotient P) (LocalComplexGeometry.AmbientGermQuotient P)

@[simp]

theorem LocalComplexGeometry.contractedQuotientMap_mk {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) (f : ↥(HolomorphicGerm n)) : (contractedQuotientMap P) ((Ideal.Quotient.mk (lowerDimensionalContraction P)) f) = (Ideal.Quotient.mk P) ((lowerDimensionalInclusion n) f)

theorem LocalComplexGeometry.lowerDimensionalContraction_isPrime {n : ℕ} {P : Ideal ↥(HolomorphicGerm (n + 1))} (hP : P.IsPrime) : (lowerDimensionalContraction P).IsPrime

Contraction of a prime ideal is prime.

theorem LocalComplexGeometry.contractedQuotientMap_injective {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : Function.Injective ⇑(contractedQuotientMap P)

The canonical map from the contracted quotient is injective.

Finiteness from a prepared monic equation

theorem LocalComplexGeometry.preparedPolynomialIdeal_le_of_mem {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) {P : Ideal ↥(HolomorphicGerm (n + 1))} (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : WPTBridge.preparedPolynomialIdeal a ha ≤ P

Membership of the prepared polynomial in P puts its principal ideal below P.

theorem LocalComplexGeometry.ambientQuotient_moduleFinite_over_germs {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (P : Ideal ↥(HolomorphicGerm (n + 1))) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : Module.Finite (↥(HolomorphicGerm n)) (AmbientGermQuotient P)

Before quotienting the base by the contraction, the ambient prime quotient is already a finite module over the lower-dimensional germ ring.

theorem LocalComplexGeometry.ambientQuotient_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) (P : Ideal ↥(HolomorphicGerm (n + 1))) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : Module.Finite (ContractedGermQuotient P) (AmbientGermQuotient P)

The ambient prime quotient is finite over the quotient by the contracted prime. This is the module-finite generic-projection statement over the local base, before passing to fraction fields.

theorem LocalComplexGeometry.ambientQuotient_isIntegral {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (P : Ideal ↥(HolomorphicGerm (n + 1))) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : Algebra.IsIntegral (ContractedGermQuotient P) (AmbientGermQuotient P)

Module-finiteness makes every class in the ambient quotient integral over the contracted quotient.

Clearing coefficients in a fraction field

theorem LocalComplexGeometry.clearFractionPolynomialDenominators {A : Type u_1} [CommRing A] [IsDomain A] (p : Polynomial (FractionRing A)) (hp : p ≠ 0) : ∃ (d : A), d ≠ 0 ∧ ∃ (q : Polynomial A), q ≠ 0 ∧ Polynomial.map (algebraMap A (FractionRing A)) q = Polynomial.C ((algebraMap A (FractionRing A)) d) * p

A nonzero polynomial over a fraction field has a nonzero common denominator and a nonzero polynomial lift after multiplication by it.

theorem LocalComplexGeometry.clearFractionPolynomialDenominators_allowZero {A : Type u_1} [CommRing A] [IsDomain A] (p : Polynomial (FractionRing A)) : ∃ (d : A), d ≠ 0 ∧ ∃ (q : Polynomial A), Polynomial.map (algebraMap A (FractionRing A)) q = Polynomial.C ((algebraMap A (FractionRing A)) d) * p

Common-denominator clearance without a nonzero hypothesis. This version also covers the zero quotient polynomial arising from a generator whose WPT remainder vanishes identically on the generic fibre.

The fraction-field generic fibre

@[reducible, inline]

abbrev LocalComplexGeometry.ContractedFractionField {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : Type

Fraction field of the contracted prime quotient.

Equations

• LocalComplexGeometry.ContractedFractionField P = FractionRing (LocalComplexGeometry.ContractedGermQuotient P)

@[reducible, inline]

abbrev LocalComplexGeometry.AmbientFractionField {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : Type

Fraction field of the ambient prime quotient.

Equations

• LocalComplexGeometry.AmbientFractionField P = FractionRing (LocalComplexGeometry.AmbientGermQuotient P)

noncomputable def LocalComplexGeometry.lastCoordinateQuotientClass {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : AmbientGermQuotient P

The last-coordinate germ viewed in the ambient prime quotient.

Equations

• LocalComplexGeometry.lastCoordinateQuotientClass P = (Ideal.Quotient.mk P) (LocalComplexGeometry.lastCoordinateGerm n)

The explicit polynomials represented by prepared and remainder germs.

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

The analytic coefficient a i, regarded as a lower-dimensional germ.

Equations

• LocalComplexGeometry.preparedCoefficientGerm a ha i = LocalComplexGeometry.HolomorphicGerm.ofFunction (a i) ⋯

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

The prepared monic polynomial with coefficients in the base germ ring.

Equations

• LocalComplexGeometry.preparedGermPolynomial a ha = Polynomial.X ^ d + ∑ i : Fin d, Polynomial.C (LocalComplexGeometry.preparedCoefficientGerm a ha i) * Polynomial.X ^ ↑i

noncomputable def LocalComplexGeometry.remainderGermPolynomial {n d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : Polynomial ↥(HolomorphicGerm n)

A WPT coefficient vector, assembled as a polynomial over the base germ ring.

Equations

• LocalComplexGeometry.remainderGermPolynomial r = ∑ i : Fin d, Polynomial.C (r i) * Polynomial.X ^ ↑i

@[simp]

theorem LocalComplexGeometry.aeval_remainderGermPolynomial {n d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : (Polynomial.aeval (lastCoordinateGerm n)) (remainderGermPolynomial r) = WPTBridge.remainderPolynomialGerm r

@[simp]

theorem LocalComplexGeometry.aeval_preparedGermPolynomial {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) : (Polynomial.aeval (lastCoordinateGerm n)) (preparedGermPolynomial a ha) = WPTBridge.preparedPolynomialGerm a ha

noncomputable def LocalComplexGeometry.complexToContractedQuotient {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : ℂ →+* ContractedGermQuotient P

The injective map from the complex constants into the contracted quotient.

Equations

• LocalComplexGeometry.complexToContractedQuotient P = (Ideal.Quotient.mk (LocalComplexGeometry.lowerDimensionalContraction P)).comp (LocalComplexGeometry.constantGermHom n)

theorem LocalComplexGeometry.complexToContractedQuotient_injective {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] : Function.Injective ⇑(complexToContractedQuotient P)

instance LocalComplexGeometry.contractedGermQuotient_charZero {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] : CharZero (ContractedGermQuotient P)

Contracted prime quotients of complex germ rings have characteristic zero.

@[instance_reducible]

noncomputable instance LocalComplexGeometry.contractedFractionFieldAlgebra {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] : Algebra (ContractedFractionField P) (AmbientFractionField P)

The ambient fraction field is canonically an algebra over the contracted fraction field, extending the contracted quotient map.

Equations

• LocalComplexGeometry.contractedFractionFieldAlgebra P = FractionRing.liftAlgebra (LocalComplexGeometry.ContractedGermQuotient P) (LocalComplexGeometry.AmbientFractionField P)

instance LocalComplexGeometry.contractedFractionField_charZero {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] : CharZero (ContractedFractionField P)

The fraction field of the contracted quotient also has characteristic zero.

noncomputable def LocalComplexGeometry.genericLastCoordinate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) : AmbientFractionField P

The last-coordinate class in the fraction-field generic fibre.

Equations

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

noncomputable def LocalComplexGeometry.genericLastCoordinateMinpoly {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] : Polynomial (ContractedFractionField P)

The minimal polynomial of the generic last-coordinate class over the contracted fraction field.

Equations

• LocalComplexGeometry.genericLastCoordinateMinpoly P = minpoly (LocalComplexGeometry.ContractedFractionField P) (LocalComplexGeometry.genericLastCoordinate P)

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

The prepared polynomial after reducing its coefficients modulo the contracted prime.

Equations

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

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

The prepared polynomial over the contracted fraction field.

Equations

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

noncomputable def LocalComplexGeometry.contractedRemainderPolynomial {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) {d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : Polynomial (ContractedGermQuotient P)

A WPT remainder polynomial after reducing its coefficients modulo the contracted prime.

Equations

• LocalComplexGeometry.contractedRemainderPolynomial P r = Polynomial.map (Ideal.Quotient.mk (LocalComplexGeometry.lowerDimensionalContraction P)) (LocalComplexGeometry.remainderGermPolynomial r)

noncomputable def LocalComplexGeometry.genericRemainderPolynomial {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) {d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : Polynomial (ContractedFractionField P)

A WPT remainder polynomial over the contracted fraction field.

Equations

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

@[simp]

theorem LocalComplexGeometry.aeval_contractedRemainderPolynomial {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) {d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : (Polynomial.aeval (lastCoordinateQuotientClass P)) (contractedRemainderPolynomial P r) = (Ideal.Quotient.mk P) (WPTBridge.remainderPolynomialGerm r)

@[simp]

theorem LocalComplexGeometry.aeval_contractedPreparedPolynomial {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) : (Polynomial.aeval (lastCoordinateQuotientClass P)) (contractedPreparedPolynomial P a ha) = (Ideal.Quotient.mk P) (WPTBridge.preparedPolynomialGerm a ha)

@[simp]

theorem LocalComplexGeometry.aeval_genericRemainderPolynomial {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : (Polynomial.aeval (genericLastCoordinate P)) (genericRemainderPolynomial P r) = (algebraMap (AmbientGermQuotient P) (AmbientFractionField P)) ((Ideal.Quotient.mk P) (WPTBridge.remainderPolynomialGerm r))

@[simp]

theorem LocalComplexGeometry.aeval_genericPreparedPolynomial {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) : (Polynomial.aeval (genericLastCoordinate P)) (genericPreparedPolynomial P a ha) = (algebraMap (AmbientGermQuotient P) (AmbientFractionField P)) ((Ideal.Quotient.mk P) (WPTBridge.preparedPolynomialGerm a ha))

theorem LocalComplexGeometry.genericPreparedPolynomial_aeval_eq_zero {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : (Polynomial.aeval (genericLastCoordinate P)) (genericPreparedPolynomial P a ha) = 0

The prepared polynomial annihilates the generic last-coordinate class.

theorem LocalComplexGeometry.genericRemainderPolynomial_aeval_eq_ambientClass {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (h : ↥(HolomorphicGerm (n + 1))) : (Polynomial.aeval (genericLastCoordinate P)) (genericRemainderPolynomial P (WPTBridge.preparedGermDivisionRemainder a ha ha0 h)) = (algebraMap (AmbientGermQuotient P) (AmbientFractionField P)) ((Ideal.Quotient.mk P) h)

WPT division represents every ambient germ class by its degree-< d remainder polynomial on the generic fibre.

theorem LocalComplexGeometry.mem_prime_iff_genericRemainder_aeval_eq_zero {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (h : ↥(HolomorphicGerm (n + 1))) : h ∈ P ↔ (Polynomial.aeval (genericLastCoordinate P)) (genericRemainderPolynomial P (WPTBridge.preparedGermDivisionRemainder a ha ha0 h)) = 0

An ambient germ belongs to P exactly when the WPT remainder polynomial vanishes at the generic last-coordinate class.

theorem LocalComplexGeometry.genericFractionField_finiteDimensional {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : FiniteDimensional (ContractedFractionField P) (AmbientFractionField P)

The two fraction fields form a finite-dimensional extension whenever P contains the prepared monic equation.

theorem LocalComplexGeometry.genericLastCoordinate_isIntegral {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : IsIntegral (ContractedFractionField P) (genericLastCoordinate P)

In particular, the generic last-coordinate class is algebraic (integral, because the base is a field).

theorem LocalComplexGeometry.genericLastCoordinateMinpoly_dvd_genericPreparedPolynomial {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : genericLastCoordinateMinpoly P ∣ genericPreparedPolynomial P a ha

The generic last-coordinate minimal polynomial divides the prepared monic polynomial which produced the finite extension.

theorem LocalComplexGeometry.mem_prime_iff_minpoly_dvd_genericRemainderPolynomial {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (h : ↥(HolomorphicGerm (n + 1))) : h ∈ P ↔ genericLastCoordinateMinpoly P ∣ genericRemainderPolynomial P (WPTBridge.preparedGermDivisionRemainder a ha ha0 h)

Prime membership is exactly divisibility of the generic WPT remainder by the generic last-coordinate minimal polynomial.

theorem LocalComplexGeometry.genericLastCoordinateMinpoly_monic {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : (genericLastCoordinateMinpoly P).Monic

The generic last-coordinate minimal polynomial is monic.

theorem LocalComplexGeometry.genericLastCoordinateMinpoly_ne_zero {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : genericLastCoordinateMinpoly P ≠ 0

The generic last-coordinate minimal polynomial is nonzero.

theorem LocalComplexGeometry.genericLastCoordinateMinpoly_separable {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : (genericLastCoordinateMinpoly P).Separable

Characteristic zero makes the generic last-coordinate minimal polynomial separable.

structure LocalComplexGeometry.GenericMinpolyLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] : Type

A single base denominator and same-degree polynomial lift of the generic last-coordinate minimal polynomial. The denominator remains nonzero modulo the contraction, and the displayed identity is an identity over the contracted fraction field.

• denominator : ↥(HolomorphicGerm n)

  The common denominator in the base germ ring.

• polynomial : Polynomial ↥(HolomorphicGerm n)

  A polynomial lift of the generic minimal polynomial.

• denominator_not_mem : self.denominator ∉ lowerDimensionalContraction P
• polynomial_mod_contraction_ne_zero : Polynomial.map (Ideal.Quotient.mk (lowerDimensionalContraction P)) self.polynomial ≠ 0
• map_polynomial : Polynomial.map (algebraMap (ContractedGermQuotient P) (ContractedFractionField P)) (Polynomial.map (Ideal.Quotient.mk (lowerDimensionalContraction P)) self.polynomial) = Polynomial.C ((algebraMap (ContractedGermQuotient P) (ContractedFractionField P)) ((Ideal.Quotient.mk (lowerDimensionalContraction P)) self.denominator)) * genericLastCoordinateMinpoly P
• natDegree_eq : self.polynomial.natDegree = (genericLastCoordinateMinpoly P).natDegree
• natDegree_pos : 0 < self.polynomial.natDegree

noncomputable def LocalComplexGeometry.genericMinpolyLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : GenericMinpolyLiftCertificate P

Canonical choice of the cleared, same-degree minimal-polynomial lift.

Equations

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

theorem LocalComplexGeometry.genericMinpolyLiftCertificate_leadingCoeff_sub_denominator_mem {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; c.polynomial.leadingCoeff - c.denominator ∈ lowerDimensionalContraction P

The top coefficient of the cleared lift agrees with its common denominator modulo the contraction. This is the coefficient-level form of the fact that the target minimal polynomial is monic.

theorem LocalComplexGeometry.genericMinpolyLiftCertificate_leadingCoeff_not_mem {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; c.polynomial.leadingCoeff ∉ lowerDimensionalContraction P

The top coefficient of the cleared minimal-polynomial lift is a concrete nonzero base germ modulo the contraction.

theorem LocalComplexGeometry.genericMinpolyLiftCertificate_resultant_not_mem {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; c.polynomial.resultant (Polynomial.derivative c.polynomial) c.polynomial.natDegree (c.polynomial.natDegree - 1) ∉ lowerDimensionalContraction P

The fixed-size derivative resultant of the lifted minimal polynomial is a second concrete base germ outside the contraction. The matrix sizes are the exact degree e and e - 1, so this is directly usable by fixed-degree polynomial-specialization results.

Denominator-cleared divisibility identities

structure LocalComplexGeometry.GenericMinpolyDivisibilityLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) (Q R : Polynomial ↥(HolomorphicGerm n)) : Type

A polynomial identity modulo the contracted prime, with one explicit common denominator outside that prime. The error field is kept as an honest polynomial over the base germ ring; every one of its coefficients is certified to lie in the contraction.

• denominator : ↥(HolomorphicGerm n)

  The denominator clearing the generic divisibility identity.

• quotient : Polynomial ↥(HolomorphicGerm n)

  The lifted quotient polynomial.

• error : Polynomial ↥(HolomorphicGerm n)

  The coefficientwise contraction error.

• denominator_not_mem : self.denominator ∉ lowerDimensionalContraction P
• identity : Polynomial.C self.denominator * R = Q * self.quotient + self.error
• error_coeff_mem (k : ℕ) : self.error.coeff k ∈ lowerDimensionalContraction P

theorem LocalComplexGeometry.remainderGermPolynomial_coefficients_eq {n e : ℕ} (B : Polynomial ↥(HolomorphicGerm n)) (hB : B.natDegree < e) : (remainderGermPolynomial fun (i : Fin e) => B.coeff ↑i) = B

A polynomial of degree strictly below e is recovered from its first e coefficients in the same format used by WPT remainders.

structure LocalComplexGeometry.GenericRemainderModMinpolyLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] (Q R : Polynomial ↥(HolomorphicGerm n)) : Type

A denominator-cleared Euclidean remainder of R modulo the generic minimal polynomial. Its displayed coefficient vector has length exactly Q.natDegree, the identity holds over the base germ ring up to a coefficientwise contraction error, and vanishing of all displayed coefficients modulo the contraction forces generic divisibility.

• positiveDegree : 0 < Q.natDegree
• coefficients : Fin Q.natDegree → ↥(HolomorphicGerm n)

  Coefficients of the strict remainder.

• denominator : ↥(HolomorphicGerm n)

  The denominator clearing the lifted Euclidean-division identity.

• quotient : Polynomial ↥(HolomorphicGerm n)

  The quotient in the lifted Euclidean-division identity.

• error : Polynomial ↥(HolomorphicGerm n)

  The coefficientwise contraction error.

• denominator_not_mem : self.denominator ∉ lowerDimensionalContraction P
• identity : Polynomial.C self.denominator * R = Q * self.quotient + remainderGermPolynomial self.coefficients + self.error
• error_coeff_mem (k : ℕ) : self.error.coeff k ∈ lowerDimensionalContraction P
• divisible_of_coeff_mem : (∀ (i : Fin Q.natDegree), self.coefficients i ∈ lowerDimensionalContraction P) → genericLastCoordinateMinpoly P ∣ Polynomial.map (algebraMap (ContractedGermQuotient P) (ContractedFractionField P)) (Polynomial.map (Ideal.Quotient.mk (lowerDimensionalContraction P)) R)

noncomputable def LocalComplexGeometry.genericMinpolyDivisibilityLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (R : Polynomial ↥(HolomorphicGerm n)) (hdiv : genericLastCoordinateMinpoly P ∣ Polynomial.map (algebraMap (ContractedGermQuotient P) (ContractedFractionField P)) (Polynomial.map (Ideal.Quotient.mk (lowerDimensionalContraction P)) R)) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; GenericMinpolyDivisibilityLiftCertificate P c.polynomial R

Clear the quotient in a generic-fibre divisibility statement. The result is a specialization-friendly identity over the original base germ ring, with a single denominator and coefficientwise contraction error.

Equations

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

structure LocalComplexGeometry.CommonGenericMinpolyDivisibilityLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) {ι : Type u_1} [Fintype ι] (Q : Polynomial ↥(HolomorphicGerm n)) (R : ι → Polynomial ↥(HolomorphicGerm n)) : Type u_1

A finite family of lifted divisibility identities sharing exactly one base denominator outside the contraction.

• denominator : ↥(HolomorphicGerm n)

  A denominator shared by the finite family of identities.

• quotient : ι → Polynomial ↥(HolomorphicGerm n)

  The family of lifted quotient polynomials.

• error : ι → Polynomial ↥(HolomorphicGerm n)

  The family of coefficientwise contraction errors.

• denominator_not_mem : self.denominator ∉ lowerDimensionalContraction P
• identity (i : ι) : Polynomial.C self.denominator * R i = Q * self.quotient i + self.error i
• error_coeff_mem (i : ι) (k : ℕ) : (self.error i).coeff k ∈ lowerDimensionalContraction P

noncomputable def LocalComplexGeometry.commonGenericMinpolyDivisibilityLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {ι : Type u_1} [Fintype ι] (Q : Polynomial ↥(HolomorphicGerm n)) (R : ι → Polynomial ↥(HolomorphicGerm n)) (C : (i : ι) → GenericMinpolyDivisibilityLiftCertificate P Q (R i)) : CommonGenericMinpolyDivisibilityLiftCertificate P Q R

Replace finitely many individual denominator-cleared identities by identities with their product as a single common denominator.

Equations

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

noncomputable def LocalComplexGeometry.genericRemainderModMinpolyLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (R : Polynomial ↥(HolomorphicGerm n)) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; GenericRemainderModMinpolyLiftCertificate P c.polynomial R

Divide an arbitrary base polynomial by the generic minimal polynomial, then clear the quotient and the strict-lower-degree remainder with one common denominator. The lifted remainder is returned as a fixed-size coefficient vector, and coefficientwise membership in the contraction recovers the original generic divisibility statement.

Equations

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

noncomputable def LocalComplexGeometry.preparedPolynomialMinpolyDivisibilityLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; GenericMinpolyDivisibilityLiftCertificate P c.polynomial (preparedGermPolynomial a ha)

The prepared monic polynomial itself has a cleared multiple identity by the lifted generic minimal polynomial.

Equations

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

noncomputable def LocalComplexGeometry.primeMemberRemainderMinpolyDivisibilityLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (h : ↥(HolomorphicGerm (n + 1))) (hh : h ∈ P) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; GenericMinpolyDivisibilityLiftCertificate P c.polynomial (remainderGermPolynomial (WPTBridge.preparedGermDivisionRemainder a ha ha0 h))

Every member of the prime has a denominator-cleared identity for its WPT remainder.

Equations

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

noncomputable def LocalComplexGeometry.ambientGermRemainderModMinpolyLiftCertificate {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (g : ↥(HolomorphicGerm (n + 1))) : have c := genericMinpolyLiftCertificate P a ha ha0 hmem; GenericRemainderModMinpolyLiftCertificate P c.polynomial (remainderGermPolynomial (WPTBridge.preparedGermDivisionRemainder a ha ha0 g))

The Euclidean-remainder certificate for the WPT remainder of an arbitrary ambient germ.

Equations

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

theorem LocalComplexGeometry.ambientGermRemainderModMinpolyLiftCertificate_mem_of_coeff_mem {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (g : ↥(HolomorphicGerm (n + 1))) : have C := ambientGermRemainderModMinpolyLiftCertificate P a ha ha0 hmem g; (∀ (i : Fin (genericMinpolyLiftCertificate P a ha ha0 hmem).polynomial.natDegree), C.coefficients i ∈ lowerDimensionalContraction P) → g ∈ P

If every coefficient of the cleared strict remainder of an ambient germ lies in the contraction, then the ambient germ lies in the original prime.

noncomputable def LocalComplexGeometry.genericMinpolyLiftSpecializationBadFactor {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : ↥(HolomorphicGerm n)

The product of the leading coefficient and the fixed-size derivative resultant is one common specialization bad factor outside the contraction.

Equations

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

theorem LocalComplexGeometry.genericMinpolyLiftSpecializationBadFactor_not_mem {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] {d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) : genericMinpolyLiftSpecializationBadFactor P a ha ha0 hmem ∉ lowerDimensionalContraction P

The common specialization bad factor is not in the contracted prime.

theorem LocalComplexGeometry.genericLastCoordinateMinpoly_aeval {n : ℕ} (P : Ideal ↥(HolomorphicGerm (n + 1))) [P.IsPrime] : (Polynomial.aeval (genericLastCoordinate P)) (genericLastCoordinateMinpoly P) = 0

The minimal polynomial annihilates the generic last-coordinate class.