Oka's coherence theorem on the model Kⁿ

Oka's coherence theorem [Fre17, Ch. I, 10.3], [GR84, Ch. 2]: for an 𝒪(U)-linear map F : 𝒪(U)^p → 𝒪(U)^q on an open U ⊆ Kⁿ, the system of kernels M_a = ker F_a, a ∈ U, is coherent, that is, locally finitely generated by germs of sections (IsCoherent (sheafKn K n), isCoherent_sheafKn; for the affine space (Kⁿ, 𝒜_{Kⁿ}), oka_coherent). The proof follows Freitag's three steps: the reduction to one row (isCoherent_of_isCoherent_top, Hironaka.AnalyticSpace.CoherentLemmas), Oka's lemma at each point (Hironaka.Analytic.Oka.Lemma), and the induction on n, which is this module.

At a point x of U, a row g with all germs zero at x is zero near x (exists_res_eq_of_germ_eq), and the relations of a zero row are everything (hasLocalGeneratorsOn_row_zero); otherwise a nonzero entry is put first (hasLocalGeneratorsOn_row_comp_perm), "after a suitable linear coordinate transformation" (a choice of the coordinates ψ: TKn_trans and exists_substEquiv_isRegularIn applied to the product of the nonzero Taylor series) all nonzero entries are x_0-regular at x, and "by the preparation theorem" each is a unit times a Weierstrass polynomial (exists_unique_weierstrassPreparation), whose coefficients and unit are realized as sections near x (exists_TKn_eq, Mathlib's TopCat.Presheaf.exists_germ_eq). The polynomial row (polyRow) has locally finitely generated relations by the core step (hasLocalGeneratorsOn_polyRow, Hironaka.AnalyticSpace.Oka.Core, whose hypothesis hIH is the induction hypothesis on the base Kᵐ applied to the coefficient matrix), and the units and the identification of the sections near x transport this to the row g (hasLocalGeneratorsOn_row_mul_units, exists_res_eq_of_germ_eq). The base case n = 0 is a point: the relations form a finitely generated submodule of the Noetherian stalk, and every stalk element is the germ of a section. Freitag writes the proof over ℂ; it is carried out here over K = ℝ or ℂ at once, with the Weierstrass theorems of Hironaka.Analytic, which hold for both fields.

Oka's theorem on the model is the first ingredient of the coherence of the structure sheaf of every analytic K-space (Hironaka.AnalyticSpace.CoherentAnalytic), the property (3.8)(3) of [BM97] used throughout the analytic strand.

theorem AnalyticSpace.polyOfCoeff_zero {R : Type u_1} [CommRing R] (N : ℕ) : polyOfCoeff 0 = 0

theorem AnalyticSpace.weierstrassList_rev {R : Type u_1} [CommRing R] {e d : ℕ} (he : e < d) (c : Fin e → R) (s : Fin e) : weierstrassList e c d ⟨e - 1 - ↑s, ⋯⟩ = c s

Reading the Weierstrass coefficients back from the padded list.

theorem AnalyticSpace.isCoherent_sheafKn_zero {K : Type} [RCLike K] : Manifold.IsCoherent (sheafKn K 0)

The base case n = 0: K⁰ is a point, its stalk is Noetherian, and every stalk element is the germ of a section.

theorem AnalyticSpace.isCoherent_sheafKn_succ {K : Type} [RCLike K] (m : ℕ) (ih : Manifold.IsCoherent (sheafKn K m)) : Manifold.IsCoherent (sheafKn K (m + 1))

The induction step: coherence of 𝒜_{Kᵐ} gives coherence of 𝒜_{Kᵐ⁺¹} ([Fre17, Ch. I, 10.3], third step of the proof).

theorem AnalyticSpace.isCoherent_sheafKn {K : Type} [RCLike K] (n : ℕ) : Manifold.IsCoherent (sheafKn K n)

Oka's coherence theorem [Fre17, Ch. I, 10.3], [GR84, Ch. 2]: the sheaf 𝒜_{Kⁿ} of analytic functions on the model Kⁿ is coherent, for K = ℝ or ℂ and every n.

theorem AnalyticSpace.oka_coherent {K : Type} [RCLike K] (n : ℕ) : Manifold.IsCoherent (affine K n).𝒪

Oka's coherence theorem for the affine space (Kⁿ, 𝒜_{Kⁿ}) (affine K n): its structure sheaf is coherent.