Polynomial sections in the distinguished coordinate over a product open

The third step of the proof of Oka's coherence theorem [Fre17, Ch. I, 10.3] writes the entries of the matrix, after the preparation theorem, as Weierstrass polynomials in z_n "with coefficients independent of z_n", and reads the relations of z_n-degree < m as vectors of 𝒪(V)[z_n : m] ≅ 𝒪(V)^m. On the model Kᵐ⁺¹ = Kn K (m + 1) with the distinguished coordinate x_0 and the projection π : Kᵐ⁺¹ → Kᵐ (projKn) this module provides, over the product open π⁻¹ V (baseOpens ψ V):

• the coordinate sections x0Sec, the constant sections cSec, the shift shiftSec V x₀ = x_0 − x₀, and the pull-back pullSec V w = w ∘ π of a section w of the base, with their germs identified with the coordinate germs and the constants (germ_x0Sec, germ_cSec) and their Taylor series at every point a of π⁻¹ V (TKn_germ_shiftSec: x_0 − x₀ ↦ X_0 − C (x₀ − a_0); TKn_germ_pullSec: w ∘ π ↦ liftTail (T_{π a} w));
• the polynomial combinations polyComb V x₀ w = Σ_k (w k ∘ π) (x_0 − x₀)^k and the monic polynomial sections polyMonic V x₀ e c = (x_0 − x₀)^e + Σ_j (c j ∘ π) (x_0 − x₀)^{e−1−j} (the shape of a Weierstrass polynomial, weierstrassPoly), whose Taylor series at a are ofPoly of the corresponding polynomial over the tail ring composed with X − C (x₀ − a_0) (TKn_germ_polyComb, TKn_germ_polyMonic): a polynomial of x_0-degree < N, respectively monic of degree e, at every point of π⁻¹ V, which is why Oka's lemma applies pointwise with one degree bound;
• coefficient extraction: a polynomial combination has germ 0 at a iff all its coefficient sections have germ 0 at π a (germ_polyComb_eq_zero_iff), through the polynomial polyOfCoeff c = Σ_k C (c k) X^k with coefficient vector c over any commutative ring (polyOfCoeff_eq_zero_iff).

Every statement is bookkeeping for the induction of Oka's theorem (Hironaka.AnalyticSpace.Oka.Core).

noncomputable def AnalyticSpace.polyOfCoeff {R : Type u_1} [CommRing R] {N : ℕ} (c : Fin N → R) : Polynomial R

Σ_k C (c k) X^k: the polynomial with coefficient vector c (degree < N).

Equations

• AnalyticSpace.polyOfCoeff c = ∑ k : Fin N, Polynomial.C (c k) * Polynomial.X ^ ↑k

theorem AnalyticSpace.coeff_polyOfCoeff {R : Type u_1} [CommRing R] {N : ℕ} (c : Fin N → R) (k : ℕ) : (polyOfCoeff c).coeff k = if h : k < N then c ⟨k, h⟩ else 0

theorem AnalyticSpace.natDegree_polyOfCoeff_lt {R : Type u_1} [CommRing R] {N : ℕ} (c : Fin N → R) (hN : 0 < N) : (polyOfCoeff c).natDegree < N

theorem AnalyticSpace.polyOfCoeff_eq_zero_iff {R : Type u_1} [CommRing R] {N : ℕ} (c : Fin N → R) : polyOfCoeff c = 0 ↔ ∀ (k : Fin N), c k = 0

