Reduction of the prime theorem to prepared coordinates

This file performs the outer, unconditional part of Rueckert's prime-ideal induction. A nonzero prime contains a nonzero nonunit germ. After a linear coordinate change that germ is associated to a positive-degree prepared polynomial. Coordinate invariance then reduces the prime zero-set theorem to the prepared-prime step isolated below.

def LocalComplexGeometry.PreparedPrimeZeroSetStep (n : ℕ) : Prop

The single remaining successor step in prepared coordinates. Unlike the comparator theorem, its hypotheses expose the exact prepared polynomial that drives generic-fiber elimination.

Equations

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

theorem LocalComplexGeometry.evalAtOrigin_eq_zero_of_mem_prime {n : ℕ} {P : Ideal ↥(HolomorphicGerm n)} (hP : P.IsPrime) {f : ↥(HolomorphicGerm n)} (hf : f ∈ P) : evalAtOrigin f = 0

Every member of a proper prime ideal in the local holomorphic germ ring vanishes at the origin.

theorem LocalComplexGeometry.primeZeroSetProperty_succ_of_preparedPrimeZeroSetStep {n : ℕ} (hstep : PreparedPrimeZeroSetStep n) : PrimeZeroSetProperty (n + 1)

A prepared-prime step implies the full prime zero-set property in the successor dimension.

theorem LocalComplexGeometry.primeZeroSetProperty_of_preparedPrimeZeroSetStep (hstep : ∀ (n : ℕ), PreparedPrimeZeroSetStep n) (n : ℕ) : PrimeZeroSetProperty n

Dimension induction closes the complete prime theorem once the prepared successor step has been supplied in every dimension.