Compatibility, commutation with local isomorphisms and indifference to empty members

The value of the monomial procedure on a relatively compact open (monomialStep3SeqOn, BMO/Step3Monomial/Value.lean) is the realised run of the input piece family, the traces on U of the ambient components meeting closure U. Three further properties are required of it: it is compatible under restriction to a smaller open (for U ≤ V the value on U is the value on V pulled back and cleaned of its empty blow-ups, [Wlo09, Theorem 2.0.3 (4)]); it commutes with local analytic isomorphisms up to empty blow-ups ([Kol07, 34.1], [Wlo09, Theorem 3.5.1 (1)–(2)]); and it is unchanged when empty members of the boundary are deleted. Each is an instance of one theorem, that the run of a piece family refining another along a local analytic isomorphism is the pull-back of the run with its empty blow-ups erased (RefinesAlong.realize_pullback_eraseEmpty, BMO/Step3Monomial/RealizePullback.lean), once the two input families are shown to refine one another along the map in question. This file proves the three refinements and reads off the three properties.

• One lemma for the three refinements (refinesAlong_inputFamily_of_componentMap): a map φ of ambient components, compatible with an order embedding of the members, that carries meeting components to meeting components, preserves the exponents, maps the trace of a component into the trace of its image, covers every point over a component and separates two components with the same image, induces a refinement of the input families; the parent map re-indexes through the enumerations and the label map factors the sorted enumerations of the members (exists_labelMap_factor).
• The three component maps: for U ≤ V the identity (a component meeting closure U meets closure V); along a local analytic isomorphism g, a connected component of g⁻¹(Eʲ) maps into one connected component of Eʲ (parentIndex), with the same exponent; for the deletion of empty members, the bijection of components BMOmod.emptyExtIdx of Modified/NonmonomialIndiff.lean.

The theorem is applied with the input family's own boundary family, so the boundary data need not be transported: the run is a function of the pieces, their exponents and the order of the labels alone.

Sorted enumerations of nested finite sets factor (the label maps)

theorem Hironaka.Manifold.BMO.exists_orderEmbedding_factor {ι : Type u_1} [LinearOrder ι] {a b : ℕ} (eU : Fin a ↪o ι) (eV : Fin b ↪o ι) (h : Set.range ⇑eU ⊆ Set.range ⇑eV) : ∃ (σ : Fin a ↪o Fin b), ∀ (ℓ : Fin a), eV (σ ℓ) = eU ℓ

Two order embeddings of Fin a and Fin b into a linear order, the range of the first inside the range of the second: the first factors through the second by an order embedding Fin a ↪o Fin b.

theorem Hironaka.Manifold.BMO.exists_labelMap_factor {ι : Type u_1} [LinearOrder ι] {a b : ℕ} (eU : Fin a ↪o ι) (eV : Fin b ↪o ι) (h : Set.range ⇑eU ⊆ Set.range ⇑eV) : ∃ (σ : ℕ → ℕ) (hσ : ∀ ℓ < a, σ ℓ < b), StrictMonoOn σ (Set.Iio a) ∧ ∀ (ℓ : ℕ) (hℓ : ℓ < a), eV ⟨σ ℓ, ⋯⟩ = eU ⟨ℓ, hℓ⟩

The factor of exists_orderEmbedding_factor as a map ℕ → ℕ on the labels below a: bounded by b and strictly monotone there, and factoring the enumerations.

Components of a pulled-back family: the parent map

def Hironaka.Manifold.BMO.comapMemberMap {M N : Type u} (g : N → M) (F : Manifold.HypersurfaceFamily M) (j : F.ι) : ↑((Manifold.HypersurfaceFamily.comap g F).hyp j) → ↑(F.hyp j)

The map from a member of the pulled-back boundary family into the member.

Equations

• Hironaka.Manifold.BMO.comapMemberMap g F j x = ⟨g ↑x, ⋯⟩

theorem Hironaka.Manifold.BMO.continuous_comapMemberMap {M N : Type u} [TopologicalSpace M] [TopologicalSpace N] {g : N → M} (F : Manifold.HypersurfaceFamily M) (hg : Continuous g) (j : F.ι) : Continuous (comapMemberMap g F j)

