The piece family after the blow-up of a centre

After blowing up the locus Z of a centre S of the state, the old pieces go to their strict transforms with their labels and exponents unchanged, and each face P ∈ S gives one new piece, π⁻¹(locus of P), with the new label (the exceptional divisor is appended last, Kol07, Definition 65) and the exponent total P − m ([Kol07, Definition 60]; in [Kol07, 111, Step 3] the new divisor gets the coefficient a_{j₁} + ⋯ + a_{j_r} − m). This file defines that transition, PieceFamily.blowUpPieces. Its labels and exponents are those of the combinatorial transition Hironaka.Monomial.MonomialState.blowUp, so that as soon as the nerve of the transition is the combinatorial one (BMO/Step3Monomial/Kernel.lean) the state of the transition is the combinatorial blow-up of the state (toState_blowUpPieces_of_nerve_eq). The label embedding into the members of the transformed boundary family is extended by the exceptional member, placed last (extendEmb).

The label embedding extended by the exceptional member

noncomputable def Hironaka.Manifold.BMO.extendEmb {ι : Type u} [LinearOrder ι] {L : ℕ} (e : Fin L ↪o ι) : Fin (L + 1) ↪o ι ⊕ₗ PUnit.{u + 1}

The label embedding of a family extended by the exceptional member, placed last: the labels < L go to the old members, the new label L to the exceptional member inr (), the top of the lexicographic sum ([Kol07, Definition 65]: the exceptional divisor is added as the last divisor).

Equations

• Hironaka.Manifold.BMO.extendEmb e = OrderEmbedding.ofStrictMono (fun (i : Fin (L + 1)) => if h : ↑i < L then toLex (Sum.inl (e ⟨↑i, h⟩)) else toLex (Sum.inr PUnit.unit)) ⋯

theorem Hironaka.Manifold.BMO.extendEmb_apply_of_lt {ι : Type u} [LinearOrder ι] {L : ℕ} (e : Fin L ↪o ι) {i : Fin (L + 1)} (h : ↑i < L) : (extendEmb e) i = toLex (Sum.inl (e ⟨↑i, h⟩))

theorem Hironaka.Manifold.BMO.extendEmb_castSucc {ι : Type u} [LinearOrder ι] {L : ℕ} (e : Fin L ↪o ι) (i : Fin L) : (extendEmb e) i.castSucc = toLex (Sum.inl (e i))

theorem Hironaka.Manifold.BMO.extendEmb_last {ι : Type u} [LinearOrder ι] {L : ℕ} (e : Fin L ↪o ι) : (extendEmb e) (Fin.last L) = toLex (Sum.inr PUnit.unit)

The transition

noncomputable def Hironaka.Manifold.BMO.PieceFamily.blowUpPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) : PieceFamily (Manifold.blowUp ψ₀ hZ)

The piece family after blowing up the locus of the centre S: old pieces go to their strict transforms with labels and exponents kept; each face P ∈ S gives one new piece, the preimage of its locus, at the index newComp S P, with the new label nextLabel and the exponent total P − m ([Kol07, 111, Step 3], [Kol07, Definition 60]). The labels and exponents are those of the combinatorial transition Hironaka.Monomial.MonomialState.blowUp.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_nextComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) : (Φ.blowUpPieces S m hZ).nextComp = Φ.nextComp + S.card

@[simp]

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_nextLabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) : (Φ.blowUpPieces S m hZ).nextLabel = Φ.nextLabel + 1

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_piece_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {c : ℕ} (hc : c < Φ.nextComp) : (Φ.blowUpPieces S m hZ).piece c = Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hZ)) (Φ.centerOf S) (Φ.piece c)

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_label_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {c : ℕ} (hc : c < Φ.nextComp) : (Φ.blowUpPieces S m hZ).label c = Φ.label c

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_a_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {c : ℕ} (hc : c < Φ.nextComp) : (Φ.blowUpPieces S m hZ).a c = Φ.a c

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_label_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {c : ℕ} (hc : Φ.nextComp ≤ c) : (Φ.blowUpPieces S m hZ).label c = Φ.nextLabel

theorem Hironaka.Manifold.BMO.PieceFamily.filter_newComp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) {P : Finset ℕ} (hP : P ∈ S) : {Q ∈ S | Φ.newComp S Q = Φ.newComp S P} = {P}

The faces of S allocated to the index newComp S P are exactly P.

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_label_newComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) (P : Finset ℕ) : (Φ.blowUpPieces S m hZ).label (Φ.newComp S P) = Φ.nextLabel

The new piece of a face carries the new label.

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_piece_newComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {P : Finset ℕ} (hP : P ∈ S) : (Φ.blowUpPieces S m hZ).piece (Φ.newComp S P) = ⇑(Manifold.blowUpπ ψ₀ hZ) ⁻¹' Φ.faceSet P

The new piece of the face P ∈ S is the preimage of its locus.

theorem Hironaka.Manifold.BMO.PieceFamily.blowUpPieces_a_newComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {P : Finset ℕ} (hP : P ∈ S) : (Φ.blowUpPieces S m hZ).a (Φ.newComp S P) = Φ.total P - m

The new piece of the face P ∈ S carries the exponent total P − m [Kol07, Definition 60].

The seam with the imported engine

theorem Hironaka.Manifold.BMO.PieceFamily.toState_blowUpPieces_of_nerve_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {n' : ℕ} (hV : Φ.IsValid n' m) (hV' : (Φ.blowUpPieces S m hZ).IsValid n' m) (h : (Φ.blowUpPieces S m hZ).nerve = ((Φ.toState n' m hV).blowUp S).nerve) : (Φ.blowUpPieces S m hZ).toState n' m hV' = (Φ.toState n' m hV).blowUp S

The state of the transition is the combinatorial blow-up of the state as soon as the nerves agree: every other data field is definitionally the combinatorial one. The nerve equality is proved in BMO/Step3Monomial/Kernel.lean.