The Taylor isomorphism on the model space Kⁿ and the projection to the base

The analogue over K of the third step of the proof of Oka's coherence theorem Fre17, Ch. I, 10.3, which Freitag carries out over ℂ, works at every point a of a product U = V × D ⊆ Kⁿ with the power series expansions at a and the projection U → V. On the model Kⁿ = Kn K n (the type ULift (Fin n → K), a manifold over itself, with sheafKn K n = 𝒜_{Kⁿ} its sheaf of analytic functions) this module fixes:

• taylorKn ψ a : 𝒜_{Kⁿ,a} ≃+* Conv K n, the Taylor isomorphism onto the convergent power series (taylorEquivConv) in the linear coordinates ψ and the identity chart, and TKn ψ a its underlying ring homomorphism into the formal power series (the Taylor homomorphism, characterised by IsTaylorHom); ψ = knCoord K n are the ULift coordinates, and ψ = L ∘ knCoord a linear change of coordinates;
• the projection projKn ψ : Kn K (m + 1) →L[K] Kn K m forgetting the distinguished coordinate x_0 = ψ_0 (Fin.tail in coordinates; analytic as a continuous linear map);
• the Taylor series of the constants (TKn_const), of the centred coordinates (TKn_coord_sub_const: x_i − x_i(a) ↦ X_i), and of a section pulled back from the base along the projection (TKn_germ_comapSection: T_a (g ∘ π) = liftTail (T_{π a} g), by the uniqueness of the power series of a germ, eq_of_evalSeries_sub_eventuallyEq, and evalSeries_liftTail).

Every statement here is bookkeeping for the induction of Hironaka.AnalyticSpace.Oka.Main.

@[reducible, inline]

abbrev AnalyticSpace.knCoord (K : Type) [RCLike K] (n : ℕ) : Kn K n ≃L[K] Fin n → K

The coordinates of Kⁿ = ULift (Fin n → K): the forgetful linear isometry.

Equations

• AnalyticSpace.knCoord K n = ContinuousLinearEquiv.ulift

@[reducible, inline]

noncomputable abbrev AnalyticSpace.sheafKn (K : Type) [RCLike K] (n : ℕ) : TopCat.Sheaf CommRingCat ↧(Kn K n)

𝒜_{Kⁿ}, the sheaf of analytic functions of Kⁿ as a manifold over itself (the structure sheaf of the affine space affine K n).

Equations

• AnalyticSpace.sheafKn K n = Manifold.structureSheaf K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n)

noncomputable def AnalyticSpace.TKn {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) : ↑((sheafKn K n).presheaf.stalk a) →+* MvPowerSeries (Fin n) K

The Taylor homomorphism at a ∈ Kⁿ in the linear coordinates ψ and the identity chart (taylorHom); ψ = knCoord K n are the ULift coordinates, ψ = L ∘ knCoord a linear change of coordinates ("after a suitable linear coordinate transformation", [Fre17, Ch. I, 10.3]).

Equations

• AnalyticSpace.TKn ψ a = Manifold.taylorHom (AnalyticSpace.Kn K n) ψ (chartAt (AnalyticSpace.Kn K n) a) ⋯ ⋯

theorem AnalyticSpace.isTaylorHom_TKn {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) : Manifold.IsTaylorHom (Kn K n) ψ (chartAt (Kn K n) a) a (TKn ψ a)

theorem AnalyticSpace.TKn_mem_conv {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) (s : ↑((sheafKn K n).presheaf.stalk a)) : (TKn ψ a) s ∈ Analytic.Conv K n

noncomputable def AnalyticSpace.taylorKn {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) : ↑((sheafKn K n).presheaf.stalk a) ≃+* ↥(Analytic.Conv K n)

The Taylor isomorphism 𝒜_{Kⁿ,a} ≃+* Conv K n in the coordinates ψ (taylorEquivConv on the model Kⁿ).

Equations

• AnalyticSpace.taylorKn ψ a = Manifold.taylorEquivConv (AnalyticSpace.Kn K n) ψ (chartAt (AnalyticSpace.Kn K n) a) ⋯ ⋯

theorem AnalyticSpace.taylorKn_apply_coe {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) (s : ↑((sheafKn K n).presheaf.stalk a)) : ↑((taylorKn ψ a) s) = (TKn ψ a) s

theorem AnalyticSpace.TKn_injective {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) : Function.Injective ⇑(TKn ψ a)

theorem AnalyticSpace.exists_TKn_eq {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) {c : MvPowerSeries (Fin n) K} (hc : c ∈ Analytic.Conv K n) : ∃ (s : ↑((sheafKn K n).presheaf.stalk a)), (TKn ψ a) s = c

