The global lift of a local analytic isomorphism to the principalizations #

Włodarczyk's principalization commutes with local analytic isomorphisms [Wlo09, Theorem 2.0.3, last sentence; Theorem 3.5.1 (2)]: for a local analytic isomorphism g : N → M and an ideal sheaf I on M, the succession of the principalization of g^*I over a neighbourhood U_{K'} of a compact of N is the pull-back of the succession of the principalization of I over a neighbourhood U_K ⊇ g(U_{K'}), up to blow-ups with empty centre (the clause isPullbackAlong of IdealSheafPair.CommutesWithLocalAnalyticIsomorphisms). Over the whole manifolds this gives a map g̃ : Ñ → M̃ over g, the "natural lifting" of [Wlo09, Theorem 2.0.1 (3)] for the principalization, which identifies Ñ with the fibre product N ×_M M̃. This module constructs it for two extension-compatible families F' over N and F over M from exactly the data the theorem asserts: every U_{K'} has compact closure (hcl) and the per-compact pull-back relation (hrel).

The pieces (liftCompact, lastLift, pieceMap): for a compact K' of N the compact K := closure g(U_{K'}) of M satisfies g(U_{K'}) ⊆ U_K, so the relation supplies a lift R_{r'} → S_r of the last stages over g (exists_lift_bijOn_fiber), a local analytic isomorphism bijective on the fibres; after toSpace K it is a map R_{r'} → M̃ over g.
Uniqueness (eqOn_of_map_eq): two maps from an open subset of Ñ to M̃, continuous there and over g, agree. Off the images Z of the centres of S the composite blow-down of S is injective, so over a point of U_K ∖ Z the fibre of F.map is a single point; the points of the piece whose image in M avoids Z are dense in the piece (dense_preimage_compl_centerImages pulled back along the open map lastLift), and M̃ is Hausdorff (Set.EqOn.of_subset_closure). This is eq_of_map_comp_eq of FamilyCoherence.lean with g in place of an inclusion.
The gluing (pieceFun, liftFun, lift): on the open piece O_{K'} = F'.map⁻¹(U_{K'}) the piece map read through the inverse of toSpace K'; the value of the lift at q is the piece map of the singleton compact {F'.map q}. Every piece map agrees with the lift on its piece (uniqueness on the overlap), so the lift is analytic, a local analytic isomorphism (isLocalDiffeomorph_lift), over g (map_lift), bijective on the fibres (bijOn_fiber_lift), and the only continuous map over g (eq_lift_of_map_eq).
IdealSheafPair.commutesWithLocalAnalyticIsomorphisms_of_isPullbackUpToEmptyAlong: the clause IdealSheafPair.CommutesWithLocalAnalyticIsomorphisms for an assignment on the pairs whose successions pull back along local analytic isomorphisms over every pair of compacts and whose neighbourhoods have compact closures; and its consequences bijOn_preimage_of_bijOn_fiber (over an open on which g is injective, the lift is a bijection between the preimages: the identification Ñ = N ×_M M̃), surjective_of_bijOn_fiber (the global content of [Wlo09, Theorem 3.5.1 (1)]), and the naturality IdealSheafPair.CommutesWithLocalAnalyticIsomorphisms.comp_eq, id_eq from uniqueness, through the lift clause at a pair given by its ideal sheaf (exists_lift_of_eq).

The global lift of a local analytic isomorphism to the principalizations #

The identification of the end result and the fibres #

The pieces #

Uniqueness of maps over g #

The gluing #

The lift clause for an assignment on pairs, and its consequences #

Uniqueness of maps over `g` #