Closed embeddings of analytic manifolds

A closed embedding τ : N → M of analytic manifolds (AnalyticManifold.IsClosedAnalyticEmbedding: an analytic embedding, Mathlib's IsSmoothEmbedding at ω, with closed image — the first two clauses of IdealSheaf.IsPushforwardAlong, IdealSheaf.IsPushforwardAlong.isClosedAnalyticEmbedding) has the universal property of the subspace τ(N): every analytic map into M with values in τ(N) factors analytically through τ (IsClosedAnalyticEmbedding.exists_comp_eq). When its image is a closed submanifold it identifies N with the bundled submanifold IsClosedSubmanifold.toAnalyticManifold of its image (IsClosedAnalyticEmbedding.toDiffeomorph): the corestriction of τ is analytic into the bundled submanifold, and its inverse is the factorization of the inclusion of the submanifold through τ. Conversely a closed embedding of the spaces onto a closed submanifold, through which the inclusion of the submanifold factors analytically, is an immersion, so a closed embedding of analytic manifolds (IsClosedAnalyticEmbedding.of_isClosedSubmanifold, through the splitting splitEquiv of the coordinates along the adapted indices); so the push-forward of ideal sheaves may equally be stated with the universal property (IdealSheaf.isPushforwardAlong_iff_exists_comp_eq). The dimensions of two analytically isomorphic nonempty manifolds agree (dim_eq_of_diffeomorph: the differential at a point is a linear isomorphism of the models).

The re-modelling of τ between manifolds on different model spaces (transportBetween, the two-model form of AnalyticMap.transport) keeps the closed embedding onto a closed submanifold (IsClosedAnalyticEmbedding.transportBetween), the closed submanifold τ(N) with its codimension (IsClosedSubmanifold.range_transportBetween), the containment of its ideal sheaf in an ideal sheaf (stalkIdeal_idealSheaf_range_transportBetween_le) and the pull-back of ideal sheaves along τ (IdealSheaf.transport_pullback_transportBetween); these carry the hypotheses of the commutation of a principalization with closed embeddings to the standard models. The restriction of τ between opens U' ⊆ N, U ⊆ M with τ(U') ⊆ U is restrictBetween.

noncomputable def Manifold.splitCoordₗ {𝕜 : Type} [RCLike 𝕜] {n s : ℕ} (σ : Fin s ↪ Fin n) : (Fin n → 𝕜) →ₗ[𝕜] (Fin (n - s) → 𝕜) × (Fin s → 𝕜)

The coordinates of 𝕜ⁿ split into those outside the range of σ and those on it.

Equations

• Manifold.splitCoordₗ σ = { toFun := fun (y : Fin n → 𝕜) => (Manifold.projCompl σ y, fun (i : Fin s) => y (σ i)), map_add' := ⋯, map_smul' := ⋯ }

theorem Manifold.splitCoordₗ_bijective {𝕜 : Type} [RCLike 𝕜] {n s : ℕ} (σ : Fin s ↪ Fin n) : Function.Bijective ⇑(splitCoordₗ σ)

The splitting of the coordinates is bijective: injective, and 𝕜ⁿ and 𝕜^{n-s} × 𝕜^s have the same dimension.

noncomputable def Manifold.splitEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin s ↪ Fin n) : ((Fin (n - s) → 𝕜) × (Fin s → 𝕜)) ≃L[𝕜] E

The linear isomorphism 𝕜^{n-s} × 𝕜^s ≃ E of the coordinates ψ split along σ: it sends (w, 0) to the point of the coordinate subspace {z_σ = 0} with the other coordinates w (splitEquiv_apply_zero).

Equations

• Manifold.splitEquiv ψ σ = (LinearEquiv.ofBijective (Manifold.splitCoordₗ σ) ⋯).symm.toContinuousLinearEquiv.trans ψ.symm

theorem Manifold.splitEquiv_apply_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin s ↪ Fin n) (w : Fin (n - s) → 𝕜) : (splitEquiv ψ σ) (w, 0) = ψ.symm (embedCompl σ w)

def AnalyticManifold.IsClosedAnalyticEmbedding {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) : Prop

The analytic map τ : N → M, between analytic manifolds modelled on E' and on E, is a closed embedding of analytic manifolds: an analytic embedding (Mathlib's IsSmoothEmbedding at ω: an analytic immersion, of the form u ↦ (u, 0) in suitable charts near every point, which is a homeomorphism onto its image) with closed image.

