The fibre product lifts to the blowings-up #
The proof of [Kol07, Proposition 37] blows up the descended centre and repeats the argument on
X₁' = X' ×_X X₁. On manifolds: given a surjective local analytic isomorphism g : N → M, a fibre
product (P, p₁, p₂) of g with itself, and a closed submanifold Z ⊆ M, the lifts
g₁ : Bl_{g⁻¹Z} N → Bl_Z M and q₁, q₂ : Bl_{p₁⁻¹g⁻¹Z} P → Bl_{g⁻¹Z} N of g, p₁, p₂
(blowUpLift; q₂ the lift of p₂ over the blowing-up of P along p₁⁻¹g⁻¹Z = p₂⁻¹g⁻¹Z) form
again a fibre product of g₁ with itself: g₁ ∘ q₁ = g₁ ∘ q₂ by the uniqueness of lifts, and the
bijection onto the set-theoretic fibre product comes from the local bijections of the lifts over
local inverses (liftPartialDiffeomorph: over a local inverse Φ of h at b, a continuous map
over h is a bijection π'⁻¹(Φ.source) → π⁻¹(Φ.target)). The pull-backs of a list along two
lifts of the same map from blowings-up along the same set agree (pullback_heq_of_comm).
Local bijections of a map over a local analytic isomorphism #
A continuous map over h is injective over the source of a local inverse of h.
A continuous map over h maps π'⁻¹(Φ.source) onto π⁻¹(Φ.target) for a local inverse Φ of
h.
Two lifts of the same map from blowings-up along the same set #
Two continuous maps over p from the chosen blowing-up of P along p⁻¹(Y) to the
chosen blowing-up of N along Y agree (uniqueness of lifts).
The pull-backs of a list along two lifts of p from blowings-up along (propositionally) the
same set are heterogeneously equal.
The lifted fibre product #
The centre p₂⁻¹(g⁻¹Z) of the second lift is the centre p₁⁻¹(g⁻¹Z) of the first.
The chosen blowing-up of P along p₁⁻¹(g⁻¹Z), read as a blowing-up along
p₂⁻¹(g⁻¹Z).
The lift of the second projection, over the blowing-up of P along p₁⁻¹(g⁻¹Z).
Equations
- Manifold.liftedSnd hg hp hZ = Manifold.blowUpLift ⋯ ⋯ ⋯ ⋯
Instances For
The lifted second projection as an analytic map.
Equations
- Manifold.liftedSndMap hg hp hZ = ⟨Manifold.liftedSnd hg hp hZ, ⋯⟩
Instances For
The two lifted composites g₁ ∘ q₁ and g₁ ∘ q₂ agree (uniqueness of lifts over
g ∘ p₁ = g ∘ p₂).
[Kol07, Proposition 37] ("X₁' = X' ×_X X₁"): the lifts of the two projections
form a fibre product of the lifted cover g₁ with itself — g₁ ∘ q₁ = g₁ ∘ q₂ by uniqueness of
lifts, and over a pair x, y with g₁ x = g₁ y the point w over the unique z with
p₁ z = π x, p₂ z = π y is found (and is unique) through the local bijections of the lifts over
local inverses of p₁ and of g.