Analytic changes of ambient coordinates

Analytic charts, analytic submanifolds, and analytic functions on submanifolds transport along an open partial homeomorphism (Fin n → 𝕜) → (Fin n' → 𝕜) that is analytic on its source with inverse analytic on its target, and in particular along a global analytic homeomorphism or a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜. Whenever the domain of such an open partial homeomorphism is nonempty, invertibility of its derivative forces n = n'.

Main declarations

• TauCeti.IsAnalyticChart.of_isImage, TauCeti.IsAnalyticSubmanifold.of_isImage, TauCeti.IsAnalyticSubmanifold.image_openPartialHomeomorph: transport of analytic charts and analytic submanifolds along analytic open partial homeomorphisms with analytic inverse.
• TauCeti.AnalyticOnSubmanifold.comp_openPartialHomeomorph, TauCeti.AnalyticOnSubmanifold.comp_symm_openPartialHomeomorph: transport of analytic functions on submanifolds along analytic open partial homeomorphisms.
• TauCeti.IsAnalyticChart.preimage, TauCeti.IsAnalyticSubmanifold.preimage: pullback along global analytic homeomorphisms.
• TauCeti.IsAnalyticSubmanifold.preimage_continuousLinearEquiv, TauCeti.IsAnalyticSubmanifold.image_continuousLinearEquiv, TauCeti.AnalyticOnSubmanifold.comp_continuousLinearEquiv, TauCeti.AnalyticOnSubmanifold.comp_symm_continuousLinearEquiv, TauCeti.IsAnalyticSubmanifold.preimage_comp_equiv: transport along continuous linear equivalences and coordinate bijections, together with @[simp] equivalences.

Open partial homeomorphisms

theorem TauCeti.IsAnalyticChart.of_isImage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S T : Set (Fin n → 𝕜)} {c φ : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} (hc : IsAnalyticChart d T c) (hφ : AnalyticOnNhd 𝕜 (↑φ) φ.source) (hφs : AnalyticOnNhd 𝕜 (↑φ.symm) φ.target) (hST : φ.IsImage S T) : IsAnalyticChart d S (φ.trans c)

Pulling back an analytic chart of T along an analytic open partial homeomorphism φ with analytic inverse, satisfying φ.IsImage S T, gives an analytic chart of S.

theorem TauCeti.IsAnalyticSubmanifold.of_isImage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} {T : Set (Fin n' → 𝕜)} {φ : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n' → 𝕜)} (hT : IsAnalyticSubmanifold d T) (hφ : AnalyticOnNhd 𝕜 (↑φ) φ.source) (hφs : AnalyticOnNhd 𝕜 (↑φ.symm) φ.target) (hS : S ⊆ φ.source) (hne : S.Nonempty) (hST : φ.IsImage S T) : IsAnalyticSubmanifold d S

Pulling back an analytic submanifold T along an analytic open partial homeomorphism φ with analytic inverse preserves analytic submanifolds when S ⊆ φ.source is nonempty and φ.IsImage S T.

