The coherence of the identifications in an extension-compatible family #
An ExtensionCompatibleFamily M ([Wlo09, Theorem 2.0.3 (1) and (4)]) identifies, for every
compact K, the end result U_r of the succession seq K over U_K = nhd K with map⁻¹(U_K)
(toSpace K, an analytic isomorphism over U_K), and for K₁ ⊆ K₂ asserts that the
restriction of seq K₂ to U_{K₁} is an extension of seq K₁ ([Wlo09, Definition 3.2.6]):
identifications e k of its stages with stages of seq K₁, over U_{K₁}. Włodarczyk's (4) says
that the restriction "determines the factorization" of the same map prin_{I|Ũ₁}; the structure
has no field tying toSpace K₂, restricted over U_{K₁}, to toSpace K₁ ∘ e r. None is needed:
the two agree, because an analytic map from the end result of a finite succession over U_K to
M̃ over U_K is unique.
ExtensionCompatibleFamily.eq_of_map_comp_eq(uniqueness): two analytic mapsf, gfrom the end resultT_rof a finite successionToverU_KtoM̃withmap ∘ f = map ∘ g = σ^r_Tare equal. Over the complement of the imagesZof the centres ofseq K(centerImages) the composite blow-down ofseq Kis injective (isAnalyticIsoOver_stageMap, [Kol07, Theorem 35 (3)]), somapis injective onmap⁻¹(U_K ∖ Z)throughtoSpace K, andf = gon(σ^r_T)⁻¹(U_K ∖ Z). That set is dense inT_r: the composite ofTis a local homeomorphism off the preimage of the images of its own centres, a dense set (dense_preimage_compl_centerImages), so the image of an open set contains an open set ofU_Kmeeting the range of the composite ofseq K, which the dense set(σ^r)⁻¹(U_K ∖ Z)of the end result ofseq Kmeets. Continuous maps into a Hausdorff space agreeing on a dense set are equal (Mathlib'sContinuous.ext_on).restrictStageIncl: the inclusion of the stages of the restriction of a succession to an open subset into the stages of the succession (the open inclusionU₁ → U₂at stage0, the inclusion of the trace at the later stages), compatible with the composite blow-downs (val_composite_restrictStageIncl).ExtensionCompatibleFamily.toSpace_comp_restrictStageIncl_eq_of_composite_comp_eqandExtensionCompatibleFamily.toSpace_comp_restrictStageIncl_eq(coherence): forK₁ ⊆ K₂,toSpace K₂after the inclusion of the end result of the restriction ofseq K₂toU_{K₁}equalstoSpace K₁after any analytic map to the end result ofseq K₁overU_{K₁}— in particular after the identificatione rof the end results provided by any witness ofisExtensionOf_restrict(its last-stage clauseblk r = rand its over-U_{K₁}clause are the hypotheses; the stageblk rofseq K₁is carried to its last stage by the compositestageMapLE, the identity at equal indices).
The composite blow-down off the images of the centres #
The centres of S lie over the images of the centres.
The composite blow-down σ^r : U_r → U_0 is an analytic isomorphism over the complement of
the images of the centres ([Kol07, Theorem 35 (3)]; isAnalyticIsoOver_stageMap).
The stage inclusions of a restriction #
ℕ-indexed: the inclusion of the stage (σ^m)⁻¹(U₁) of the restriction of S to U₁ into
the stage U_m of S — the open inclusion U₁ → U₂ at stage 0 (restrictOpensIncl), the
inclusion of the trace, an open subset of U_m, at the later stages.
Equations
- S.restrictStageInclAux h 0 x_2 = AnalyticManifold.FiniteSuccession.restrictOpensIncl h
- S.restrictStageInclAux h m.succ hm = (S.stage ⟨m + 1, hm⟩).inclusion (S.restrictStageOpens U₁ ⟨m + 1, hm⟩)
Instances For
The inclusion of the stage i of the restriction of S to U₁ ≤ U₂ into the stage U_i
of S (the restriction's stages are the preimages of U₁, open subsets of the stages of S).
Equations
- S.restrictStageIncl h i = S.restrictStageInclAux h ↑i ⋯
Instances For
ℕ-indexed: the composite blow-down of the restriction, read in M, is the composite
blow-down of S after the stage inclusion (val_stageMap_restrict_aux at the later stages).
The composite blow-down of the restriction, read in M, is the composite blow-down of S
after the inclusion of the end results.
At two equal indices the composite stageMapLE between the stages is the transported
identity: it commutes with the composite blow-downs to M (stageMapLE_self).
The coherence of the identifications #
map ∘ toSpace K = σ^r at a point, read in M (map_toSpace).
toSpace K is onto map⁻¹(U_K) (the bijection clause of toSpace_isIso).
Uniqueness of the identification ([Wlo09, Theorem 2.0.3 (4)]: the restriction of the
factorization of prin_{I|Ũ₂} "determines" that of prin_{I|Ũ₁}). Two analytic maps f, g from
the end result T_r of a finite succession T over U_K to M̃ which are over U_K
(map ∘ f = map ∘ g = σ^r_T, as maps to M) are equal. Off the images Z of the centres of
seq K the composite blow-down of seq K is injective, so through the identification toSpace K
the map map is injective on map⁻¹(U_K ∖ Z) and f = g on (σ^r_T)⁻¹(U_K ∖ Z); that set is
dense in T_r, and continuous maps into a Hausdorff space agreeing on a dense set are equal.
The identification toSpace K₂ of the end result of the succession over U_{K₂}, after the
inclusion of the end result of its restriction to U_{K₁}, is over U_{K₁}.
Coherence of the identifications, general form ([Wlo09, Theorem 2.0.3 (4)]). For
K₁ ⊆ K₂ and any analytic map φ from the end result of the restriction of seq K₂ to U_{K₁}
to the end result of seq K₁ which is over U_{K₁} (σ^r_{K₁} ∘ φ is the composite of the
restriction), toSpace K₂ after the inclusion of the end results equals toSpace K₁ ∘ φ: both
are over U_{K₁}, and such a map is unique (eq_of_map_comp_eq).
Coherence of the identifications ([Wlo09, Theorem 2.0.3 (4)] with
[Wlo09, Definition 3.2.6]). For K₁ ⊆ K₂ and a witness (blk, e) of isExtensionOf_restrict
— only its clauses blk r = r (hl) and "the e k are over U_{K₁}" (hover) are used — the
identification toSpace K₂, restricted to the end result of the restriction of seq K₂ to
U_{K₁}, is toSpace K₁ after the identification e r of the end results (the stage blk r
of seq K₁ carried to its last stage by stageMapLE, the identity at equal indices): the
restriction of the factorization over U_{K₂} determines the factorization over U_{K₁}.