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 in the interior and smooth everywhere (including at the boundary). The definition mirrors SmoothManifoldWithCorners, but using an analyticGroupoid in place of contDiffGroupoid. All analytic manifolds are smooth manifolds.

Completeness is required throughout, but this is nonessential: it is due to many of the lemmas about AnalyticWithinOn` requiring completeness for ease of proof.

analyticGroupoid

f ∈ PartialHomeomorph 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.

def analyticPregroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 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 AnalyticWithinOn when read in E through I. Using AnalyticWithinOn rather than AnalyticOn gives us meaningful definitions at boundary points.

Equations

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

def analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 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 AnalyticWithinOn when read in E through I. Using AnalyticWithinOn rather than AnalyticOn 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] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {s : Set H} (hs : IsOpen s) : PartialHomeomorph.ofSet s hs ∈ analyticGroupoid I

An identity partial homeomorphism belongs to the analytic groupoid.

theorem symm_trans_mem_analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] (e : PartialHomeomorph M H) : e.symm.trans e ∈ analyticGroupoid I

The composition of a 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] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : ClosedUnderRestriction (analyticGroupoid I)

The analytic groupoid is closed under restriction.

Equations

• ⋯ = ⋯

theorem mem_analyticGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {f : PartialHomeomorph H H} : f ∈ analyticGroupoid I ↔ AnalyticWithinOn 𝕜 (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ Set.range ↑I) ∧ AnalyticWithinOn 𝕜 (↑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] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] (e : PartialHomeomorph H H) : e ∈ analyticGroupoid I ↔ AnalyticOn 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I '' e.source) ∧ AnalyticOn 𝕜 (↑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 partial homeomorphisms which are analytic and have analytic inverse.

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

analyticGroupoid is closed under products

class AnalyticManifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_5) [TopologicalSpace M] [ChartedSpace H M] extends HasGroupoid : 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.

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

Normed spaces are analytic manifolds over themselves.

Equations

• ⋯ = ⋯

instance AnalyticManifold.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type} {A : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [TopologicalSpace A] {F : Type} {B : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 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

Equations

• ⋯ = ⋯

instance AnalyticManifold.smoothManifoldWithCorners {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [cm : AnalyticManifold I M] : SmoothManifoldWithCorners I M

Analytic manifolds are smooth manifolds.

Equations

• ⋯ = ⋯