Every convergent series is the Taylor series of a germ.

theorem AnalyticSpace.TKn_const {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) (c : K) : (TKn ψ a) ((Manifold.const K (Kn K n) (Kn K n) a) c) = MvPowerSeries.C c

The Taylor series of a constant is the constant series.

noncomputable def AnalyticSpace.coordKn {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) (i : Fin n) : ↑((sheafKn K n).presheaf.stalk a)

The coordinate germ x_i = ψ_i at a (coord in the coordinates ψ).

Equations

• AnalyticSpace.coordKn ψ a i = Manifold.coord (AnalyticSpace.Kn K n) ψ (chartAt (AnalyticSpace.Kn K n) a) ⋯ ⋯ i

theorem AnalyticSpace.eval_coordKn {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) (i : Fin n) : (Manifold.eval K (Kn K n) (Kn K n) a) (coordKn ψ a i) = ψ a i

theorem AnalyticSpace.TKn_coord_sub_const {K : Type} [RCLike K] {n : ℕ} (ψ : Kn K n ≃L[K] Fin n → K) (a : Kn K n) (i : Fin n) : (TKn ψ a) (coordKn ψ a i - (Manifold.const K (Kn K n) (Kn K n) a) (ψ a i)) = MvPowerSeries.X i

The Taylor series of the centred coordinate x_i − a_i is X_i.

def AnalyticSpace.tailProjCLM (K : Type) [RCLike K] (m : ℕ) : (Fin (m + 1) → K) →L[K] Fin m → K

Forgetting the first coordinate, Fin.tail, as a continuous linear map over K.

Equations

• AnalyticSpace.tailProjCLM K m = ContinuousLinearMap.pi fun (i : Fin m) => ContinuousLinearMap.proj i.succ

theorem AnalyticSpace.tailProjCLM_apply (K : Type) [RCLike K] (m : ℕ) (y : Fin (m + 1) → K) : (tailProjCLM K m) y = Fin.tail y

def AnalyticSpace.projKn {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) : Kn K (m + 1) →L[K] Kn K m

The projection Kᵐ⁺¹ → Kᵐ forgetting the distinguished coordinate x_0 = ψ_0, as a continuous linear map (the projection V × (−r, r) → V of [Fre17, Ch. I, 10.3]); the base carries the ULift coordinates.

Equations

• AnalyticSpace.projKn ψ = ↑(AnalyticSpace.knCoord K m).symm ∘SL AnalyticSpace.tailProjCLM K m ∘SL ↑ψ

theorem AnalyticSpace.projKn_apply {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (y : Kn K (m + 1)) : (projKn ψ) y = { down := Fin.tail (ψ y) }

theorem AnalyticSpace.down_projKn {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (y : Kn K (m + 1)) : ((projKn ψ) y).down = Fin.tail (ψ y)

theorem AnalyticSpace.contMDiff_projKn {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) : ContMDiff (modelWithCornersSelf K (Kn K (m + 1))) (modelWithCornersSelf K (Kn K m)) ⊤ ⇑(projKn ψ)

theorem AnalyticSpace.extendSection_comapSection {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) {U : TopologicalSpace.Opens (Kn K m)} (g : ↑((sheafKn K m).presheaf.obj (Opposite.op U))) (x : Kn K (m + 1)) : Manifold.extendSection K (Kn K (m + 1)) (Manifold.comapSection ⇑(projKn ψ) ⋯ g) x = Manifold.extendSection K (Kn K m) g ((projKn ψ) x)

The extension by zero of a pulled-back section is the pulled-back extension.

theorem AnalyticSpace.TKn_germ_comapSection {K : Type} [RCLike K] {m : ℕ} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) → K) (a : Kn K (m + 1)) {U : TopologicalSpace.Opens (Kn K m)} (hU : (projKn ψ) a ∈ U) (g : ↑((sheafKn K m).presheaf.obj (Opposite.op U))) : (TKn ψ a) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (Manifold.preimageOpens ⇑(projKn ψ) ⋯ U) a ⋯)) (Manifold.comapSection ⇑(projKn ψ) ⋯ g)) = Analytic.liftTail ((TKn (knCoord K m) ((projKn ψ) a)) ((CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ U ((projKn ψ) a) hU)) g))

The Taylor series at a (coordinates ψ) of a section pulled back from the base along the projection is the lift of its Taylor series at π a (coefficients "independent of z_n", Fre17, Ch. I, 10.3).