Lemma 102: indifference to empty boundary members

The analytic functors are required to be indifferent to empty boundary members (AnalyticBlowUpSequenceAssignment.IndifferentToEmptyMembers; the counterpart for boundary members of the empty blow-up convention [Kol07, 32]): deleting empty members of the boundary along an order embedding of index sets does not change the value. For BDan, the analytic BD_{n,m,·} of [Kol07, Lemma 102], the value at a kept member e i of E equals the value at the member i of the smaller boundary F'.

The first centre and the transform of the member depend only on the hypersurface E^j = E^{e i} = F'^i itself (Zminus1_eq_of_hyp_eq, transformS_eq_transformSOf, read through the parametrized core of BDOf.lean); the two restricted triples differ only in the index set of their boundary, and the indifference of the input functor absorbs the difference: the restriction of E - E^{e i} to S_0 embeds the restriction of F' - F'^i along e, with the members matched and empty outside the range.

• BDan.withBoundary — the triple with its boundary replaced.
• BDan.Zminus1_eq_of_hyp_eq, BDan.transformS_eq_transformSOf — the data at e i and at i.
• BDan.core_indifferentToEmptyMembers — the clause for the core at the mark s.
• BDan_indifferentToEmptyMembers — the clause for BDan, tuning keeping the boundary.

@[reducible, inline]

abbrev Hironaka.Manifold.BDan.withBoundary {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') : Manifold.AnalyticTriple ψ₀ M

The triple T with its boundary replaced by the family F' with simple normal crossings.

Equations

• Hironaka.Manifold.BDan.withBoundary T F' hsnc' = { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }

theorem Hironaka.Manifold.BDan.Zminus1_eq_of_hyp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (i : F'.ι) : BD.Zminus1 T.I s (T.F.hyp (e i)) = BD.Zminus1 (withBoundary T F' hsnc').I s ((withBoundary T F' hsnc').F.hyp i)

The first centre at the member e i of E is the first centre at the member i of F'.

theorem Hironaka.Manifold.BDan.transformS_eq_transformSOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (i : F'.ι) : transformS T s (e i) = transformSOf (withBoundary T F' hsnc') i ⋯

The transform of the member e i of E is the transform of the member i of F' (over the first centre at e i).

theorem Hironaka.Manifold.BDan.core_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (i : F'.ι) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (inp : BMOanData 𝕜 (n - 1) s) (hT : BDClass s T) (hT₂ : BDClass s (withBoundary T F' hsnc')) : core T s (e i) inp hT = core (withBoundary T F' hsnc') s i inp hT₂

Indifference to empty boundary members for the core at the mark s: the core at the member e i of E is the core at the member i of F'. The first centre and the transform of the member agree, and the input functor is indifferent to the empty members of the restricted boundary: the restriction of E - E^{e i} to S_0 embeds that of F' - F'^i along e, with matched members and empty members outside the range.

theorem Hironaka.Manifold.BDan_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (inp : BMOanData 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hT : Manifold.AnalyticTriple.BOClass m T) (hT' : Manifold.AnalyticTriple.BOClass m { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) (i : F'.ι) : BDan m inp T hT (e i) = BDan m inp { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } hT' i

BD_{n,m,·} is indifferent to empty boundary members (the counterpart for boundary members of the empty blow-up convention [Kol07, 32]): for a boundary F' with simple normal crossings embedding order-preservingly into E along e, with the members matched and empty outside the range, the value at the kept member e i equals the value at i for the triple with boundary F'. It is the clause for the core at the tuned triple, tuning keeping the boundary.