Tools for the exponents of a step of the monomial phase

Facts used by Step2bExponent.lean:

• the stalk of the ideal sheaf of a closed submanifold at a point depends only on the submanifold near the point (IsClosedSubmanifold.stalkIdeal_idealSheaf_congr_nhds, by the span form of the stalk on an adapted chart shrunk to the neighbourhood);
• the order along a centre transports along a bijective ring homomorphism of stalks carrying both ideals (IdealSheaf.ordAlongIdeal_eq_of_map, the pointwise form of ordAlongIdeal_pullback_diffeomorph);
• the blow-down of a step is a local analytic isomorphism (isLocalDiffeomorph_stepπ): the centre has codimension one (exists_diffeomorph_of_codim_one; see the remarks after [Wlo09, Theorem 2.0.3]);
• the centre Z is open in its member (a union of components of E^j), so the strict transform of the top member lies over E^j ∖ Z (notMem_step2bCenter_of_mem_stepFamily_top);
• two distinct members of a simple normal crossing divisor through a point: the point lies in the closure of the first minus the second (mem_closure_hyp_diff_hyp_of_ne, along the coordinate line of the chart; the transversality of [Kol07, Definition 24] in the form the strict transform needs), so the strict transform of every other member under the blow-up is its whole preimage (stepFamily_hyp_inl_of_ne; the blow-up is an open map), and every strict transform agrees with the preimage off the exceptional divisor (stepFamily_hyp_inl_inter_compl, mem_strictTransform_iff_of_notMem).

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_congr_nhds {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y Y' : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hY' : IsClosedSubmanifold ψ Y' c) {a : M} (ha : a ∈ Y) {U : Set M} (hU : IsOpen U) (haU : a ∈ U) (hYY' : Y ∩ U = Y' ∩ U) : hY.idealSheaf.stalkIdeal a = hY'.idealSheaf.stalkIdeal a

The stalk at a of the ideal sheaf of a closed submanifold depends only on the submanifold near a: two closed submanifolds of the same codimension which agree on an open neighbourhood of a have the same stalk ideal there (the span form on an adapted chart shrunk to the neighbourhood is adapted to both).

theorem Manifold.IdealSheaf.ordAlongIdeal_eq_of_map {X : TopCat} {X' : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {𝒪' : TopCat.Sheaf CommRingCat X'} {a : ↑X} {a' : ↑X'} (f : ↑(𝒪.presheaf.stalk a) →+* ↑(𝒪'.presheaf.stalk a')) (hf : Function.Bijective ⇑f) (D J : IdealSheaf 𝒪) (D' J' : IdealSheaf 𝒪') (hD : D'.stalkIdeal a' = Ideal.map f (D.stalkIdeal a)) (hJ : J'.stalkIdeal a' = Ideal.map f (J.stalkIdeal a)) : D'.ordAlongIdeal J' a' = D.ordAlongIdeal J a

The order of J along D transports along a bijective ring homomorphism of stalks carrying both stalk ideals: inclusions and powers of ideals are preserved by Ideal.map along a bijection (the pointwise form of ordAlongIdeal_pullback_diffeomorph).

The positive locus is open in its member

theorem Hironaka.Manifold.BMOmod.exists_isOpen_inter_subset_positiveLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {j : T.F.ι} {x : M.carrier} (hx : x ∈ positiveLocus T j) : ∃ (U : Set M.carrier), IsOpen U ∧ x ∈ U ∧ U ∩ T.F.hyp j ⊆ positiveLocus T j

The positive locus is open in its member: near each of its points the member lies in the component of the point (exists_adaptedChart_source_inter_subset), which lies in the positive locus (connectedComponentIn_subset_Zminus1).

Two members through a point: the closure of the difference

theorem Hironaka.Manifold.BMOmod.mem_closure_hyp_diff_hyp_of_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {j k : T.F.ι} (hjk : k ≠ j) {y : M.carrier} (hyk : y ∈ T.F.hyp k) (hyj : y ∈ T.F.hyp j) : y ∈ closure (T.F.hyp k \ T.F.hyp j)

For two distinct members E^k, E^j of the simple normal crossing divisor through y, y lies in the closure of E^k ∖ E^j [Kol07, Definition 24]: in a chart at y the points φ⁻¹(φ y + ε e_j) (e_j the coordinate direction of E^j) lie on E^k, off E^j for ε ≠ 0, and tend to y.

The strict transforms under the Step 2b blow-up

theorem Hironaka.Manifold.BMOmod.isLocalDiffeomorph_stepπ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(stepπ T hfin hne)

The blow-down of a step is a local analytic isomorphism: its centre has codimension one (exists_diffeomorph_of_codim_one; the remarks after [Wlo09, Theorem 2.0.3]).

theorem Hironaka.Manifold.BMOmod.notMem_step2bCenter_of_mem_stepFamily_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {x' : (stepStage T hfin hne).carrier} (hx' : x' ∈ (stepFamily T hfin hne).hyp (toLex (Sum.inl (topMember T hfin hne)))) : (stepπ T hfin hne) x' ∉ step2bCenter T hfin hne

The strict transform of the TOP member lies over E^j \ Z: the positive locus Z is open in E^j, so no point of Z is a limit of points of E^j \ Z.

theorem Hironaka.Manifold.BMOmod.stepFamily_hyp_inl_of_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {k : T.F.ι} (hk : k ≠ topMember T hfin hne) : (stepFamily T hfin hne).hyp (toLex (Sum.inl k)) = ⇑(stepπ T hfin hne) ⁻¹' T.F.hyp k

Under the blow-up of a step (an open map) the strict transform of every other member is its whole preimage: E^k ∖ Z is dense in E^k (mem_closure_hyp_diff_hyp_of_ne at the points of E^k ∩ Z ⊆ E^k ∩ E^j).

theorem Hironaka.Manifold.BMOmod.stepFamily_hyp_inl_inter_compl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (k : T.F.ι) : (stepFamily T hfin hne).hyp (toLex (Sum.inl k)) ∩ ⇑(stepπ T hfin hne) ⁻¹' (step2bCenter T hfin hne)ᶜ = ⇑(stepπ T hfin hne) ⁻¹' T.F.hyp k ∩ ⇑(stepπ T hfin hne) ⁻¹' (step2bCenter T hfin hne)ᶜ

Off the exceptional divisor every strict transform is the preimage (mem_strictTransform_iff_of_notMem).