Equations

• AnalyticManifold.IsClosedAnalyticEmbedding τ = (Manifold.IsSmoothEmbedding (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ ⇑τ ∧ IsClosed (Set.range ⇑τ))

The factorization through a closed embedding

theorem AnalyticManifold.IsClosedAnalyticEmbedding.isClosedEmbedding {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hτ : IsClosedAnalyticEmbedding τ) : Topology.IsClosedEmbedding ⇑τ

A closed embedding of analytic manifolds is a closed embedding of the underlying spaces.

theorem AnalyticManifold.IsClosedAnalyticEmbedding.exists_comp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hτ : IsClosedAnalyticEmbedding τ) {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {P : AnalyticManifold 𝕜 F} (h : ContMDiffMap (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 E) P.carrier M.carrier ⊤) (hh : Set.range ⇑h ⊆ Set.range ⇑τ) : ∃ (h' : ContMDiffMap (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 E') P.carrier N.carrier ⊤), ∀ (x : P.carrier), τ (h' x) = h x

Every analytic map into M with values in τ(N) factors analytically through τ: the factor is continuous since τ is a topological embedding, and analytic since τ is an analytic immersion (ContMDiff.iff_comp_isImmersion).

theorem AnalyticManifold.IsClosedAnalyticEmbedding.exists_isClosedSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hτ : IsClosedAnalyticEmbedding τ) [FiniteDimensional 𝕜 E] : ∃ (n : ℕ) (s : ℕ) (ψ : E ≃L[𝕜] Fin n → 𝕜), Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s

The image of a closed embedding of analytic manifolds is a closed submanifold, for a finite-dimensional model E of M, in the coordinates ψ : E ≃ 𝕜ⁿ of any basis, of codimension the dimension s of the complement of the immersion. At τ x, in the charts c of N and d of M in which τ reads u ↦ ε(u, 0) (ε : E' × F ≃ E), the chart d read through the linear automorphism ψ⁻¹ ∘ A ∘ ε⁻¹ of E, with A : E' × F ≃ 𝕜ⁿ sending F onto the last s coordinates, and restricted to the open set where ε⁻¹ ∘ d has its first component in the target of c and over which the image of the source of c is the trace of τ(N) (τ being a topological embedding), is adapted to τ(N).

The identification of N with the bundled submanifold τ(N)

theorem AnalyticManifold.range_inclusionMap_subset_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) : Set.range ⇑hS.inclusionMap ⊆ Set.range ⇑τ

The range of the inclusion of the bundled submanifold τ(N) lies in the range of τ.

def AnalyticManifold.diffeomorphOfSection {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) (hinj : Function.Injective ⇑τ) (h' : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 E') hS.toAnalyticManifold.carrier N.carrier ⊤) (hh' : ∀ (p : hS.toAnalyticManifold.carrier), τ (h' p) = ↑p) : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤

An injective analytic map τ with an analytic section h' : τ(N) → N over the inclusion of the bundled closed submanifold τ(N) is an analytic isomorphism of N with τ(N): the corestriction of τ, analytic into the bundled submanifold (IsClosedSubmanifold.contMDiff_codRestrict), with inverse h'.

Equations

