The coproduct of local analytic isomorphisms is a local analytic isomorphism #
A local inverse Φ of f i at x lifts to a local inverse of the coproduct fun p => f p.1 p.2
at ⟨i, x⟩: source Sigma.mk i '' Φ.source, inverse y ↦ ⟨i, Φ.symm y⟩
(PartialDiffeomorph.sigmaLift). Hence the coproduct of a family of local diffeomorphisms is a
local diffeomorphism (IsLocalDiffeomorph.sigmaDesc); this is the map g : ∐ Uᵢ → X of the proof
of [Kol07, Proposition 37], a surjective local analytic isomorphism.
noncomputable def
PartialDiffeomorph.sigmaLift
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{n : WithTop ℕ∞}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace H' P]
{ι : Type u_7}
{M : ι → Type u_8}
[(i : ι) → TopologicalSpace (M i)]
[(i : ι) → ChartedSpace H (M i)]
{f : (i : ι) → M i → P}
(hf : ∀ (i : ι), ContMDiff I J n (f i))
{i : ι}
(Φ : PartialDiffeomorph I J (M i) P n)
(hΦ : Set.EqOn (f i) (↑Φ.toPartialEquiv) Φ.source)
:
PartialDiffeomorph I J ((i : ι) × M i) P n
A local inverse of f i at x, lifted to the disjoint union.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
IsLocalDiffeomorph.sigmaDesc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners 𝕜 E' H'}
{n : WithTop ℕ∞}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace H' P]
{ι : Type u_7}
{M : ι → Type u_8}
[(i : ι) → TopologicalSpace (M i)]
[(i : ι) → ChartedSpace H (M i)]
{f : (i : ι) → M i → P}
(hf : ∀ (i : ι), IsLocalDiffeomorph I J n (f i))
:
IsLocalDiffeomorph I J n fun (p : (i : ι) × M i) => f p.fst p.snd
The coproduct of local diffeomorphisms is a local diffeomorphism.