Lemma 102 in the compatible-family form: indifference to empty boundary members

The value of BD_{n,m,j} on a relatively compact open does not see empty members of the boundary (BDanFam_indifferentToEmptyMembers; the counterpart of BDan_indifferentToEmptyMembers of BDIndiff.lean; for boundary members the counterpart of Kollár's convention that empty blow-ups are ignored, [Kol07, 32]): when F' is E with empty members deleted along an order embedding e, the value at the member e i of E equals the value at the member i of F', on every open. As in BDIndiff.lean, the core on an open is first written over an arbitrary centre and transform (coreFamOn_eq_of_eq, the counterpart of core_eq_of_eq; the centre and the transform at e i and at i agree as sets by Zminus1_eq_of_hyp_eq and transformS_eq_transformSOf, so both sides live on the same data), and then the input family's own indifference identifies the two values read at the trace of π_{-1}^{-1}(U): the restricted boundary of E - E^{e i} embeds that of F' - F'^i along e, with empty members outside the range.

• coreFamOn_eq_of_eq — the core on an open over an arbitrary closed hypersurface Z and a closed hypersurface S' of its blowing-up (with piOpenOf, liftInclOf of BDFam.lean);
• coreFamOn_indifferentToEmptyMembers, BDanFam_indifferentToEmptyMembers.

This is the indifferentToEmptyMembers field of Lemma 102's family data bdanFamDataOfInput in BOanFamOfInput.lean.

The core on an open over an arbitrary centre and transform

theorem Hironaka.Manifold.BDan.coreFamOn_eq_of_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) (s : ℕ) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (hZeq : Z = BD.Zminus1 T.I s (T.F.hyp j)) (hSeq : S' = transformSOf T j hZ) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : coreFamOn T s j inp hT U hU = (AnalyticManifold.BlowUpSequence.cons ⋯ ((AnalyticManifold.BlowUpSequence.pushforwardRestrict hS' (piOpenOf hZ U) ((inp.functor.fam (restrictedTripleOf T s j hZ hS' hT hZeq hSeq) ⋯).seqOn (hS'.preimageOpens (piOpenOf hZ U)) ⋯)).pullback (liftInclOf hZ U) ⋯)).eraseEmpty

The core on an open (coreFamOn, BDFam.lean) read over any closed hypersurface Z = Z_{-1} and any closed hypersurface S' = S_0 of its blowing-up (a substitution; the counterpart of core_eq_of_eq in BDOf.lean).

Indifference

theorem Hironaka.Manifold.BDan.coreFamOn_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 : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (hT₂ : BDClass s (withBoundary T F' hsnc')) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : coreFamOn T s (e i) inp hT U hU = coreFamOn (withBoundary T F' hsnc') s i inp hT₂ U hU

The core on an open is indifferent to empty boundary members: the core at the member e i of E is the core at the member i of F', when F' is E with the empty members outside the range of e deleted. The first centre and the transform are the same sets, and the input family is indifferent, on the trace of π_{-1}^{-1}(U), to the empty members of the restricted boundary (E - E^{e i})|_{S_0}, which embeds (F' - F'^i)|_{S_0} along e.

theorem Hironaka.Manifold.BDanFam_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (inp : BMOanFam 𝕜 (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'.ι) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : BDanFam m inp T hT (e i) U hU = BDanFam m inp { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } hT' i U hU

The value of BD_{n,m,·} on every relatively compact open is indifferent to empty boundary members: when F' is E with the empty members outside the range of the order embedding e deleted, the value at the member e i of E equals the value at the member i of F'. This is coreFamOn_indifferentToEmptyMembers at the tuned triple (the tuning keeps the boundary).