• AnalyticManifold.diffeomorphOfSection hS hinj h' hh' = { toFun := fun (x : N.carrier) => ⟨τ x, ⋯⟩, invFun := ⇑h', left_inv := ⋯, right_inv := ⋯, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

noncomputable def AnalyticManifold.IsClosedAnalyticEmbedding.ofSub {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hτ : IsClosedAnalyticEmbedding τ) (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 E') hS.toAnalyticManifold.carrier N.carrier ⊤

The factorization of the inclusion of the bundled submanifold τ(N) through τ, an analytic map τ(N) → N (IsClosedAnalyticEmbedding.exists_comp_eq).

Equations

• hτ.ofSub hS = ⋯.choose

theorem AnalyticManifold.IsClosedAnalyticEmbedding.apply_ofSub {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hτ : IsClosedAnalyticEmbedding τ) (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) (p : hS.toAnalyticManifold.carrier) : τ ((hτ.ofSub hS) p) = ↑p

τ after the factorization is the inclusion of the submanifold.

noncomputable def AnalyticManifold.IsClosedAnalyticEmbedding.toDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hτ : IsClosedAnalyticEmbedding τ) (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤

The closed embedding τ as an analytic isomorphism of N with the bundled closed submanifold τ(N) (diffeomorphOfSection), with inverse the factorization of the inclusion through τ (IsClosedAnalyticEmbedding.ofSub).

Equations

• hτ.toDiffeomorph hS = AnalyticManifold.diffeomorphOfSection hS ⋯ (hτ.ofSub hS) ⋯

theorem AnalyticManifold.IsClosedAnalyticEmbedding.coe_toDiffeomorph_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hτ : IsClosedAnalyticEmbedding τ) (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) (x : N.carrier) : ↑((hτ.toDiffeomorph hS) x) = τ x

The isomorphism is τ on points.

theorem AnalyticManifold.isImmersionOfComplement_of_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) (e : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤) (he : ∀ (x : N.carrier), ↑(e x) = τ x) : Manifold.IsImmersionOfComplement (Fin s → 𝕜) (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ ⇑τ

An analytic map identified with the inclusion of a closed submanifold of its image is an immersion: if an analytic isomorphism e : N ≃ τ(N) onto the bundled closed submanifold τ(N) of codimension s is τ on points, then τ is an analytic immersion with complement 𝕜^s. At x, with the adapted chart φ (indices σ) of the chosen chart of τ(N) at e x and the differential L : 𝕜^{n-s} ≃ E' of e⁻¹ at e x, τ reads u ↦ ψ⁻¹(embedCompl σ (L⁻¹ u)) in the chart L ∘ chartAt ∘ e of N and the chart φ of M, a linear map u ↦ (u, 0) up to the splitting splitEquiv ψ σ of the coordinates.

theorem AnalyticManifold.IsClosedAnalyticEmbedding.of_isClosedSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) (hτc : Topology.IsClosedEmbedding ⇑τ) (h' : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 E') hS.toAnalyticManifold.carrier N.carrier ⊤) (hh' : ∀ (p : hS.toAnalyticManifold.carrier), τ (h' p) = ↑p) : IsClosedAnalyticEmbedding τ

A closed embedding of the spaces whose image is a closed submanifold, through which the inclusion of the submanifold factors analytically, is a closed embedding of analytic manifolds: the factorization identifies N with the bundled submanifold (diffeomorphOfSection), so τ is an immersion (isImmersionOfComplement_of_diffeomorph).

The push-forward of ideal sheaves through a closed submanifold

