Refinement of a piece family along an analytic map

To compare the monomial procedure run on a restricted or pulled-back triple with the run on the original, the piece families of the two are related by a refinement: Ψ on X refines Φ on Y along ρ : X → Y with parent map p on the pieces and label map σ when every piece of Ψ lies in the preimage of its parent, the preimage of a parent is the union of its children, children of one parent are disjoint, labels pass through the strictly monotone σ, and exponents through p (PieceFamily.RefinesAlong). No order on the pieces is assumed; only the order of the labels is preserved, which is all the lexicographic comparison of member tuples in [Kol07, 111, Step 3] uses. The label map is an embedding rather than the identity because two open sets carry different sets of labels.

The file proves the elementary consequences: the face through x maps bijectively onto the face through ρ x, so the exponent sums agree (total_faceAt); faces map to faces and a face with a point over X lifts; the preimage of the centre of a set of faces is the centre of the faces of Ψ mapping into it (preimage_centerOf), empty when there are none. It also provides the pull-back family Φ.pullbackFamily ρ (the same pieces, labels and exponents, the pieces replaced by their whole preimages), which refines Φ with the identity maps and whose state is a sub-state of the state of Φ in the sense of the combinatorial model (Hironaka.Monomial.MonomialState.Sub), and the relabelling Ψ.relabel σ L, whose state is related to the state of Ψ by the renaming of labels Hironaka.Monomial.MonomialState.Rel and refines the state of the pull-back family (Hironaka.Monomial.MonomialState.Refines). These are the three relations through which the combinatorial model compares the two runs (BMO/Step3Monomial/RealizePullback.lean).

structure Hironaka.Manifold.BMO.PieceFamily.RefinesAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (ρ : AnalyticMap X Y) (p σ : ℕ → ℕ) (Φ : PieceFamily Y) : Prop

Ψ on X refines Φ on Y along ρ : X → Y, with parent map p on pieces and label map σ, strictly monotone on the labels in use: every piece of Ψ lies in the preimage of its parent, the preimage of a parent is the union of its children, children of one parent are disjoint, labels pass through σ and exponents through p. A parent may have no child (its preimage is then empty) or several; a label of Φ off the range of σ has no child, so its members are empty over X.

• p_lt (c : ℕ) : c < Ψ.nextComp → p c < Φ.nextComp

  Parents of live children are live.

• σ_lt (ℓ : ℕ) : ℓ < Ψ.nextLabel → σ ℓ < Φ.nextLabel

  The label map lands in Φ's label range.

• σ_strictMonoOn : StrictMonoOn σ (Set.Iio Ψ.nextLabel)

  The label map is an order embedding of the label range.

• label_eq (c : ℕ) : c < Ψ.nextComp → Φ.label (p c) = σ (Ψ.label c)

  Labels pass through σ.

• a_eq (c : ℕ) : c < Ψ.nextComp → Φ.a (p c) = Ψ.a c

  Exponents pass through p.

• piece_subset (c : ℕ) : c < Ψ.nextComp → Ψ.piece c ⊆ ⇑ρ ⁻¹' Φ.piece (p c)

  A child lies in the preimage of its parent.

• preimage_eq (c : ℕ) : c < Φ.nextComp → ⇑ρ ⁻¹' Φ.piece c = ⋃ c' ∈ {c' ∈ Finset.range Ψ.nextComp | p c' = c}, Ψ.piece c'

  The preimage of a parent is the union of its children.

• disjoint (c c' : ℕ) : c < Ψ.nextComp → c' < Ψ.nextComp → c ≠ c' → p c = p c' → Disjoint (Ψ.piece c) (Ψ.piece c')

  Children of one parent are disjoint.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.exists_child {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) {c : ℕ} (hc : c < Φ.nextComp) {x : X.carrier} (hx : ρ x ∈ Φ.piece c) : ∃ c' < Ψ.nextComp, p c' = c ∧ x ∈ Ψ.piece c'

A point of X in the preimage of a parent lies in one of its children.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.image_faceAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) (x : X.carrier) : Finset.image p (Ψ.faceAt x) = Φ.faceAt (ρ x)

The parent map sends the face through x onto the face through ρ x.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.injOn_faceAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) (x : X.carrier) : Set.InjOn p ↑(Ψ.faceAt x)

The parent map is injective on the face through x, children of one parent being disjoint.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.total_faceAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) (x : X.carrier) : Ψ.total (Ψ.faceAt x) = Φ.total (Φ.faceAt (ρ x))

The exponent sums of the faces through x and through ρ x agree.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.image_mem_nerve {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) {T : Finset ℕ} (hT : T ∈ Ψ.nerve) : Finset.image p T ∈ Φ.nerve ∧ Set.InjOn p ↑T

A face of Ψ maps to a face of Φ, and the parent map is injective on it.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.exists_lift {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) {T' : Finset ℕ} (hT' : T' ∈ Φ.nerve) {x : X.carrier} (hx : ρ x ∈ Φ.faceSet T') : ∃ T ∈ Ψ.nerve, Finset.image p T = T' ∧ x ∈ Ψ.faceSet T

A face of Φ with a point over X lifts to a face of Ψ through that point.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.preimage_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) (S : Finset (Finset ℕ)) (hS : ∀ P ∈ S, P ∈ Φ.nerve) : ⇑ρ ⁻¹' Φ.centerOf S = Ψ.centerOf ({Q ∈ Ψ.nerve | Finset.image p Q ∈ S})

