The positive locus is local, and it commutes with local isomorphisms

Two facts about the centre of the monomial phase (Step2bCenter.lean):

• Locality. A point x of the member E^j lies in the positive locus (Kollár's Z_{-1} at the mark 1: its connected component in E^j lies in cosupp(𝓘, 1)) iff ord_{E^j} 𝓘 ≥ 1 at x, i.e. iff 𝓘_x ⊆ 𝓘_{E^j, x}, a condition on the stalk at x alone. Forwards, this is the criterion stalkIdeal_le_pow_of_eventually_le_ord (near x the points of E^j lie in the component of x, eventually_connectedComponentIn_eq); backwards, the constancy of the order along E^j on its connected components (ordAlong_eq_of_isPreconnected, an identity theorem) together with ord_{E^j} 𝓘 ≤ ord 𝓘. This is the form in which the exponents after a step and the restriction to opens are read.

• Functoriality. Along a local analytic isomorphism h : N → M the positive locus of the pulled-back triple is the preimage of the positive locus (Zminus1_comap, the functoriality argument in the proof of [Kol07, Lemma 102]), so the active members of the pull-back are among the active members, and the centre of the pulled-back step is the preimage of the centre whenever the top members agree: the ingredients of the commutation of the phase with local isomorphisms [Kol07, 34.1] and of its compatibility under restriction.

Locality

theorem Hironaka.Manifold.BMOmod.mem_positiveLocus_iff_one_le_ordAlong {𝕜 : 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} : x ∈ positiveLocus T j ↔ x ∈ T.F.hyp j ∧ ↑1 ≤ ⋯.idealSheaf.ordAlongIdeal T.I x

x ∈ E^j lies in the positive locus iff the order of 𝓘 along E^j at x is at least 1, a condition on the stalk at x.

Functoriality along local analytic isomorphisms

theorem Hironaka.Manifold.BMOmod.positiveLocus_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (j : T.F.ι) : positiveLocus (T.pullback h hh) j = ⇑h ⁻¹' positiveLocus T j

The positive locus of the pulled-back triple is the preimage of the positive locus (Zminus1_comap at the mark 1).

theorem Hironaka.Manifold.BMOmod.activeMembers_pullback_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : activeMembers (T.pullback h hh) ⊆ activeMembers T

A member active for the pull-back is active.

theorem Hironaka.Manifold.BMOmod.mem_activeMembers_pullback_of_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {j : T.F.ι} {x : M.carrier} (hx : x ∈ positiveLocus T j) (hxr : x ∈ Set.range ⇑h) : j ∈ activeMembers (T.pullback h hh)

A member whose positive locus meets the range of h is active for the pull-back.

theorem Hironaka.Manifold.BMOmod.activeMembers_pullback_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) : activeMembers (T.pullback h hh) = activeMembers T

For a surjective local isomorphism the active members agree.

theorem Hironaka.Manifold.BMOmod.step2bCenter_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (hfin' : (activeMembers (T.pullback h hh)).Finite) (hne' : (activeMembers (T.pullback h hh)).Nonempty) (htop : topMember (T.pullback h hh) hfin' hne' = topMember T hfin hne) : step2bCenter (T.pullback h hh) hfin' hne' = ⇑h ⁻¹' step2bCenter T hfin hne

When the top members agree, the Step 2b centre of the pull-back is the preimage of the Step 2b centre.

theorem Hironaka.Manifold.BMOmod.topMember_pullback_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (hfin' : (activeMembers (T.pullback h hh)).Finite) (hne' : (activeMembers (T.pullback h hh)).Nonempty) (hmem : topMember T hfin hne ∈ activeMembers (T.pullback h hh)) : topMember (T.pullback h hh) hfin' hne' = topMember T hfin hne

The top members agree as soon as the top member of T is active for the pull-back (the pull-back's active members lie among T's, and T's top member bounds them).