def AnalyticSpace.x0Sec {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (W : TopologicalSpace.Opens (Kn K n)) (i : Fin n) : ↑((sheafKn K n).presheaf.obj (Opposite.op W))

The coordinate function x_i = ψ_i as a section of 𝒜_{Kⁿ} over W.

Equations

• AnalyticSpace.x0Sec ψ W i = Manifold.sectionOfContMDiffOn (fun (y : AnalyticSpace.Kn K n) => ψ y i) W ⋯

theorem AnalyticSpace.x0Sec_apply {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (W : TopologicalSpace.Opens (Kn K n)) (i : Fin n) (y : ↥W) : ↑(x0Sec ψ W i) y = ψ (↑y) i

def AnalyticSpace.cSec {K : Type} [RCLike K] {n : ℕ} (W : TopologicalSpace.Opens (Kn K n)) (t : K) : ↑((sheafKn K n).presheaf.obj (Opposite.op W))

The constant t as a section over W.

Equations

• AnalyticSpace.cSec W t = Manifold.sectionOfContMDiffOn (fun (x : AnalyticSpace.Kn K n) => t) W ⋯

theorem AnalyticSpace.cSec_apply {K : Type} [RCLike K] {n : ℕ} (W : TopologicalSpace.Opens (Kn K n)) (t : K) (y : ↥W) : ↑(cSec W t) y = t

theorem AnalyticSpace.germ_x0Sec {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) {W : TopologicalSpace.Opens (Kn K n)} {a : Kn K n} (ha : a ∈ W) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom ((sheafKn K n).presheaf.germ W a ha)) (x0Sec ψ W i) = coordKn ψ a i

The germ of the coordinate section is the coordinate germ coordKn.

theorem AnalyticSpace.germ_cSec {K : Type} [RCLike K] {n : ℕ} {W : TopologicalSpace.Opens (Kn K n)} {a : Kn K n} (ha : a ∈ W) (t : K) : (CategoryTheory.ConcreteCategory.hom ((sheafKn K n).presheaf.germ W a ha)) (cSec W t) = (Manifold.const K (Kn K n) (Kn K n) a) t

The germ of the constant section is the constant.

theorem AnalyticSpace.TKn_germ_x0Sec {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) {W : TopologicalSpace.Opens (Kn K n)} {a : Kn K n} (ha : a ∈ W) (i : Fin n) : (TKn ψ a) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K n).presheaf.germ W a ha)) (x0Sec ψ W i)) = MvPowerSeries.X i + MvPowerSeries.C (ψ a i)

theorem AnalyticSpace.TKn_germ_cSec {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) {W : TopologicalSpace.Opens (Kn K n)} {a : Kn K n} (ha : a ∈ W) (t : K) : (TKn ψ a) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K n).presheaf.germ W a ha)) (cSec W t)) = MvPowerSeries.C t

@[reducible, inline]

abbrev AnalyticSpace.baseOpens {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (V : TopologicalSpace.Opens (Kn K m)) : TopologicalSpace.Opens (Kn K (m + 1))

The product open π⁻¹ V ⊆ Kᵐ⁺¹ over an open V ⊆ Kᵐ (Freitag's V × (−r, r) Fre17, Ch. I, 10.3, here with the whole line as second factor).

Equations

• AnalyticSpace.baseOpens ψ V = Manifold.preimageOpens ⇑(AnalyticSpace.projKn ψ) ⋯ V

theorem AnalyticSpace.mem_baseOpens {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) {V : TopologicalSpace.Opens (Kn K m)} {a : Kn K (m + 1)} : a ∈ baseOpens ψ V ↔ (projKn ψ) a ∈ V

noncomputable def AnalyticSpace.shiftSec {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (V : TopologicalSpace.Opens (Kn K m)) (x0 : K) : ↑((sheafKn K (m + 1)).presheaf.obj (Opposite.op (baseOpens ψ V)))

The shifted coordinate x_0 − x₀ over π⁻¹ V.

Equations

• AnalyticSpace.shiftSec ψ V x0 = AnalyticSpace.x0Sec ψ (AnalyticSpace.baseOpens ψ V) 0 - AnalyticSpace.cSec (AnalyticSpace.baseOpens ψ V) x0

noncomputable def AnalyticSpace.pullSec {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (V : TopologicalSpace.Opens (Kn K m)) (w : ↑((sheafKn K m).presheaf.obj (Opposite.op V))) : ↑((sheafKn K (m + 1)).presheaf.obj (Opposite.op (baseOpens ψ V)))

The pull-back w ∘ π of a section of the base.

Equations

• AnalyticSpace.pullSec ψ V w = Manifold.comapSection ⇑(AnalyticSpace.projKn ψ) ⋯ w

theorem AnalyticSpace.TKn_germ_shiftSec {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) {V : TopologicalSpace.Opens (Kn K m)} {a : Kn K (m + 1)} (ha : a ∈ baseOpens ψ V) (x0 : K) : (TKn ψ a) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (shiftSec ψ V x0)) = MvPowerSeries.X 0 - MvPowerSeries.C (x0 - ψ a 0)

theorem AnalyticSpace.TKn_germ_pullSec {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) {V : TopologicalSpace.Opens (Kn K m)} {a : Kn K (m + 1)} (ha : a ∈ baseOpens ψ V) (w : ↑((sheafKn K m).presheaf.obj (Opposite.op V))) : (TKn ψ a) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (pullSec ψ V w)) = Analytic.liftTail ((TKn (knCoord K m) ((projKn ψ) a)) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V ((projKn ψ) a) ha)) w))

