Steps 2.1 and 2 and empty boundary members: the index correspondence

Kollár's functors ignore empty blow-ups ([Kol07, 32]); the counterpart of this convention for the members of the boundary is the indifference of a functor to empty boundary members (AnalyticBlowUpSequenceAssignment.IndifferentToEmptyMembers). For a boundary F' with simple normal crossings embedding order-preservingly into E along e, the members matched along e and empty outside its range, Step 2.1 of the proof of [Kol07, Theorem 103] on (M, 𝓘, E) equals Step 2.1 on (M, 𝓘, F'): the nonempty members of E in the order of the index set are the images along e of those of F' (nonemptyList_eq_map, both lists sorted and permutations of each other), and at each step the data of Lemma 102 are indifferent on the induced triples, whose boundaries correspond along the index correspondence of BoundaryEnlarge.lean, here an order embedding (corrIdx) matching the members and empty outside its range. Step 2.2 then coincides, since the exceptional divisors, the transform of the hypersurface of maximal contact and the controlled transform do not see the index set of the boundary, so Step 2 is indifferent as well.

• FiniteSuccession.corrIdxAux_le_iff, FiniteSuccession.corrIdx — the index correspondence as an order embedding; hyp_corrIdxAux_of_forall, hyp_eq_empty_of_notMem_range_corrIdx — matched members, empty outside the range.
• BO.nonemptyList_eq_map — the sorted lists of nonempty members correspond along e.

The argument itself is carried out in the compatible-family form in Step21FamIndiff.lean (Step 2.1) and Step2AssemblyComm.lean (Step 2).

theorem AnalyticManifold.FiniteSuccession.corrIdxAux_le_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι ↪o F.ι) (i : ℕ) (h : i < S.length + 1) (a b : (S.totalTransformSeqFromAux G i h).ι) : S.corrIdxAux (⇑e) i h a ≤ S.corrIdxAux (⇑e) i h b ↔ a ≤ b

The index correspondence induced by an order embedding is order-reflecting at every stage: transforms of original members compare as the originals, exceptional divisors as themselves, and the lexicographic sum puts the new divisor last.

def AnalyticManifold.FiniteSuccession.corrIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι ↪o F.ι) (i : Fin (S.length + 1)) : (S.totalTransformSeqFrom G i).ι ↪o (S.totalTransformSeqFrom F i).ι

The index correspondence at stage i induced by an order embedding, as an order embedding.

Equations

• S.corrIdx e i = OrderEmbedding.ofMapLEIff (S.corrIdxAux ⇑e ↑i ⋯) ⋯

theorem AnalyticManifold.FiniteSuccession.corrIdx_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι ↪o F.ι) (i : Fin (S.length + 1)) (a : (S.totalTransformSeqFrom G i).ι) : (S.corrIdx e i) a = S.corrIdxAux ⇑e ↑i ⋯ a

theorem AnalyticManifold.FiniteSuccession.hyp_corrIdxAux_of_forall {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι → F.ι) (hmem : ∀ (j : G.ι), G.hyp j = F.hyp (e j)) (i : Fin (S.length + 1)) (kk : (S.totalTransformSeqFrom G i).ι) : (S.totalTransformSeqFrom G i).hyp kk = (S.totalTransformSeqFrom F i).hyp (S.corrIdxAux e ↑i ⋯ kk)

When the members of G are members of F along e, the members of the stage-i families correspond along the index correspondence.

theorem AnalyticManifold.FiniteSuccession.hyp_eq_empty_of_notMem_range_corrIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι ↪o F.ι) (hout : ∀ b ∉ Set.range ⇑e, F.hyp b = ∅) (i : Fin (S.length + 1)) (b : (S.totalTransformSeqFrom F i).ι) (hb : b ∉ Set.range ⇑(S.corrIdx e i)) : (S.totalTransformSeqFrom F i).hyp b = ∅

When the members of F outside the range of e are empty, the members of the stage-i family from F outside the range of the index correspondence are empty (the exceptional divisors all lie in the range).

theorem Hironaka.Manifold.BO.nonemptyList_eq_map {𝕜 : 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) (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 = ∅) (hF : Finite { j : T.F.ι // T.F.hyp j ≠ ∅ }) (hF' : Finite { j : F'.ι // F'.hyp j ≠ ∅ }) : T.F.nonemptyList hF = List.map (⇑e) (F'.nonemptyList hF')

The nonempty members of E in the order of the index set are the images along e of the nonempty members of F' in the order of theirs: both lists are sorted and are permutations of each other, the nonempty members of E lying in the range of e with the matched members.