A local analytic isomorphism injective on an open set #
In the proof of [Kol07, Proposition 37], X'' := ∐_{i≤j} Uᵢ ∩ Uⱼ comes with the surjective open
immersions τ₁, τ₂ : X'' → X': the pieces of a coproduct of open embeddings g : N → M are the
clopen sets on which g is injective, and there g is an analytic isomorphism onto its (open)
image, the inverse being, near each point, the inverse of a local inverse of g. The analytic
isomorphism restrictInjOn (source the open set, target its image) transports charts: a chart of
M whose source contains the image gives a chart of N with source exactly the open set
(exists_chart_eq_of_injOn, through transportChart). These are the charts of the fibre product
in the hypothesis LocalCoversFibreClosed of the globalization theorem.
Near a point of h '' W, Function.invFunOn h W is the inverse of a local inverse of h.
A local analytic isomorphism injective on an open set W as an analytic isomorphism from W
onto its image (the pieces Uᵢ of X' = ∐ Uᵢ → X in [Kol07, Proposition 37]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A chart of M whose source contains h '' W transports along the inverse of h|_W to a chart
of N with source exactly W (transportChart).