Reductions for the induction of Oka's theorem

Freitag's third step [Fre17, Ch. I, 10.3, proof] first makes the entries F_1, …, F_p of the row z_n-general at the origin by a linear change of coordinates, then Weierstrass polynomials by the preparation theorem. This module provides the reductions the induction of Hironaka.AnalyticSpace.Oka.Main uses at a point x:

• TKn_trans: the Taylor series in the coordinates L ∘ knCoord is the substitution substConv L⁻¹ of the Taylor series in the ULift coordinates, so that the linear change of coordinates is a choice of ψ in the modules on Oka's theorem;
• exists_isUnit_res_of_isUnit_germ: a section whose germ is a unit is a unit on a neighbourhood (in any sheaf of rings);
• hasLocalGeneratorsOn_row_mul_units: local generators of the relations of (u_j g_j)_j, for unit sections u_j, from those of (g_j)_j (the units of the preparation theorem);
• hasLocalGeneratorsOn_row_comp_perm: local generators of the relations of a row from those of a permuted row (the monic entry is put first);
• hasLocalGeneratorsOn_row_zero: the relations of a zero row are everything, generated by the unit vectors.

The relation system of a row g is relationSubmodule 𝒪 (fun _ : Fin 1 => g), the kernel system of the 1 × p matrix g (Hironaka.AnalyticSpace.Coherent), and HasLocalGeneratorsOn says that it is locally finitely generated by germs of sections. None of this is in the sources as a separate statement.

theorem AnalyticSpace.TKn_trans {K : Type} [RCLike K] {n : ℕ} (L : (Fin n → K) ≃L[K] Fin n → K) (a : Kn K n) (s : ↑((sheafKn K n).presheaf.stalk a)) : (TKn ((knCoord K n).trans L) a) s = ↑(Analytic.substConv ↑L.symm ⟨(TKn (knCoord K n) a) s, ⋯⟩)

Freitag's "linear coordinate transformation" [Fre17, Ch. I, 10.3]: the Taylor series in the coordinates L ∘ knCoord is substConv L⁻¹ of the Taylor series in the ULift coordinates.

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

A section whose germ at x is a unit is a unit on a neighbourhood of x.

theorem AnalyticSpace.mem_relationSubmodule_row_iff {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p : ℕ} (g : Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) {y : ↑X} (hy : y ∈ U) (a : Fin p → ↑(𝒪.presheaf.stalk y)) : a ∈ Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) => g) y hy ↔ ∑ j : Fin p, (CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U y hy)) (g j) * a j = 0

A relation of a row: the sum form.

theorem AnalyticSpace.hasLocalGeneratorsOn_row_zero {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p : ℕ} (g : Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) (hg : ∀ (j : Fin p), g j = 0) : Manifold.HasLocalGeneratorsOn 𝒪 U p fun (y : ↑X) (hy : y ∈ U) => Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) => g) y hy

The relations of a zero row are everything, generated by the unit vectors.

theorem AnalyticSpace.hasLocalGeneratorsOn_row_comp_perm {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p : ℕ} (g : Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) (σ : Equiv.Perm (Fin p)) (h : Manifold.HasLocalGeneratorsOn 𝒪 U p fun (y : ↑X) (hy : y ∈ U) => Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) => g ∘ ⇑σ) y hy) : Manifold.HasLocalGeneratorsOn 𝒪 U p fun (y : ↑X) (hy : y ∈ U) => Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) => g) y hy

Relations of a permuted row give relations of the row.

theorem AnalyticSpace.hasLocalGeneratorsOn_row_mul_units {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {U : TopologicalSpace.Opens ↑X} {p : ℕ} (g u : Fin p → ↑(𝒪.presheaf.obj (Opposite.op U))) (hu : ∀ (j : Fin p), IsUnit (u j)) (h : Manifold.HasLocalGeneratorsOn 𝒪 U p fun (y : ↑X) (hy : y ∈ U) => Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) => g) y hy) : Manifold.HasLocalGeneratorsOn 𝒪 U p fun (y : ↑X) (hy : y ∈ U) => Manifold.relationSubmodule 𝒪 (fun (x : Fin 1) (j : Fin p) => u j * g j) y hy

Relations of (u_j g_j)_j for unit sections u_j from those of (g_j)_j.