Documentation

Hironaka.AnalyticSpace.Oka.Core

The core step of Oka's theorem on the model #

After the preparation theorem, the entries F_1, …, F_p of the row are Weierstrass polynomials at the origin and normalized polynomials of degree < d at every other point of U = V Γ— (βˆ’r, r); the row F then induces an π’ͺ(V)-linear map π’ͺ(V)[z_n : m]^p β†’ π’ͺ(V)[z_n : m + d] between polynomials of bounded degree, whose kernel is finitely generated by the induction hypothesis, and Oka's lemma turns this into the finite generation of the kernel system of F Fre17, Ch. I, 10.3, third step of the proof.

hasLocalGeneratorsOn_polyRow is that step. For a row P_j = polyComb V xβ‚€ (pc j) of polynomial sections of degree < d in the shifted coordinate over π⁻¹ V, with P_0 monic of degree e < d at every point of V: if the relations of the coefficient matrix coeffMatSec pc (d + 3d) (3d) over the base are locally finitely generated on V (the induction hypothesis in dimension m), then the relations of the row are locally finitely generated on π⁻¹ V. At a ∈ π⁻¹ V, generators A^{(l)} of the base kernel near Ο€ a give the polynomial sections R^{(l)}_j = Ξ£_t A^{(l)}_{(j,t)} (x_0 βˆ’ xβ‚€)^t; they are relations, by the coefficient correspondence of Hironaka.AnalyticSpace.Oka.Coeff, and they generate: a relation b at a point a' is, on the Taylor side, in the span over the convergent series of the relations of x_0-degree < 3d (Oka's lemma, rowKer_le_span_degLt), each of which is Ξ¨_{a'} of a polynomial vector of degree < 3d (exists_psi_eq_of_degLt) whose coefficient vector is a base relation, hence a combination of the A^{(l)}. Every step follows Freitag's text.

source
noncomputable def AnalyticSpace.polyRow {K : Type} [RCLike K] {m : β„•} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) β†’ K) (V : TopologicalSpace.Opens (Kn K m)) (x0 : K) {q d : β„•} (pc : Fin q β†’ Fin d β†’ ↑((sheafKn K m).presheaf.obj (Opposite.op V))) :
Fin q β†’ ↑((sheafKn K (m + 1)).presheaf.obj (Opposite.op (baseOpens ψ V)))

The row j ↦ Ξ£_t (pc j t ∘ Ο€) (x_0 βˆ’ xβ‚€)^t of polynomial sections over π⁻¹ V.

Equations
Instances For
    source
    theorem AnalyticSpace.germ_polyRow {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) {q d : β„•} (pc : Fin q β†’ Fin d β†’ ↑((sheafKn K m).presheaf.obj (Opposite.op V))) (j : Fin q) :
    (CategoryTheory.ConcreteCategory.hom ((sheafKn K (m + 1)).presheaf.germ (baseOpens ψ V) a ha)) (polyRow ψ V x0 pc j) = (psi ψ a x0) (polyOfCoeff fun (t : Fin d) => (CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V ((projKn ψ) a) ha)) (pc j t))
    source
    theorem AnalyticSpace.baseOpens_mono {K : Type} [RCLike K] {m : β„•} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) β†’ K) {V V' : TopologicalSpace.Opens (Kn K m)} (h : V' ≀ V) :
    baseOpens ψ V' ≀ baseOpens ψ V
    source
    @[reducible, inline]
    abbrev AnalyticSpace.rowKerR {R : Type u_1} [CommRing R] {p : β„•} (G : Fin p β†’ R) :
    Submodule R (Fin p β†’ R)

    The relations of a row over any commutative ring (the kernel of a 1 Γ— p matrix, relKer).

    Equations
    Instances For
      source
      theorem AnalyticSpace.mem_rowKerR_iff {R : Type u_1} [CommRing R] {p : β„•} (G P : Fin p β†’ R) :
      P ∈ rowKerR G ↔ βˆ‘ j : Fin p, G j * P j = 0
      source
      theorem AnalyticSpace.polyOfCoeff_sum_mul {R : Type u_1} [CommRing R] {N k : β„•} (lam : Fin k β†’ R) (c : Fin k β†’ Fin N β†’ R) :
      (polyOfCoeff fun (t : Fin N) => βˆ‘ l : Fin k, lam l * c l t) = βˆ‘ l : Fin k, Polynomial.C (lam l) * polyOfCoeff (c l)

      polyOfCoeff of a linear combination of coefficient vectors.

      source
      theorem AnalyticSpace.hasLocalGeneratorsOn_polyRow {K : Type} [RCLike K] {m : β„•} (ψ : Kn K (m + 1) ≃L[K] Fin (m + 1) β†’ K) {q d e : β„•} (hd : 0 < d) (he : e < d) (V : TopologicalSpace.Opens (Kn K m)) (x0 : K) (pc : Fin (q + 1) β†’ Fin d β†’ ↑((sheafKn K m).presheaf.obj (Opposite.op V))) (hmonic : βˆ€ (b : Kn K m) (hb : b ∈ V), (polyOfCoeff fun (t : Fin d) => (CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V b hb)) (pc 0 t)).Monic ∧ (polyOfCoeff fun (t : Fin d) => (CategoryTheory.ConcreteCategory.hom ((sheafKn K m).presheaf.germ V b hb)) (pc 0 t)).natDegree = e) (hIH : Manifold.HasLocalGeneratorsOn (sheafKn K m) V ((q + 1) * (3 * d)) fun (b : ↑↧(Kn K m)) (hb : b ∈ V) => Manifold.relationSubmodule (sheafKn K m) (coeffMatSec pc (d + 3 * d) (3 * d)) b hb) :
      Manifold.HasLocalGeneratorsOn (sheafKn K (m + 1)) (baseOpens ψ V) (q + 1) fun (a : ↑↧(Kn K (m + 1))) (ha : a ∈ baseOpens ψ V) => Manifold.relationSubmodule (sheafKn K (m + 1)) (fun (x : Fin 1) => polyRow ψ V x0 pc) a ha

      The third step of the proof of Oka's theorem [Fre17, Ch. I, 10.3]: the relations of a row of polynomial sections of degree < d (the first one monic of degree e < d at every point) are locally finitely generated on π⁻¹ V, given that the relations of the coefficient matrix over the base are locally finitely generated on V.