Auxiliary lemmas for the induction of Oka's theorem

Bookkeeping for Hironaka.AnalyticSpace.Oka.Main: membership in a finite infimum of open sets, composed restrictions of sections and the agreement on a neighbourhood of two sections with the same germ (exists_res_eq_of_germ_eq), the Weierstrass polynomial as the polynomial of a padded coefficient list (weierstrassList, polyOfCoeff_weierstrassList), the regularity in x_0 of the factors of a finite product (isRegularIn_of_mul iterated), and the restriction of a row's relation system to a smaller open set and back (hasLocalGeneratorsOn_row_res, hasLocalGeneratorsOn_row_of_res). None of this is in the sources as a separate statement.

theorem AnalyticSpace.mem_finset_inf_opens {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} (s : Finset ι) (f : ι → TopologicalSpace.Opens X) {x : X} (h : ∀ i ∈ s, x ∈ f i) : x ∈ s.inf f

A point lying in every member of a finite family of opens lies in their infimum.

theorem AnalyticSpace.finset_inf_opens_le {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} (s : Finset ι) (f : ι → TopologicalSpace.Opens X) {i : ι} (hi : i ∈ s) : s.inf f ≤ f i

theorem AnalyticSpace.res_res_eq_res {X : TopCat} (F : TopCat.Sheaf CommRingCat X) {U V W : TopologicalSpace.Opens ↑X} (hVU : V ≤ U) (hWV : W ≤ V) (s : ↑(F.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE hWV).op)) ((CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE hVU).op)) s) = (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE ⋯).op)) s

Restricting twice is restricting once.

theorem AnalyticSpace.exists_res_eq_of_germ_eq {X : TopCat} (F : TopCat.Sheaf CommRingCat X) {U : TopologicalSpace.Opens ↑X} {x : ↑X} (hx : x ∈ U) (s t : ↑(F.presheaf.obj (Opposite.op U))) (h : (CategoryTheory.ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (CategoryTheory.ConcreteCategory.hom (F.presheaf.germ U x hx)) t) : ∃ (W : TopologicalSpace.Opens ↑X) (hWU : W ≤ U) (_ : x ∈ W), (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE hWU).op)) s = (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE hWU).op)) t

Two sections with the same germ at x agree after restriction to some open neighbourhood of x.

def AnalyticSpace.weierstrassList {R : Type u_1} [CommRing R] (e : ℕ) (c : Fin e → R) (d : ℕ) : Fin d → R

The coefficient list of weierstrassPolynomial e c padded to length d > e: x_0^e + Σ_j c_j x_0^{e−1−j} has coefficient 1 at e, c_{e−1−t} at t < e, and 0 above e.

Equations

• AnalyticSpace.weierstrassList e c d t = if h : ↑t < e then c ⟨e - 1 - ↑t, ⋯⟩ else if ↑t = e then 1 else 0

theorem AnalyticSpace.polyOfCoeff_weierstrassList {R : Type u_1} [CommRing R] [Nontrivial R] {e d : ℕ} (he : e < d) (c : Fin e → R) : polyOfCoeff (weierstrassList e c d) = Analytic.weierstrassPolynomial e c

theorem AnalyticSpace.map_weierstrassList {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (e : ℕ) (c : Fin e → R) (d : ℕ) (t : Fin d) : f (weierstrassList e c d t) = weierstrassList e (fun (j : Fin e) => f (c j)) d t

The list is natural in ring homomorphisms.

theorem AnalyticSpace.exists_isRegularIn_of_prod {K : Type u_1} [RCLike K] {m : ℕ} {ι : Type u_2} (s : Finset ι) (f : ι → MvPowerSeries (Fin (m + 1)) K) {d : ℕ} (h : Analytic.IsRegularIn (∏ i ∈ s, f i) d) {i : ι} (hi : i ∈ s) : ∃ (d' : ℕ), Analytic.IsRegularIn (f i) d'

The factors of an x_0-regular finite product are x_0-regular (isRegularIn_of_mul).

theorem AnalyticSpace.hasLocalGeneratorsOn_row_res {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U W : TopologicalSpace.Opens ↑X} (hWU : W ≤ U) {p : ℕ} (g : Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) (h : Manifold.HasLocalGeneratorsOn 𝒪 U p fun (y : ↑X) (hy : y ∈ U) => Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) => g) y hy) : Manifold.HasLocalGeneratorsOn 𝒪 W p fun (y : ↑X) (hy : y ∈ W) => Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) (j : Fin p) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map (CategoryTheory.homOfLE hWU).op)) (g j)) y hy

Restricting a row's relation system to a smaller open.

theorem AnalyticSpace.hasLocalGeneratorsOn_row_of_res {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U W : TopologicalSpace.Opens ↑X} (hWU : W ≤ U) {x : ↑X} (hx : x ∈ W) {p : ℕ} (g : Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) (h : Manifold.HasLocalGeneratorsOn 𝒪 W p fun (y : ↑X) (hy : y ∈ W) => Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) (j : Fin p) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.map (CategoryTheory.homOfLE hWU).op)) (g j)) y hy) : ∃ (V : TopologicalSpace.Opens ↑X) (hVU : V ≤ U) (_ : x ∈ V) (k : ℕ) (r : Fin k → Fin p → ↑(𝒪.presheaf.obj (Opposite.op V))), ∀ (y : ↑X) (hy : y ∈ V), Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) => g) y ⋯ = Submodule.span (↑(𝒪.presheaf.stalk y)) (Set.range fun (l : Fin k) (j : Fin p) => (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ V y hy)) (r l j))

Conversely, local generators for the restricted row at x are local generators for the row.