theorem AnalyticManifold.IdealSheaf.IsPushforwardAlong.isClosedAnalyticEmbedding {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {I : M.IdealSheaf} {J : N.IdealSheaf} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (h : I.IsPushforwardAlong J τ) : IsClosedAnalyticEmbedding τ

Along a push-forward of ideal sheaves, τ is a closed embedding of analytic manifolds.

theorem AnalyticManifold.IdealSheaf.IsPushforwardAlong.stalkIdeal_idealSheaf_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {I : M.IdealSheaf} {J : N.IdealSheaf} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (h : I.IsPushforwardAlong J τ) {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s) (x : M.carrier) : hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x

The ideal sheaf of the closed submanifold τ(N), in any coordinates, lies in I when the ideal of τ(N) does: its stalks are the vanishing ideals (IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_vanishingStalk).

theorem AnalyticManifold.IdealSheaf.IsPushforwardAlong.exists_isClosedSubmanifold_stalkIdeal_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {I : M.IdealSheaf} {J : N.IdealSheaf} {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} [FiniteDimensional 𝕜 E] (h : I.IsPushforwardAlong J τ) : ∃ (n : ℕ) (s : ℕ) (ψ : E ≃L[𝕜] Fin n → 𝕜) (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s), ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x

For a finite-dimensional model E of M, the image of τ is a closed submanifold whose ideal sheaf lies in I (IsClosedAnalyticEmbedding.exists_isClosedSubmanifold).

theorem AnalyticManifold.IdealSheaf.isPushforwardAlong_iff_exists_comp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (I : M.IdealSheaf) (J : N.IdealSheaf) (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) [FiniteDimensional 𝕜 E] : I.IsPushforwardAlong J τ ↔ (Topology.IsClosedEmbedding ⇑τ ∧ ∀ (F : Type) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] (P : AnalyticManifold 𝕜 F) (h : ContMDiffMap (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 E) P.carrier M.carrier ⊤), Set.range ⇑h ⊆ Set.range ⇑τ → ∃ (h' : ContMDiffMap (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 E') P.carrier N.carrier ⊤), ∀ (x : P.carrier), τ (h' x) = h x) ∧ (∃ (n : ℕ) (s : ℕ) (ψ : E ≃L[𝕜] Fin n → 𝕜) (hS : Manifold.IsClosedSubmanifold ψ (Set.range ⇑τ) s), ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) ∧ J = Manifold.IdealSheaf.pullback ⇑τ ⋯ I

The push-forward of ideal sheaves through the closed submanifold and the universal property of the embedding, for a finite-dimensional model E of M: I.IsPushforwardAlong J τ holds exactly when τ is a closed embedding of the spaces through which every analytic map into M with values in τ(N) factors analytically, τ(N) is a closed submanifold whose ideal sheaf lies in I, and J = τ^*I. Given the closed submanifold, the factorization of its inclusion makes τ an immersion (IsClosedAnalyticEmbedding.of_isClosedSubmanifold), and the stalks of its ideal sheaf are the vanishing ideals; conversely a closed embedding of analytic manifolds has the universal property (IsClosedAnalyticEmbedding.exists_comp_eq) and its image is a closed submanifold (IsClosedAnalyticEmbedding.exists_isClosedSubmanifold).

The dimensions of isomorphic manifolds

theorem AnalyticManifold.dim_eq_of_diffeomorph {𝕜 : Type} [RCLike 𝕜] {m k : ℕ} {X : AnalyticManifold 𝕜 (Fin m → 𝕜)} {Y : AnalyticManifold 𝕜 (Fin k → 𝕜)} (e : Diffeomorph (modelWithCornersSelf 𝕜 (Fin m → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) X.carrier Y.carrier ⊤) (x : X.carrier) : m = k

Two analytically isomorphic manifolds modelled on 𝕜^m and 𝕜^k, one of them nonempty, have m = k: the differential of the isomorphism at a point is a linear isomorphism of the models.

The restriction of τ between opens

def AnalyticManifold.restrictBetween {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (U' : TopologicalSpace.Opens N.carrier) (U : TopologicalSpace.Opens M.carrier) (h : ⇑τ '' ↑U' ⊆ ↑U) : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) (N.restrict U').carrier (M.restrict U).carrier ⊤

The restriction U' → U of an analytic map τ : N → M to opens with τ(U') ⊆ U.

Equations

• AnalyticManifold.restrictBetween τ U' U h = ⟨fun (p : (N.restrict U').carrier) => ⟨τ ↑p, ⋯⟩, ⋯⟩

theorem AnalyticManifold.coe_restrictBetween_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {U' : TopologicalSpace.Opens N.carrier} {U : TopologicalSpace.Opens M.carrier} (h : ⇑τ '' ↑U' ⊆ ↑U) (p : (N.restrict U').carrier) : ↑((restrictBetween τ U' U h) p) = τ ↑p

The restriction is τ on points.

The re-modelling of τ

