The lifts of a pull-back up to empty blow-ups are bijective on the fibres #
For R.IsPullbackUpToEmptyAlong S g ([Wlo09, Theorem 3.5.1 (2)] read on successions), the lifts
f_k : R_{j_k} → S_k of the local analytic isomorphism g are local analytic isomorphisms over
g; this module shows that each f_k maps the fibre of the composite blow-down of R over a
point y bijectively onto the fibre of the composite blow-down of S over g y
(FiniteSuccession.bijOn_fiber_of_isPullbackUpToEmptyAlong_clauses). This is the sense in which
the stages of R are the fibre products N ×_M S_k [Wlo09, Proposition 3.4.1], stated without
forming them; it is what the global lift of g to the principalizations
(Hironaka/Resolution/Analytic/Wlo09/FamilyLift.lean) needs to identify Ñ with N ×_M M̃.
The argument is an induction on the stage. At stage 0 the lift is the restriction of g, and
both fibres are single points. At a step where S blows up a centre Z and R blows up its
pull-back f_k⁻¹(Z), a continuous map over f_k between the two blowings-up is bijective over
a local inverse of f_k (injOn_of_comm_local, exists_eq_of_comm_local, from the uniqueness
of the blowing-up), so f_{k+1} maps the fibre of the blow-down over c bijectively onto the
fibre over f_k c (bijOn_fiber_of_comm; a point off the pulled-back centre has a single
preimage on both sides, a centre of codimension 0 has none, and the chart data of the two
blowings-up are aligned by IsBlowUp.congr_chart and IsClosedSubmanifold.codim_eq_of_nonempty).
At a step where the pulled-back centre is empty, the blow-up of S is a bijection over the
complement of its centre, which contains the range of f_k.
stageMapLE_bijective_of_eq,stageMapLE_apply_of_eq: at two equal indices the compositestageMapLEis a bijection commuting with the composite blow-downs (the transported identity).PartialDiffeomorph.restrOpen,IsLocalDiffeomorphAt.congr_of_eventuallyEq: a map agreeing near a point with a local analytic isomorphism at that point is one.bijOn_fiber_of_comm: the one-step fibre bijection.bijOn_fiber_of_isPullbackUpToEmptyAlong_clauses: the fibre bijection at every stage, andIsPullbackUpToEmptyAlong.exists_lift_bijOn_fiberfor the last stage, with the lift carried to the last stage ofR.
Partial diffeomorphisms restricted to an open subset #
The restriction of a partial diffeomorphism to an open subset s of its domain: the source
becomes Φ.source ∩ s, the target its image.
Equations
Instances For
A map which agrees near x with a local diffeomorphism at x is a local diffeomorphism at
x: the partial diffeomorphism of the latter, restricted to the open set where the two agree.
The composite between two equal stages #
At two equal indices the composite stageMapLE is a bijection (the transported identity,
stageMapLE_self).
At two equal indices the composite stageMapLE is a local analytic isomorphism.
The one-step fibre bijection #
A blowing-up along a centre of codimension 0 has no point over the centre (there is no
blow-up chart of index i : Fin 0, while the charts cover the preimage of every adapted chart).
The one-step fibre bijection. For h : N₀ → M₀ a local analytic isomorphism, π the
blowing-up of M₀ along the closed submanifold Y and π' the blowing-up of N₀ along
h⁻¹(Y) (with any chart data), a continuous map G over h maps the fibre of π' over every
b bijectively onto the fibre of π over h b. Over a point off h⁻¹(Y) both fibres are
single points (IsBlowUp.bijOn_compl); over a point of h⁻¹(Y) the codimensions agree
(IsClosedSubmanifold.codim_eq_of_nonempty), a codimension 0 leaves both fibres empty, and
otherwise G is a bijection over a local inverse of h (injOn_of_comm_local,
exists_eq_of_comm_local).
The fibre bijection along a pull-back up to empty blow-ups #
The fibre of the composite blow-down of R at stage a over y.
Instances For
The fibre of the composite blow-down of S at stage k over g y, read in M.
Equations
Instances For
The fibre at an index equal to 0 is a single point.
Two points of the fibre of S at stage 0 over g y coincide.
The fibre of R at the stage after j, pulled down by the blow-up, lies in the fibre at the
stage of j.
The fibre of S at the stage after k, pulled down by the blow-up, lies in the fibre at the
stage of k.
A non-jump step. The stages a = b of R carry two lifts fa, fb to consecutive
stages of S with σ^S_{k+1} ∘ fb = fa (through the transported identity stageMapLE), and the
pull-back of the centre of S along fa is empty. Then the fibre bijection passes from fa to
fb: the blow-up of S is a bijection over the complement of its centre, which contains the
range of fa.
A jump step. The stage b of R is the stage after j, the blow-up of R along the
pull-back of the centre of S at stage k, and σ^S_{k+1} ∘ fb = fa ∘ σ^R_{j+1} (through
stageMapLE, which is σ^R_{j+1} here). The fibre bijection passes from fa to fb by the
one-step fibre bijection over every point of the fibre of R at stage j
(bijOn_fiber_of_comm).
The fibre bijection at every stage, for the clauses of IsPullbackUpToEmptyAlong: the lift
f k maps the fibre of the composite blow-down of R at stage blk k over y bijectively onto
the fibre of the composite blow-down of S at stage k over g y. Induction on k: at stage 0
the fibres are single points; at a non-jump bijOn_fiber_nonjump, at a jump bijOn_fiber_jump.
The last lift of a pull-back up to empty blow-ups is bijective on the fibres, carried to
the last stage of R: for R.IsPullbackUpToEmptyAlong S g there is a local analytic isomorphism
φ : R_{r'} → S_r over g which maps the fibre of the composite of R over every y bijectively
onto the fibre of the composite of S over g y. The last lift of any witness, after the
transported identity stageMapLE from the last stage of R to the stage blk r.