noncomputable def AnalyticSpace.polyComb {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (V : TopologicalSpace.Opens (Kn K m)) (x0 : K) {N : ℕ} (w : Fin N → ↑((sheafKn K m).presheaf.obj (Opposite.op V))) : ↑((sheafKn K (m + 1)).presheaf.obj (Opposite.op (baseOpens ψ V)))

Σ_k (w k ∘ π) (x_0 − x₀)^k: a polynomial section of degree < N in the shifted coordinate.

Equations

• AnalyticSpace.polyComb ψ V x0 w = ∑ k : Fin N, AnalyticSpace.pullSec ψ V (w k) * AnalyticSpace.shiftSec ψ V x0 ^ ↑k

noncomputable def AnalyticSpace.polyMonic {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (V : TopologicalSpace.Opens (Kn K m)) (x0 : K) (e : ℕ) (c : Fin e → ↑((sheafKn K m).presheaf.obj (Opposite.op V))) : ↑((sheafKn K (m + 1)).presheaf.obj (Opposite.op (baseOpens ψ V)))

(x_0 − x₀)^e + Σ_j (c j ∘ π) (x_0 − x₀)^{e−1−j}: a monic polynomial section of degree e, the shape of weierstrassPoly e c.

Equations

• AnalyticSpace.polyMonic ψ V x0 e c = AnalyticSpace.shiftSec ψ V x0 ^ e + ∑ j : Fin e, AnalyticSpace.pullSec ψ V (c j) * AnalyticSpace.shiftSec ψ V x0 ^ (e - 1 - ↑j)

theorem AnalyticSpace.ofPoly_comp_X_sub_C {K : Type} [RCLike K] {m : ℕ} (P : Polynomial (MvPowerSeries (Fin m) K)) (s : K) : Analytic.ofPoly (P.comp (Polynomial.X - Polynomial.C (MvPowerSeries.C s))) = Polynomial.eval₂ (Analytic.ofPolyHom.comp Polynomial.C) (MvPowerSeries.X 0 - MvPowerSeries.C s) P

theorem AnalyticSpace.ofPolyHom_comp_C {K : Type} [RCLike K] {m : ℕ} (c : MvPowerSeries (Fin m) K) : (Analytic.ofPolyHom.comp Polynomial.C) c = Analytic.liftTail c

theorem AnalyticSpace.ofPoly_polyOfCoeff_comp {K : Type} [RCLike K] {m N : ℕ} (c : Fin N → MvPowerSeries (Fin m) K) (s : K) : Analytic.ofPoly ((polyOfCoeff c).comp (Polynomial.X - Polynomial.C (MvPowerSeries.C s))) = ∑ k : Fin N, Analytic.liftTail (c k) * (MvPowerSeries.X 0 - MvPowerSeries.C s) ^ ↑k

theorem AnalyticSpace.ofPoly_weierstrassPolynomial_comp {K : Type} [RCLike K] {m e : ℕ} (c : Fin e → MvPowerSeries (Fin m) K) (s : K) : Analytic.ofPoly ((Analytic.weierstrassPolynomial e c).comp (Polynomial.X - Polynomial.C (MvPowerSeries.C s))) = (MvPowerSeries.X 0 - MvPowerSeries.C s) ^ e + ∑ j : Fin e, Analytic.liftTail (c j) * (MvPowerSeries.X 0 - MvPowerSeries.C s) ^ (e - 1 - ↑j)

theorem AnalyticSpace.TKn_germ_polyComb {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) {V : TopologicalSpace.Opens (Kn K m)} {a : Kn K (m + 1)} (ha : a ∈ baseOpens ψ V) (x0 : K) {N : ℕ} (w : Fin N → ↑((sheafKn K m).presheaf.obj (Opposite.op V))) : (TKn ψ a) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (polyComb ψ V x0 w)) = Analytic.ofPoly ((polyOfCoeff fun (k : Fin N) => (TKn (knCoord K m) ((projKn ψ) a)) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V ((projKn ψ) a) ha)) (w k))).comp (Polynomial.X - Polynomial.C (MvPowerSeries.C (x0 - ψ a 0))))