The preimage of the centre of a set S of faces of Φ is the centre of the faces of Ψ mapping into S.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.preimage_centerOf_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) (S : Finset (Finset ℕ)) (hS : ∀ P ∈ S, P ∈ Φ.nerve) (hno : ∀ Q ∈ Ψ.nerve, Finset.image p Q ∉ S) : ⇑ρ ⁻¹' Φ.centerOf S = ∅

A centre none of whose faces is the image of a face of Ψ has empty preimage; the corresponding blow-up is then deleted from the run over X ([Kol07, 32]).

The pull-back family

def Hironaka.Manifold.BMO.PieceFamily.pullbackFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Φ : PieceFamily Y) (ρ : AnalyticMap X Y) : PieceFamily X

The pull-back of Φ along ρ: the same pieces, labels and exponents, the pieces replaced by their whole preimages (possibly empty, possibly disconnected).

Equations

• Φ.pullbackFamily ρ = { nextComp := Φ.nextComp, nextLabel := Φ.nextLabel, piece := fun (c : ℕ) => ⇑ρ ⁻¹' Φ.piece c, label := Φ.label, a := Φ.a, label_lt := ⋯, isClosed_piece := ⋯ }

theorem Hironaka.Manifold.BMO.PieceFamily.pullbackFamily_refinesAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Φ : PieceFamily Y) (ρ : AnalyticMap X Y) : (Φ.pullbackFamily ρ).RefinesAlong ρ id id Φ

The pull-back family refines Φ along ρ with the identity maps: one child per parent.

theorem Hironaka.Manifold.BMO.PieceFamily.mem_nerve_pullbackFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Φ : PieceFamily Y) (ρ : AnalyticMap X Y) (T : Finset ℕ) : T ∈ (Φ.pullbackFamily ρ).nerve ↔ T ∈ Φ.nerve ∧ (Φ.faceSet T ∩ Set.range ⇑ρ).Nonempty

The nerve of the pull-back family is the set of faces of Φ with a point over X.

theorem Hironaka.Manifold.BMO.PieceFamily.isValid_pullbackFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Φ : PieceFamily Y) (ρ : AnalyticMap X Y) {n m : ℕ} (hV : Φ.IsValid n m) : (Φ.pullbackFamily ρ).IsValid n m

The invariants of the state pass to the pull-back family: a sub-nerve closed under nonempty subsets.

theorem Hironaka.Manifold.BMO.PieceFamily.sub_toState_pullbackFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Φ : PieceFamily Y) (ρ : AnalyticMap X Y) {n m : ℕ} (hV : Φ.IsValid n m) : ((Φ.pullbackFamily ρ).toState n m ⋯).Sub (Φ.toState n m hV)

The state of the pull-back family is a sub-state of the state of Φ: the same data and a sub-nerve (Hironaka.Monomial.MonomialState.Sub).

The relabelling and the chain of states

def Hironaka.Manifold.BMO.PieceFamily.relabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (σ : ℕ → ℕ) (L : ℕ) (hσ : ∀ ℓ < Ψ.nextLabel, σ ℓ < L) : PieceFamily X

The relabelling of a piece family along a label map into a larger label range; the pieces are unchanged.

Equations

• Ψ.relabel σ L hσ = { nextComp := Ψ.nextComp, nextLabel := L, piece := Ψ.piece, label := fun (c : ℕ) => σ (Ψ.label c), a := Ψ.a, label_lt := ⋯, isClosed_piece := ⋯ }

theorem Hironaka.Manifold.BMO.PieceFamily.nerve_relabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (σ : ℕ → ℕ) (L : ℕ) (hσ : ∀ ℓ < Ψ.nextLabel, σ ℓ < L) : (Ψ.relabel σ L hσ).nerve = Ψ.nerve

The relabelled family has the nerve of Ψ, its pieces being unchanged.

theorem Hironaka.Manifold.BMO.PieceFamily.mem_nerve_toState_relabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (σ : ℕ → ℕ) (L : ℕ) (hσ : ∀ ℓ < Ψ.nextLabel, σ ℓ < L) {n m : ℕ} (hV' : (Ψ.relabel σ L hσ).IsValid n m) (T : Finset ℕ) : T ∈ ((Ψ.relabel σ L hσ).toState n m hV').nerve ↔ T ∈ Ψ.nerve

The nerve of the state of the relabelled family is the nerve of Ψ.

theorem Hironaka.Manifold.BMO.PieceFamily.rel_toState_relabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) {n m : ℕ} (hV : Ψ.IsValid n m) (hV' : (Ψ.relabel σ Φ.nextLabel ⋯).IsValid n m) : Monomial.MonomialState.Rel id σ (Ψ.toState n m hV) ((Ψ.relabel σ Φ.nextLabel ⋯).toState n m hV')

The state of the relabelled family is the state of Ψ with the labels renamed by the order embedding σ, the pieces untouched (Hironaka.Monomial.MonomialState.Rel).

theorem Hironaka.Manifold.BMO.PieceFamily.refines_toState_relabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) {n m : ℕ} (hV' : (Ψ.relabel σ Φ.nextLabel ⋯).IsValid n m) (hVΦ : Φ.IsValid n m) : Monomial.MonomialState.Refines p ((Ψ.relabel σ Φ.nextLabel ⋯).toState n m hV') ((Φ.pullbackFamily ρ).toState n m ⋯)

The relabelled state refines the state of the pull-back family along the parent map (Hironaka.Monomial.MonomialState.Refines): faces map injectively to faces, and every face with a point over X lifts.