Fibrewise linear partial diffeomorphisms

Let L : M → F₁ →L[𝕜] F₂ be a C^n family of invertible continuous linear maps on an open subset s of a charted space M, where F₁ is a Banach space and F₂ is a normed space. Operator inversion is C^n on invertible operators (ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse), so the fibrewise inverses x ↦ (L x).inverse also form a C^n family on s. Consequently, the map (x, v) ↦ (x, L x v) defines a C^n partial diffeomorphism TauCeti.fiberwiseLinearPartialDiffeomorph from s ×ˢ univ ⊆ M × F₁ onto s ×ˢ univ ⊆ M × F₂, with inverse (x, w) ↦ (x, (L x).inverse w).

Unlike FiberwiseLinear.openPartialHomeomorph, the family need only be C^n in the forward direction and invertible on s, and the source and target fibres F₁ and F₂ need not coincide. In parameterized normal-form constructions (such as straightening a C^n vector subbundle in bundle trivializations using a fixed complement), this turns a C^n family of split injections completed by a complement into a local C^n coordinate change on the trivialized bundle.

Main definitions and results

• TauCeti.fiberwiseLinearPartialDiffeomorph: the C^n partial diffeomorphism (x, v) ↦ (x, L x v) from M × F₁ to M × F₂ over s ×ˢ univ.
• TauCeti.fiberwiseLinearPartialDiffeomorph_source, TauCeti.fiberwiseLinearPartialDiffeomorph_target, TauCeti.fiberwiseLinearPartialDiffeomorph_apply, TauCeti.fiberwiseLinearPartialDiffeomorph_symm_apply, TauCeti.fiberwiseLinearPartialDiffeomorph_toPartialEquiv_symm_apply: characteristic lemmas for its source, target, forward map, and inverse map.

Formal sources

This is the PartialDiffeomorph counterpart of FiberwiseLinear.openPartialHomeomorph in Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear, by Floris van Doorn and Heather Macbeth, inferring inverse regularity from ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse and allowing distinct source and target fibres.

noncomputable def TauCeti.fiberwiseLinearPartialDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} [CompleteSpace F₁] (L : M → F₁ →L[𝕜] F₂) {s : Set M} (hs : IsOpen s) (hL : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n L s) (hInv : ∀ x ∈ s, (L x).IsInvertible) : PartialDiffeomorph (I.prod (modelWithCornersSelf 𝕜 F₁)) (I.prod (modelWithCornersSelf 𝕜 F₂)) (M × F₁) (M × F₂) n

A C^n family of invertible continuous linear maps L : M → F₁ →L[𝕜] F₂ on an open set s ⊆ M, with F₁ complete, defines a C^n partial diffeomorphism (x, v) ↦ (x, L x v) from s ×ˢ univ ⊆ M × F₁ onto s ×ˢ univ ⊆ M × F₂ with inverse (x, w) ↦ (x, (L x).inverse w).

@[simp]

theorem TauCeti.fiberwiseLinearPartialDiffeomorph_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} [CompleteSpace F₁] (L : M → F₁ →L[𝕜] F₂) {s : Set M} (hs : IsOpen s) (hL : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n L s) (hInv : ∀ x ∈ s, (L x).IsInvertible) : (fiberwiseLinearPartialDiffeomorph L hs hL hInv).source = s ×ˢ Set.univ

The source of fiberwiseLinearPartialDiffeomorph L hs hL hInv is s ×ˢ univ.

@[simp]

theorem TauCeti.fiberwiseLinearPartialDiffeomorph_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} [CompleteSpace F₁] (L : M → F₁ →L[𝕜] F₂) {s : Set M} (hs : IsOpen s) (hL : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n L s) (hInv : ∀ x ∈ s, (L x).IsInvertible) : (fiberwiseLinearPartialDiffeomorph L hs hL hInv).target = s ×ˢ Set.univ

The target of fiberwiseLinearPartialDiffeomorph L hs hL hInv is s ×ˢ univ.

@[simp]

theorem TauCeti.fiberwiseLinearPartialDiffeomorph_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} [CompleteSpace F₁] (L : M → F₁ →L[𝕜] F₂) {s : Set M} (hs : IsOpen s) (hL : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n L s) (hInv : ∀ x ∈ s, (L x).IsInvertible) (p : M × F₁) : ↑(fiberwiseLinearPartialDiffeomorph L hs hL hInv).toPartialEquiv p = (p.1, (L p.1) p.2)

fiberwiseLinearPartialDiffeomorph preserves the first coordinate and applies L to the second coordinate.

theorem TauCeti.fiberwiseLinearPartialDiffeomorph_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} [CompleteSpace F₁] (L : M → F₁ →L[𝕜] F₂) {s : Set M} (hs : IsOpen s) (hL : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n L s) (hInv : ∀ x ∈ s, (L x).IsInvertible) (q : M × F₂) : ↑(fiberwiseLinearPartialDiffeomorph L hs hL hInv).symm.toPartialEquiv q = (q.1, (L q.1).inverse q.2)

The inverse partial diffeomorphism of fiberwiseLinearPartialDiffeomorph preserves the first coordinate and applies (L ·).inverse to the second coordinate.

@[simp]

theorem TauCeti.fiberwiseLinearPartialDiffeomorph_toPartialEquiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {n : WithTop ℕ∞} [CompleteSpace F₁] (L : M → F₁ →L[𝕜] F₂) {s : Set M} (hs : IsOpen s) (hL : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n L s) (hInv : ∀ x ∈ s, (L x).IsInvertible) (q : M × F₂) : ↑(fiberwiseLinearPartialDiffeomorph L hs hL hInv).symm q = (q.1, (L q.1).inverse q.2)

The inverse of the underlying PartialEquiv of fiberwiseLinearPartialDiffeomorph preserves the first coordinate and applies (L ·).inverse to the second coordinate.