Two charts (x₁, y) and (x₁', y) with a common complement

Kollár's coordinates in the proof of the uniqueness of maximal contact [Kol07, 95]: at p ∈ H ∩ H' he picks local sections x₁, x₁' ∈ MC(I) with H = (x₁ = 0) and H' = (x₁' = 0), further coordinates x₂, …, x_{s+1} with Eⁱ = (x_{i+1} = 0), and observes that "for a general choice of x_{s+2}, …, xₙ" both x₁, x₂, …, xₙ and x₁', x₂, …, xₙ are local coordinate systems. The ring-level version of this linear algebra (Hironaka/Algebra/Local/RegularSystemCommon.lean) is carried to the analytic stalk through the linear parts of germs (linearPart, Hironaka/Manifold/Chart/Cotangent.lean) in a base chart:

• the snc chart φ of H + E at p gives coordinates z = ψ ∘ φ with H = {z_{i₀} = 0} and E^j = {z_{k j} = 0} on its source (exists_sncChart_append); the snc chart φ' of H' + E gives x₁' = z'_{i₀'} and the same components as {z'_{k' j} = 0};
• the linear part v of x₁' in the chart φ does not lie in the span of the e_{k j} (linearPart_notMem_span_of_isSncChartAt): the equations z_{k j} and z'_{k' j} of one component generate the same vanishing ideal, so their linear parts are proportional (linearPart_mul_of_mem_maximalIdeal), and in φ' the family x₁', z'_{k' j} has independent linear parts (distinct coordinates), a property independent of the chart (linearIndependent_cotangentClass_iff_linearPart);
• hence some free index m₀ ∉ {k j} has v_{m₀} ≠ 0: if v_{i₀} ≠ 0 no tilt is needed, otherwise the coordinate z_{m₀} is tilted to z_{m₀} + z_{i₀} (Kollár's "general choice"; the protected coordinates z_{k j} are untouched); the tilted family and the family with z_{i₀} replaced by x₁' both span the cotangent space, hence have independent differentials, and the chart-extension theorem exists_chart_extending turns each into a chart of the maximal atlas centred at p; the second is recoordinatised by a permutation so that the two charts share the coordinates ≠ i₀ (exists_commonCharts).

The two charts are the input of the coordinate swap that realises the formal equivalence of H and H' (Hironaka/Resolution/Analytic/MaximalContact/SwapRealizes.lean).

Linear parts: products with a germ of 𝔪, and coordinate families

theorem Hironaka.Manifold.linearPart_mul_of_mem_maximalIdeal {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (r : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) {s : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)} (hs : s ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk a)) : (Manifold.linearPart E ψ φ hφ ha) (r * s) = (Manifold.eval 𝕜 E M a) r • (Manifold.linearPart E ψ φ hφ ha) s

The linear part of r · s for s ∈ 𝔪_a is r(a) times the linear part of s.

theorem Hironaka.Manifold.linearPart_coord_eq_single {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (k : Fin n) : (Manifold.linearPart E ψ φ hφ ha) (Manifold.coord E ψ φ hφ ha k) = Pi.single k 1

The linear part of the coordinate germ z_k is the unit vector e_k.

theorem Hironaka.Manifold.linearIndependent_linearPart_coord {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {ι : Type u_2} (idx : ι → Fin n) (hidx : Function.Injective idx) : LinearIndependent 𝕜 fun (o : ι) => (Manifold.linearPart E ψ φ hφ ha) (Manifold.coord E ψ φ hφ ha (idx o))

Distinct coordinate germs of a chart have linearly independent linear parts.

The snc chart of E + H at a point of H, unpacked

theorem Hironaka.Manifold.exists_sncChart_append {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {F : Manifold.HypersurfaceFamily M} {H : Set M} (hHF : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H)) {p : M} (hpH : p ∈ H) : ∃ (φ : OpenPartialHomeomorph M E) (_ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (_ : p ∈ φ.source) (i₀ : Fin n) (k : { j : F.ι // p ∈ F.hyp j } → Fin n), (∀ x ∈ φ.source, x ∈ H ↔ ψ (↑φ x) i₀ = 0) ∧ (∀ (j : { j : F.ι // p ∈ F.hyp j }), ∀ x ∈ φ.source, x ∈ F.hyp ↑j ↔ ψ (↑φ x) (k j) = 0) ∧ (∀ (j : { j : F.ι // p ∈ F.hyp j }), k j ≠ i₀) ∧ Function.Injective k

An snc chart of the family F.append H at p ∈ H reads H as the coordinate hyperplane of an index i₀ and every component E^j through p as the hyperplane of an index k j ≠ i₀, the k j distinct.

The linear part of x₁' is transverse to the components through p

theorem Hironaka.Manifold.linearPart_mem_span_of_span_singleton_eq {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {p : M} {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hp : p ∈ φ.source) {a b : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk p)} (hb : b ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk p)) (h : Ideal.span {a} = Ideal.span {b}) : (Manifold.linearPart E ψ φ hφ hp) a ∈ 𝕜 ∙ (Manifold.linearPart E ψ φ hφ hp) b

The equation z_k of a component in one adapted chart is a unit multiple of its equation in another: their linear parts (in any chart) are proportional. Here span {a} = span {b} for two germs of 𝔪_p, and the linear part of a is a multiple of that of b.

theorem Hironaka.Manifold.linearPart_notMem_span_of_isSncChartAt {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {F : Manifold.HypersurfaceFamily M} {p : M} {φ φ' : OpenPartialHomeomorph M E} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hp : p ∈ φ.source) {k : { j : F.ι // p ∈ F.hyp j } → Fin n} (hk : ∀ (j : { j : F.ι // p ∈ F.hyp j }), ∀ x ∈ φ.source, x ∈ F.hyp ↑j ↔ ψ (↑φ x) (k j) = 0) (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hp' : p ∈ φ'.source) {i₀' : Fin n} {k' : { j : F.ι // p ∈ F.hyp j } → Fin n} (hk' : ∀ (j : { j : F.ι // p ∈ F.hyp j }), ∀ x ∈ φ'.source, x ∈ F.hyp ↑j ↔ ψ (↑φ' x) (k' j) = 0) (hk'i : ∀ (j : { j : F.ι // p ∈ F.hyp j }), k' j ≠ i₀') (hk'inj : Function.Injective k') : (Manifold.linearPart E ψ φ hφ hp) (Manifold.coord E ψ φ' hφ' hp' i₀') ∉ Submodule.span 𝕜 (Set.range fun (j : { j : F.ι // p ∈ F.hyp j }) => Pi.single (k j) 1)

In the snc chart φ of E + H at p (components E^j = {z_{k j} = 0}), the linear part of the equation x₁' of H' taken from an snc chart φ' of E + H' does not lie in the span of the unit vectors e_{k j} (the hypothesis that H' + E has simple normal crossings, [Kol07, Theorem 92]).

The free index: where to tilt

theorem Hironaka.Manifold.exists_free_index {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u_2} (k : ι → Fin n) (i₀ : Fin n) (hk : ∀ (j : ι), k j ≠ i₀) (v : Fin n → 𝕜) (hv : v ∉ Submodule.span 𝕜 (Set.range fun (j : ι) => Pi.single (k j) 1)) : ∃ (m₀ : Fin n), (∀ (j : ι), k j ≠ m₀) ∧ v m₀ ≠ 0 ∧ (v i₀ ≠ 0 → m₀ = i₀)

Kollár's "general choice" [Kol07, 95]: a vector v outside the span of the unit vectors e_{k j} has a nonzero coordinate at some index m₀ off the k j; take m₀ = i₀ when v_{i₀} ≠ 0.

Two families of vectors of 𝕜ⁿ: the tilted basis and the basis with one vector replaced

theorem Hironaka.Manifold.linearIndependent_tilt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (i₀ m₀ : Fin n) : LinearIndependent 𝕜 fun (m : Fin n) => Pi.single m 1 + if m = m₀ ∧ m₀ ≠ i₀ then Pi.single i₀ 1 else 0

The tilted family e_m + [m = m₀ ∧ m₀ ≠ i₀] e_{i₀} is a basis of 𝕜ⁿ.

theorem Hironaka.Manifold.linearIndependent_update_tilt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (i₀ m₀ : Fin n) (v : Fin n → 𝕜) (hvm : v m₀ ≠ 0) (hvi : m₀ ≠ i₀ → v i₀ = 0) : LinearIndependent 𝕜 (Function.update (fun (m : Fin n) => Pi.single m 1 + if m = m₀ ∧ m₀ ≠ i₀ then Pi.single i₀ 1 else 0) i₀ v)

The tilted family with the vector at i₀ replaced by v, where v_{m₀} ≠ 0 and v_{i₀} = 0 unless m₀ = i₀, is a basis of 𝕜ⁿ (Kollár's "x₁', x₂, …, xₙ are local coordinates").

Germs of coordinates and of sections, compared through their representatives

theorem Hironaka.Manifold.stalkToGerm_germ_sectionOf {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {p : M} {W : TopologicalSpace.Opens M} (hpW : p ∈ W) (f : M → 𝕜) (hf : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ f ↑W) : (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M p) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M).presheaf.germ W p hpW)) (Manifold.sectionOfContMDiffOn f W hf)) = ↑f

The germ of a section built from a function is the germ of the function.

theorem Hironaka.Manifold.stalkToGerm_coord_eq {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {p : M} {e : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hpe : p ∈ e.source) (i : Fin n) : (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M p) (Manifold.coord E ψ e he hpe i) = ↑fun (x : M) => ψ (↑e x) i

The germ of a chart coordinate is the germ of the coordinate function.

theorem Hironaka.Manifold.coord_eq_coord_of_eventuallyEq {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {p : M} {e e' : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hpe : p ∈ e.source) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hpe' : p ∈ e'.source) {i i' : Fin n} (h : ∀ᶠ (x : M) in nhds p, ψ (↑e x) i = ψ (↑e' x) i') : Manifold.coord E ψ e he hpe i = Manifold.coord E ψ e' he' hpe' i'

Two chart coordinates whose functions agree near p have the same germ.

The charts (x₁, y) and (x₁', y)

theorem Hironaka.Manifold.exists_commonCharts {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] {F : Manifold.HypersurfaceFamily M} {H H' : Set M} {p : M} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hH : Manifold.IsClosedSubmanifold ψ H 1) (hH' : Manifold.IsClosedSubmanifold ψ H' 1) (hHF : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H)) (hH'F : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H')) (hpH : p ∈ H) (hpH' : p ∈ H') : ∃ (e : OpenPartialHomeomorph M E) (e' : OpenPartialHomeomorph M E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hpe : p ∈ e.source) (hpe' : p ∈ e'.source) (i₀ : Fin n), ↑e p = 0 ∧ ↑e' p = 0 ∧ (∀ (i : Fin n), i ≠ i₀ → Manifold.coord E ψ e he hpe i = Manifold.coord E ψ e' he' hpe' i) ∧ Manifold.vanishingStalk H p = Ideal.span {Manifold.coord E ψ e he hpe i₀} ∧ Manifold.vanishingStalk H' p = Ideal.span {Manifold.coord E ψ e' he' hpe' i₀} ∧ ∀ (j : F.ι), p ∈ F.hyp j → ∃ (l : Fin n), l ≠ i₀ ∧ Manifold.vanishingStalk (F.hyp j) p = Ideal.span {Manifold.coord E ψ e he hpe l}

Kollár's two coordinate systems x₁, x₂, …, xₙ and x₁', x₂, …, xₙ [Kol07, 95]: at p ∈ H ∩ H', with E + H and E + H' snc, there are two charts of the maximal atlas centred at p sharing all coordinates except the one of index i₀, in which H (resp. H') is the hyperplane {x_{i₀} = 0} — its vanishing ideal at p is generated by the i₀-th coordinate germ — and every component of E through p is a coordinate hyperplane of an index ≠ i₀.