The polynomial map from the base stalk into the stalk of the model

Freitag's subring 𝒪_{n−1}[z_n] ⊆ 𝒪_n at a point a of the product V × D Fre17, Ch. I, 10.3 and 10.4, as the ring homomorphism Ψ_a : 𝒪_{Kᵐ, π a}[X] →+* 𝒪_{Kᵐ⁺¹, a} (psi ψ a x₀) evaluating a polynomial with coefficients in the base stalk, pulled back along the projection π by the map of germs germMapProj, at the shifted coordinate x_0 − x₀:

• TKn_germMap: the Taylor series of a pulled-back stalk element is the lift of its Taylor series;
• psi and TKn_psi: T_a (Ψ_a Q) = ofPoly ((Q.map T_{π a}).comp (X − C (x₀ − a_0))) (two ring homomorphisms agreeing on constants and on X), hence psi_injective;
• the germs of the polynomial sections of Hironaka.AnalyticSpace.Oka.PolySection are Ψ_a of the polynomials with the germs of their coefficients (germ_polyComb_eq_psi, germ_polyMonic_eq_psi);
• exists_psi_eq_of_degLt: for 0 < N, every stalk element whose Taylor series has x_0-degree < N is Ψ_a Q for a polynomial Q of degree < N, the identification K_N = 𝒪_{n−1}[z_n : N]^p ∩ K in the statement of Oka's lemma [Fre17, Ch. I, 10.4].

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

@[reducible, inline]

noncomputable abbrev AnalyticSpace.germMapProj {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) : ↑((sheafKn K m).presheaf.stalk ((projKn ψ) a)) →+* ↑((sheafKn K (m + 1)).presheaf.stalk a)

The stalk map 𝒪_{Kᵐ, π a} →+* 𝒪_{Kᵐ⁺¹, a} of the projection.

Equations

• AnalyticSpace.germMapProj ψ a = Manifold.germMap ⇑(AnalyticSpace.projKn ψ) ⋯ a

theorem AnalyticSpace.TKn_germMap {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x : ↑((sheafKn K m).presheaf.stalk ((projKn ψ) a))) : (TKn ψ a) ((germMapProj ψ a) x) = Analytic.liftTail ((TKn (knCoord K m) ((projKn ψ) a)) x)

The Taylor series of a pulled-back stalk element is the lift of its Taylor series.

noncomputable def AnalyticSpace.shiftGerm {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x0 : K) : ↑((sheafKn K (m + 1)).presheaf.stalk a)

The shifted coordinate germ x_0 − x₀ at a.

Equations

• AnalyticSpace.shiftGerm ψ a x0 = AnalyticSpace.coordKn ψ a 0 - (Manifold.const K (AnalyticSpace.Kn K (m + 1)) (AnalyticSpace.Kn K (m + 1)) a) x0

theorem AnalyticSpace.TKn_shiftGerm {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x0 : K) : (TKn ψ a) (shiftGerm ψ a x0) = MvPowerSeries.X 0 - MvPowerSeries.C (x0 - ψ a 0)

theorem AnalyticSpace.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) : (CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (shiftSec ψ V x0) = shiftGerm ψ a x0

theorem AnalyticSpace.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))) : (CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (pullSec ψ V w) = (germMapProj ψ a) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V ((projKn ψ) a) ha)) w)

noncomputable def AnalyticSpace.psi {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x0 : K) : Polynomial ↑((sheafKn K m).presheaf.stalk ((projKn ψ) a)) →+* ↑((sheafKn K (m + 1)).presheaf.stalk a)

Freitag's 𝒪_{n−1}[z_n] → 𝒪_n at a [Fre17, Ch. I, 10.3]: evaluate a polynomial with coefficients in the base stalk (pulled back along π) at the shifted coordinate x_0 − x₀.

Equations

• AnalyticSpace.psi ψ a x0 = Polynomial.eval₂RingHom (AnalyticSpace.germMapProj ψ a) (AnalyticSpace.shiftGerm ψ a x0)

theorem AnalyticSpace.psi_C {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x0 : K) (x : ↑((sheafKn K m).presheaf.stalk ((projKn ψ) a))) : (psi ψ a x0) (Polynomial.C x) = (germMapProj ψ a) x

theorem AnalyticSpace.psi_X {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x0 : K) : (psi ψ a x0) Polynomial.X = shiftGerm ψ a x0

theorem AnalyticSpace.ofPoly_X_sub_C {K : Type} [RCLike K] {m : ℕ} (s : K) : Analytic.ofPoly (Polynomial.X - Polynomial.C (MvPowerSeries.C s)) = MvPowerSeries.X 0 - MvPowerSeries.C s

theorem AnalyticSpace.TKn_psi {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x0 : K) (Q : Polynomial ↑((sheafKn K m).presheaf.stalk ((projKn ψ) a))) : (TKn ψ a) ((psi ψ a x0) Q) = Analytic.ofPoly ((Polynomial.map (TKn (knCoord K m) ((projKn ψ) a)) Q).comp (Polynomial.X - Polynomial.C (MvPowerSeries.C (x0 - ψ a 0))))

The Taylor series of Ψ_a Q: the polynomial with the Taylor series of the coefficients, composed with the shift X − C (x₀ − a_0).

theorem AnalyticSpace.psi_injective {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x0 : K) : Function.Injective ⇑(psi ψ a x0)

theorem AnalyticSpace.germ_polyComb_eq_psi {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) = (psi ψ a x0) (∑ k : Fin N, Polynomial.C ((CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V ((projKn ψ) a) ha)) (w k)) * Polynomial.X ^ ↑k)

The germ of a polynomial combination is Ψ_a of the polynomial with the germs of the coefficients.

theorem AnalyticSpace.germ_polyMonic_eq_psi {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))) : (CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (polyMonic ψ V x0 e c) = (psi ψ a x0) (Analytic.weierstrassPolynomial e fun (j : Fin e) => (CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V ((projKn ψ) a) ha)) (c j))

The germ of a monic polynomial section is Ψ_a of the Weierstrass-shaped polynomial with the germs of the coefficients.

theorem AnalyticSpace.exists_psi_eq_of_degLt {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) (x0 : K) {N : ℕ} (hN : 0 < N) (b : ↑((sheafKn K (m + 1)).presheaf.stalk a)) (hb : Analytic.DegLt N ((TKn ψ a) b)) : ∃ (Q : Polynomial ↑((sheafKn K m).presheaf.stalk ((projKn ψ) a))), Q.natDegree < N ∧ (psi ψ a x0) Q = b

Freitag's identification K_N = 𝒪_{n−1}[z_n : N] ∩ K [Fre17, Ch. I, 10.4]: for 0 < N, a stalk element whose Taylor series has x_0-degree < N is Ψ_a Q for a polynomial Q over the base stalk of degree < N.