theorem TauCeti.IsAnalyticSubmanifold.image_openPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} {φ : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n' → 𝕜)} (hS : IsAnalyticSubmanifold d S) (hφ : AnalyticOnNhd 𝕜 (↑φ) φ.source) (hφs : AnalyticOnNhd 𝕜 (↑φ.symm) φ.target) (hne : (S ∩ φ.source).Nonempty) : IsAnalyticSubmanifold d (↑φ '' (S ∩ φ.source))

The image of the part of an analytic submanifold lying in the source of an analytic open partial homeomorphism with analytic inverse is an analytic submanifold of the same dimension, provided that intersection is nonempty.

theorem TauCeti.AnalyticOnSubmanifold.comp_openPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} {T : Set (Fin n' → 𝕜)} {φ : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n' → 𝕜)} {f : (Fin n' → 𝕜) → E} (hf : AnalyticOnSubmanifold d f T) (hφ : AnalyticOnNhd 𝕜 (↑φ) φ.source) (hφs : AnalyticOnNhd 𝕜 (↑φ.symm) φ.target) (hS : S ⊆ φ.source) (hST : φ.IsImage S T) : AnalyticOnSubmanifold d (f ∘ ↑φ) S

Precomposing an analytic function on T with an analytic open partial homeomorphism φ with analytic inverse gives an analytic function on S when S ⊆ φ.source and φ.IsImage S T.

theorem TauCeti.AnalyticOnSubmanifold.comp_symm_openPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} {φ : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n' → 𝕜)} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) (hφ : AnalyticOnNhd 𝕜 (↑φ) φ.source) (hφs : AnalyticOnNhd 𝕜 (↑φ.symm) φ.target) : AnalyticOnSubmanifold d (f ∘ ↑φ.symm) (↑φ '' (S ∩ φ.source))

Pushing an analytic function on S forward along an analytic open partial homeomorphism φ with analytic inverse gives an analytic function on φ '' (S ∩ φ.source).

Global homeomorphisms and continuous linear equivalences

theorem TauCeti.IsAnalyticChart.preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} {c : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} (hc : IsAnalyticChart d S c) (e : (Fin n → 𝕜) ≃ₜ (Fin n → 𝕜)) (he : AnalyticOnNhd 𝕜 (⇑e) Set.univ) (he' : AnalyticOnNhd 𝕜 (⇑e.symm) Set.univ) : IsAnalyticChart d (⇑e ⁻¹' S) (e.toOpenPartialHomeomorph.trans c)

Pulling back an analytic chart along an analytic change of ambient coordinates gives an analytic chart of the inverse image.

theorem TauCeti.IsAnalyticSubmanifold.preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n n' d : ℕ} {T : Set (Fin n' → 𝕜)} (hT : IsAnalyticSubmanifold d T) (e : (Fin n → 𝕜) ≃ₜ (Fin n' → 𝕜)) (he : AnalyticOnNhd 𝕜 (⇑e) Set.univ) (he' : AnalyticOnNhd 𝕜 (⇑e.symm) Set.univ) : IsAnalyticSubmanifold d (⇑e ⁻¹' T)

An analytic change of ambient coordinates preserves analytic submanifolds and their dimension. The inverse must also be analytic.

theorem TauCeti.IsAnalyticSubmanifold.preimage_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n n' d : ℕ} {T : Set (Fin n' → 𝕜)} (hT : IsAnalyticSubmanifold d T) (e : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) : IsAnalyticSubmanifold d (⇑e ⁻¹' T)

Pulling back an analytic submanifold along a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜 preserves analytic submanifolds and their dimension.

theorem TauCeti.IsAnalyticSubmanifold.image_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} (hS : IsAnalyticSubmanifold d S) (e : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) : IsAnalyticSubmanifold d (⇑e '' S)

Mapping an analytic submanifold by a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜 preserves analytic submanifolds and their dimension.

@[simp]

theorem TauCeti.isAnalyticSubmanifold_preimage_continuousLinearEquiv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n n' d : ℕ} {T : Set (Fin n' → 𝕜)} (e : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) : IsAnalyticSubmanifold d (⇑e ⁻¹' T) ↔ IsAnalyticSubmanifold d T

Preimage under a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜 preserves IsAnalyticSubmanifold.

@[simp]

theorem TauCeti.isAnalyticSubmanifold_image_continuousLinearEquiv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} (e : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) : IsAnalyticSubmanifold d (⇑e '' S) ↔ IsAnalyticSubmanifold d S

Image under a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜 preserves IsAnalyticSubmanifold.

theorem TauCeti.AnalyticOnSubmanifold.comp_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' d : ℕ} {T : Set (Fin n' → 𝕜)} {f : (Fin n' → 𝕜) → E} (hf : AnalyticOnSubmanifold d f T) (e : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) : AnalyticOnSubmanifold d (f ∘ ⇑e) (⇑e ⁻¹' T)

Precomposing an analytic function on a submanifold with a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜 gives an analytic function on the preimage.

theorem TauCeti.AnalyticOnSubmanifold.comp_symm_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) (e : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) : AnalyticOnSubmanifold d (f ∘ ⇑e.symm) (⇑e '' S)

Transporting an analytic function on a submanifold along a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜 gives an analytic function on the image.

@[simp]

theorem TauCeti.analyticOnSubmanifold_comp_continuousLinearEquiv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' d : ℕ} {T : Set (Fin n' → 𝕜)} {f : (Fin n' → 𝕜) → E} (e : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) : AnalyticOnSubmanifold d (f ∘ ⇑e) (⇑e ⁻¹' T) ↔ AnalyticOnSubmanifold d f T

Precomposing with a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜 preserves AnalyticOnSubmanifold on the preimage.

@[simp]

theorem TauCeti.analyticOnSubmanifold_comp_symm_continuousLinearEquiv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} (e : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) : AnalyticOnSubmanifold d (f ∘ ⇑e.symm) (⇑e '' S) ↔ AnalyticOnSubmanifold d f S

Transporting along a continuous linear equivalence (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜 preserves AnalyticOnSubmanifold on the image.

theorem TauCeti.IsAnalyticSubmanifold.preimage_comp_equiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n n' d : ℕ} {S : Set (Fin n → 𝕜)} (hS : IsAnalyticSubmanifold d S) (e : Fin n ≃ Fin n') : IsAnalyticSubmanifold d ((fun (x : Fin n' → 𝕜) => x ∘ ⇑e) ⁻¹' S)

Reindexing the ambient coordinates along a bijection Fin n ≃ Fin n' preserves analytic submanifolds and their dimension. For n' = n this is a permutation of the coordinates.