The Taylor series at a ∈ π⁻¹ V of a polynomial combination: the polynomial with the Taylor series of the coefficients at π a, composed with the shift X − C (x₀ − a_0).

theorem AnalyticSpace.TKn_germ_polyMonic {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) {V : TopologicalSpace.Opens (Kn K m)} {a : Kn K (m + 1)} (ha : a ∈ baseOpens ψ V) (x0 : K) (e : ℕ) (c : Fin e → ↑((sheafKn K m).presheaf.obj (Opposite.op V))) : (TKn ψ a) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (polyMonic ψ V x0 e c)) = Analytic.ofPoly ((Analytic.weierstrassPolynomial e fun (j : Fin e) => (TKn (knCoord K m) ((projKn ψ) a)) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V ((projKn ψ) a) ha)) (c j))).comp (Polynomial.X - Polynomial.C (MvPowerSeries.C (x0 - ψ a 0))))

The Taylor series at a ∈ π⁻¹ V of a monic polynomial section: weierstrassPolynomial e (T c) composed with the shift, monic of degree e at every point.

theorem AnalyticSpace.monic_weierstrassPolynomial_comp {K : Type} [RCLike K] {m e : ℕ} (c : Fin e → MvPowerSeries (Fin m) K) (s : K) : ((Analytic.weierstrassPolynomial e c).comp (Polynomial.X - Polynomial.C (MvPowerSeries.C s))).Monic

theorem AnalyticSpace.natDegree_weierstrassPolynomial_comp {K : Type} [RCLike K] {m e : ℕ} (c : Fin e → MvPowerSeries (Fin m) K) (s : K) : ((Analytic.weierstrassPolynomial e c).comp (Polynomial.X - Polynomial.C (MvPowerSeries.C s))).natDegree = e

theorem AnalyticSpace.comp_X_sub_C_eq_zero_iff {R : Type u_1} [CommRing R] (P : Polynomial R) (r : R) : P.comp (Polynomial.X - Polynomial.C r) = 0 ↔ P = 0

Composition with X − C r is injective on polynomials.

theorem AnalyticSpace.ofPoly_injective {K : Type} [RCLike K] {m : ℕ} : Function.Injective Analytic.ofPoly

theorem AnalyticSpace.germ_polyComb_eq_zero_iff {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) {V : TopologicalSpace.Opens (Kn K m)} {a : Kn K (m + 1)} (ha : a ∈ baseOpens ψ V) (x0 : K) {N : ℕ} (w : Fin N → ↑((sheafKn K m).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (polyComb ψ V x0 w) = 0 ↔ ∀ (k : Fin N), (CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V ((projKn ψ) a) ha)) (w k) = 0

Coefficient extraction: a polynomial combination has germ 0 at a iff every coefficient has germ 0 at π a.