Analytic manifolds (possibly with boundary or corners)

An analytic manifold is a manifold modelled on a normed vector space, or a subset like a half-space (to get manifolds with boundaries) for which changes of coordinates are analytic everywhere. The definition mirrors IsManifold, but using an analyticGroupoid in place of contDiffGroupoid. All analytic manifolds are smooth manifolds.

This file is deprecated: one should use IsManifold I ω M instead

analyticGroupoid

f ∈ OpenPartialHomeomorph H H is in analyticGroupoid I if f and f.symm are smooth everywhere, analytic on the interior, and map the interior to itself. This allows us to define AnalyticManifold including in cases with boundary.

@[deprecated "use instead `contDiffPregroupoid ω`" (since := "2025-04-13")]

def analyticPregroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : Pregroupoid H

Given a model with corners (E, H), we define the pregroupoid of analytic transformations of H as the maps that are AnalyticOn when read in E through I. Using AnalyticOn rather than AnalyticOnNhd gives us meaningful definitions at boundary points.

Equations

• analyticPregroupoid I = { property := fun (f : H → H) (s : Set H) => AnalyticOn 𝕜 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I), comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }

@[deprecated "use instead `contDiffGroupoid ω`" (since := "2025-04-13")]

def analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : StructureGroupoid H

Given a model with corners (E, H), we define the groupoid of analytic transformations of H as the maps that are AnalyticOn when read in E through I. Using AnalyticOn rather than AnalyticOnNhd gives us meaningful definitions at boundary points.

Equations

• analyticGroupoid I = (analyticPregroupoid I).groupoid

theorem ofSet_mem_analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {s : Set H} (hs : IsOpen s) : OpenPartialHomeomorph.ofSet s hs ∈ analyticGroupoid I

An identity open partial homeomorphism belongs to the analytic groupoid.

theorem symm_trans_mem_analyticGroupoid {𝕜 : 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] (e : OpenPartialHomeomorph M H) : e.symm.trans e ∈ analyticGroupoid I

The composition of an open partial homeomorphism from H to M and its inverse belongs to the analytic groupoid.

instance instClosedUnderRestrictionAnalyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} : ClosedUnderRestriction (analyticGroupoid I)

The analytic groupoid is closed under restriction.

theorem mem_analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {f : OpenPartialHomeomorph H H} : f ∈ analyticGroupoid I ↔ AnalyticOn 𝕜 (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ Set.range ↑I) ∧ AnalyticOn 𝕜 (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ Set.range ↑I)

f ∈ analyticGroupoid iff it and its inverse are analytic within range I.

theorem mem_analyticGroupoid_of_boundaryless {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] (e : OpenPartialHomeomorph H H) : e ∈ analyticGroupoid I ↔ AnalyticOnNhd 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I '' e.source) ∧ AnalyticOnNhd 𝕜 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I '' e.target)

The analytic groupoid on a boundaryless charted space modeled on a complete vector space consists of the open partial homeomorphisms which are analytic and have analytic inverse.

theorem analyticGroupoid_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E A : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace A] {F B : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {I : ModelWithCorners 𝕜 E A} {J : ModelWithCorners 𝕜 F B} {f : OpenPartialHomeomorph A A} {g : OpenPartialHomeomorph B B} (fa : f ∈ analyticGroupoid I) (ga : g ∈ analyticGroupoid J) : f.prod g ∈ analyticGroupoid (I.prod J)

analyticGroupoid is closed under products

@[deprecated "use instead `IsManifold ω`" (since := "2025-04-13")]

class AnalyticManifold {𝕜 : 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_5) [TopologicalSpace M] [ChartedSpace H M] extends HasGroupoid M (analyticGroupoid I) : Prop

An analytic manifold w.r.t. a model I : ModelWithCorners 𝕜 E H is a charted space over H s.t. all extended chart conversion maps are analytic.

• compatible {e e' : OpenPartialHomeomorph M H} : e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ analyticGroupoid I

instance AnalyticManifold.self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] : AnalyticManifold (modelWithCornersSelf 𝕜 E) E

Normed spaces are analytic manifolds over themselves.

instance AnalyticManifold.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E A : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace A] {F B : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {I : ModelWithCorners 𝕜 E A} {J : ModelWithCorners 𝕜 F B} {M : Type} [TopologicalSpace M] [ChartedSpace A M] [m : AnalyticManifold I M] {N : Type} [TopologicalSpace N] [ChartedSpace B N] [n : AnalyticManifold J N] : AnalyticManifold (I.prod J) (M × N)

M × N is an analytic manifold if M and N are

instance AnalyticManifold.isManifold {𝕜 : 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] [cm : AnalyticManifold I M] : IsManifold I (↑⊤) M

Analytic manifolds are smooth manifolds.