noncomputable def Hironaka.Manifold.BMO.parentIndex {M N : Type u} [TopologicalSpace M] [TopologicalSpace N] {g : N → M} (F : Manifold.HypersurfaceFamily M) (hg : Continuous g) (i' : ComponentIndex (Manifold.HypersurfaceFamily.comap g F)) : ComponentIndex F

The parent of a component of the pulled-back family: the same member, and the connected component into which the image of the component maps (a connected set maps into one connected component).

Equations

• Hironaka.Manifold.BMO.parentIndex F hg i' = ⟨i'.fst, ⋯.connectedComponentsLift i'.snd⟩

theorem Hironaka.Manifold.BMO.parentIndex_fst {M N : Type u} [TopologicalSpace M] [TopologicalSpace N] {g : N → M} (F : Manifold.HypersurfaceFamily M) (hg : Continuous g) (i' : ComponentIndex (Manifold.HypersurfaceFamily.comap g F)) : (parentIndex F hg i').fst = i'.fst

theorem Hironaka.Manifold.BMO.mem_componentSet_parentIndex {M N : Type u} [TopologicalSpace M] [TopologicalSpace N] {g : N → M} (F : Manifold.HypersurfaceFamily M) (hg : Continuous g) {i' : ComponentIndex (Manifold.HypersurfaceFamily.comap g F)} {x : N} (hx : x ∈ componentSet (Manifold.HypersurfaceFamily.comap g F) i') : g x ∈ componentSet F (parentIndex F hg i')

theorem Hironaka.Manifold.BMO.componentSet_comap_subset_preimage {M N : Type u} [TopologicalSpace M] [TopologicalSpace N] {g : N → M} (F : Manifold.HypersurfaceFamily M) (hg : Continuous g) (i' : ComponentIndex (Manifold.HypersurfaceFamily.comap g F)) : componentSet (Manifold.HypersurfaceFamily.comap g F) i' ⊆ g ⁻¹' componentSet F (parentIndex F hg i')

theorem Hironaka.Manifold.BMO.exists_parentIndex_eq {M N : Type u} [TopologicalSpace M] [TopologicalSpace N] {g : N → M} (F : Manifold.HypersurfaceFamily M) (hg : Continuous g) {i : ComponentIndex F} {x : N} (hx : g x ∈ componentSet F i) : ∃ (i' : ComponentIndex (Manifold.HypersurfaceFamily.comap g F)), x ∈ componentSet (Manifold.HypersurfaceFamily.comap g F) i' ∧ parentIndex F hg i' = i

Every point over a component lies on a component of the pulled-back family whose parent is that component.

theorem Hironaka.Manifold.BMO.componentSet_disjoint_of_ne {M : Type u} [TopologicalSpace M] (F : Manifold.HypersurfaceFamily M) {j : F.ι} {C₁ C₂ : ConnectedComponents ↑(F.hyp j)} (h : C₁ ≠ C₂) : Disjoint (componentSet F ⟨j, C₁⟩) (componentSet F ⟨j, C₂⟩)

Two distinct components of one member are disjoint.

The index of a meeting piece in the enumeration

noncomputable def Hironaka.Manifold.BMO.meetingIndex {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {i : ComponentIndex T.F} (hi : i ∈ meetingPieces T U hU) : Fin (meetingPieces T U hU).card

The index of a meeting piece in the enumeration meetingPiece.

Equations

• Hironaka.Manifold.BMO.meetingIndex T U hU hi = (Hironaka.Manifold.BMO.meetingPieces T U hU).equivFin ⟨i, hi⟩

theorem Hironaka.Manifold.BMO.meetingPiece_meetingIndex {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {i : ComponentIndex T.F} (hi : i ∈ meetingPieces T U hU) : meetingPiece T U hU (meetingIndex T U hU hi) = i

The refinements between input families

theorem Hironaka.Manifold.BMO.PieceFamily.refinesAlong_inputFamily_of_componentMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M₁ M₂ : AnalyticManifold 𝕜 E} (T₁ : Manifold.AnalyticTriple ψ₀ M₁) (U₁ : TopologicalSpace.Opens M₁.carrier) (hU₁ : IsCompact (closure ↑U₁)) (T₂ : Manifold.AnalyticTriple ψ₀ M₂) (U₂ : TopologicalSpace.Opens M₂.carrier) (hU₂ : IsCompact (closure ↑U₂)) (ρ : AnalyticMap (M₁.restrict U₁) (M₂.restrict U₂)) (φ : ComponentIndex T₁.F → ComponentIndex T₂.F) (eMem : T₁.F.ι ↪o T₂.F.ι) (hφfst : ∀ (i : ComponentIndex T₁.F), (φ i).fst = eMem i.fst) (hφmeet : ∀ i ∈ meetingPieces T₁ U₁ hU₁, φ i ∈ meetingPieces T₂ U₂ hU₂) (hφa : ∀ i ∈ meetingPieces T₁ U₁ hU₁, componentExponent T₂.F ⋯ T₂.I (φ i) = componentExponent T₁.F ⋯ T₁.I i) (hsub : ∀ i ∈ meetingPieces T₁ U₁ hU₁, ∀ (x : (M₁.restrict U₁).carrier), (M₁.inclusion U₁) x ∈ componentSet T₁.F i → (M₂.inclusion U₂) (ρ x) ∈ componentSet T₂.F (φ i)) (hcover : ∀ i₂ ∈ meetingPieces T₂ U₂ hU₂, ∀ (x : (M₁.restrict U₁).carrier), (M₂.inclusion U₂) (ρ x) ∈ componentSet T₂.F i₂ → ∃ i ∈ meetingPieces T₁ U₁ hU₁, φ i = i₂ ∧ (M₁.inclusion U₁) x ∈ componentSet T₁.F i) (hdisj : ∀ i ∈ meetingPieces T₁ U₁ hU₁, ∀ i' ∈ meetingPieces T₁ U₁ hU₁, i ≠ i' → φ i = φ i' → ∀ (x : (M₁.restrict U₁).carrier), (M₁.inclusion U₁) x ∈ componentSet T₁.F i → (M₁.inclusion U₁) x ∉ componentSet T₁.F i') : ∃ (p : ℕ → ℕ) (σ : ℕ → ℕ), (inputFamily T₁ U₁ hU₁).RefinesAlong ρ p σ (inputFamily T₂ U₂ hU₂)

The common form of the three refinements: a map φ of ambient components, compatible with an order embedding eMem of the members, carrying meeting components to meeting components, preserving the exponents, mapping the trace of a component into the trace of its image, covering every point over a component, and separating two components with the same image, induces a refinement of the input families along ρ with some parent map p and label map σ.

theorem Hironaka.Manifold.BMO.PieceFamily.refinesAlong_inputFamily_restrictLE {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {U V : TopologicalSpace.Opens M.carrier} (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : ∃ (p : ℕ → ℕ) (σ : ℕ → ℕ), (inputFamily T U hU).RefinesAlong (M.restrictLE hUV) p σ (inputFamily T V hV)

For U ≤ V the input family of U refines the input family of V along the open inclusion: one child per parent, its trace.

theorem Hironaka.Manifold.BMO.PieceFamily.refinesAlong_inputFamily_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (T' : Manifold.AnalyticTriple ψ₀ N) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT'T : T'.IsPullbackOf T g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : ∃ (p : ℕ → ℕ) (σ : ℕ → ℕ), (inputFamily T' U' hU').RefinesAlong (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) p σ (inputFamily T (AnalyticMap.imageOpens g hg U') ⋯)

For T' the pull-back of T along a local analytic isomorphism g and U' ⊆ N relatively compact, the input family of (T', U') refines the input family of (T, g(U')) along g|_{U'}: the connected components of g⁻¹(Eʲ) over one component of Eʲ are the children of that component.

theorem Hironaka.Manifold.BMO.PieceFamily.refinesAlong_inputFamily_indiff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o T.F.ι) (h1 : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (h2 : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) : ∃ (p : ℕ → ℕ) (σ : ℕ → ℕ), (inputFamily { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } U hU).RefinesAlong ContMDiffMap.id p σ (inputFamily T U hU)

The input families of T and of T with its empty boundary members deleted refine one another along the identity: a bijection of the pieces, the labels through the order embedding e.

The three properties of the value

theorem Hironaka.Manifold.BMO.monomialStep3SeqOn_compat {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : monomialStep3SeqOn T m hT U hU = ((monomialStep3SeqOn T m hT V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

Compatibility under restriction: the value on U is the value on V ⊇ U pulled back to U with its empty blow-ups erased ([Wlo09, Theorem 2.0.3 (4)]).

theorem Hironaka.Manifold.BMO.monomialStep3SeqOn_pullback {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (hT : Manifold.AnalyticTriple.BMOClass m T) (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hT'T : T'.IsPullbackOf T g) (hT' : Manifold.AnalyticTriple.BMOClass m T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : monomialStep3SeqOn T' m hT' U' hU' = ((monomialStep3SeqOn T m hT (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

Commutation with local analytic isomorphisms ([Kol07, 34.1]): for T' the pull-back of T along a local analytic isomorphism g and a relatively compact open U', the value on U' is the value on g(U') pulled back along g|_{U'} with its empty blow-ups erased.

theorem Hironaka.Manifold.BMO.monomialStep3SeqOn_indiff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') (e : F'.ι ↪o T.F.ι) (h1 : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (h2 : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hT' : Manifold.AnalyticTriple.BMOClass m { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) : monomialStep3SeqOn T m hT U hU = monomialStep3SeqOn { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } m hT' U hU

Indifference to empty boundary members: deleting the empty members of the boundary does not change the value.