Pulling back endomorphism fields along open partial homeomorphisms

For an open partial homeomorphism e : E → F and a field J : F → (F →L[𝕜] F) of endomorphisms, the pullback (e^* J) p = (De_p)⁻¹ ∘ J (e p) ∘ De_p is a field of endomorphisms on the source of e. The inverse of De_p is written as the derivative of e.symm at e p, so no inversion of operators is involved. When J is an almost complex structure, e^* J is the structure that makes e complex linear, also written (e⁻¹)_* J.

Differentiating e and e.symm costs one derivative: if both are C^(n+1) and J is C^n, the pullback is C^n.

Main declarations

• OpenPartialHomeomorph.pullbackEnd: the pulled-back endomorphism field.
• OpenPartialHomeomorph.contDiffOn_pullbackEnd: the pullback costs one derivative.
• OpenPartialHomeomorph.fderiv_comp_pullbackEnd: the derivative of e intertwines the pullback with J.
• OpenPartialHomeomorph.pullbackEnd_apply_pullbackEnd_apply: the pullback of a field squaring to -1 squares to -1.

noncomputable def OpenPartialHomeomorph.pullbackEnd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : OpenPartialHomeomorph E F) (J : F → F →L[𝕜] F) (p : E) : E →L[𝕜] E

The pullback (e^* J) p = (De_p)⁻¹ ∘ J (e p) ∘ De_p of an endomorphism field along an open partial homeomorphism, as a field on its source. The inverse of De_p is written as the derivative of e.symm, so no inversion of operators is involved.

@[simp]

theorem OpenPartialHomeomorph.pullbackEnd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : OpenPartialHomeomorph E F} (J : F → F →L[𝕜] F) (p v : E) : (e.pullbackEnd J p) v = (fderiv 𝕜 (↑e.symm) (↑e p)) ((J (↑e p)) ((fderiv 𝕜 (↑e) p) v))

Evaluate a pulled-back endomorphism field.

theorem OpenPartialHomeomorph.contDiffOn_pullbackEnd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : OpenPartialHomeomorph E F} {J : F → F →L[𝕜] F} {ℓ n : WithTop ℕ∞} (he : ContDiffOn 𝕜 ℓ (↑e) e.source) (hes : ContDiffOn 𝕜 ℓ (↑e.symm) e.target) (hJ : ContDiffOn 𝕜 n J e.target) (hn : n + 1 ≤ ℓ) : ContDiffOn 𝕜 n (e.pullbackEnd J) e.source

Pulling back costs one derivative. If an open partial homeomorphism and its inverse are C^ℓ and the field J is C^n on the target with n + 1 ≤ ℓ, the pulled-back field is C^n on the source.

theorem OpenPartialHomeomorph.fderiv_comp_pullbackEnd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : OpenPartialHomeomorph E F} (J : F → F →L[𝕜] F) {p : E} (hp : p ∈ e.source) (he : DifferentiableAt 𝕜 (↑e) p) (hs : DifferentiableAt 𝕜 (↑e.symm) (↑e p)) : fderiv 𝕜 (↑e) p ∘SL e.pullbackEnd J p = J (↑e p) ∘SL fderiv 𝕜 (↑e) p

The derivative of e intertwines the pulled-back field with J.

theorem OpenPartialHomeomorph.pullbackEnd_apply_pullbackEnd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : OpenPartialHomeomorph E F} {J : F → F →L[𝕜] F} {p : E} (hp : p ∈ e.source) (he : DifferentiableAt 𝕜 (↑e) p) (hs : DifferentiableAt 𝕜 (↑e.symm) (↑e p)) (hsq : ∀ (w : F), (J (↑e p)) ((J (↑e p)) w) = -w) (v : E) : (e.pullbackEnd J p) ((e.pullbackEnd J p) v) = -v

The pullback of an almost complex structure is an almost complex structure. If J (e p) squares to -1, so does the pulled-back endomorphism at p.