def AnalyticManifold.transportBetween {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {E₁ : Type u_3} {E₁' : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₁'] [NormedSpace 𝕜 E₁'] (ψ : E ≃L[𝕜] E₁) (ψ' : E' ≃L[𝕜] E₁') (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) : ContMDiffMap (modelWithCornersSelf 𝕜 E₁') (modelWithCornersSelf 𝕜 E₁) (N.transport ψ').carrier (M.transport ψ).carrier ⊤

An analytic map τ : N → M read between the re-modelled manifolds N.transport ψ' and M.transport ψ, for two model changes: the same map on points (the two-model form of AnalyticMap.transport).

Equations

• AnalyticManifold.transportBetween ψ ψ' τ = ⟨fun (x : (N.transport ψ').carrier) => M.toTransport ψ (τ (N.ofTransport ψ' x)), ⋯⟩

theorem AnalyticManifold.transportBetween_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {E₁ : Type u_3} {E₁' : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₁'] [NormedSpace 𝕜 E₁'] (ψ : E ≃L[𝕜] E₁) (ψ' : E' ≃L[𝕜] E₁') (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (x : N.carrier) : (transportBetween ψ ψ' τ) (N.toTransport ψ' x) = M.toTransport ψ (τ x)

The re-modelled map is the map on points.

theorem AnalyticManifold.range_transportBetween {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {E₁ : Type u_3} {E₁' : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₁'] [NormedSpace 𝕜 E₁'] (ψ : E ≃L[𝕜] E₁) (ψ' : E' ≃L[𝕜] E₁') (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) : Set.range ⇑(transportBetween ψ ψ' τ) = ⇑(M.transportDiffeomorph ψ).symm ⁻¹' Set.range ⇑τ

The range of the re-modelled map is the preimage of the range of τ under the identity M.transport ψ → M.

theorem AnalyticManifold.IsClosedSubmanifold.range_transportBetween {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {E₁ : Type u_3} {E₁' : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₁'] [NormedSpace 𝕜 E₁'] (ψ : E ≃L[𝕜] E₁) (ψ' : E' ≃L[𝕜] E₁') {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} {n₀ s : ℕ} {ψ₀ : E ≃L[𝕜] Fin n₀ → 𝕜} (hS : Manifold.IsClosedSubmanifold ψ₀ (Set.range ⇑τ) s) : Manifold.IsClosedSubmanifold (ψ.symm.trans ψ₀) (Set.range ⇑(transportBetween ψ ψ' τ)) s

The range of the re-modelled map is a closed submanifold of the re-modelled M of the same codimension, for the chart read through ψ (IsClosedSubmanifold.preimage_of_square along the identity M.transport ψ → M).

theorem AnalyticManifold.IsClosedAnalyticEmbedding.transportBetween {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {E₁ : Type u_3} {E₁' : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₁'] [NormedSpace 𝕜 E₁'] (ψ : E ≃L[𝕜] E₁) (ψ' : E' ≃L[𝕜] E₁') {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} {n₀ s : ℕ} {ψ₀ : E ≃L[𝕜] Fin n₀ → 𝕜} (hτ : IsClosedAnalyticEmbedding τ) (hS : Manifold.IsClosedSubmanifold ψ₀ (Set.range ⇑τ) s) : IsClosedAnalyticEmbedding (AnalyticManifold.transportBetween ψ ψ' τ)

The re-modelled map of a closed embedding of analytic manifolds whose image is a closed submanifold is a closed embedding: the same map of the same spaces, whose image is the closed submanifold IsClosedSubmanifold.range_transportBetween, through which the inclusion of that submanifold factors (through τ, after the identity M.transport ψ → M; IsClosedAnalyticEmbedding.of_isClosedSubmanifold).

theorem AnalyticManifold.stalkIdeal_idealSheaf_range_transportBetween_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {E₁ : Type u_3} {E₁' : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₁'] [NormedSpace 𝕜 E₁'] (ψ : E ≃L[𝕜] E₁) (ψ' : E' ≃L[𝕜] E₁') {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} {n₀ s : ℕ} {ψ₀ : E ≃L[𝕜] Fin n₀ → 𝕜} {n₁ : ℕ} {ψ₁ : E₁ ≃L[𝕜] Fin n₁ → 𝕜} (hS : Manifold.IsClosedSubmanifold ψ₀ (Set.range ⇑τ) s) (hS₁ : Manifold.IsClosedSubmanifold ψ₁ (Set.range ⇑(transportBetween ψ ψ' τ)) s) (I : M.IdealSheaf) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) (x : (M.transport ψ).carrier) : hS₁.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal (IdealSheaf.transport ψ I) x

The containment of the ideal sheaf of τ(N) in an ideal sheaf I, stalk by stalk, carries to the re-modelled manifold (IsClosedSubmanifold.idealSheaf_pullbackDiffeomorph).

theorem AnalyticManifold.IdealSheaf.transport_pullback_transportBetween {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} {E₁ : Type u_3} {E₁' : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₁'] [NormedSpace 𝕜 E₁'] (ψ : E ≃L[𝕜] E₁) (ψ' : E' ≃L[𝕜] E₁') {τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} (I : M.IdealSheaf) : transport ψ' (Manifold.IdealSheaf.pullback ⇑τ ⋯ I) = Manifold.IdealSheaf.pullback ⇑(transportBetween ψ ψ' τ) ⋯ (transport ψ I)

The re-modelled pull-back of an ideal sheaf along τ is the pull-back of the re-modelled ideal sheaf along the re-modelled map (both are the pull-back along the same map on points).