The two bundlings of a restricted closed submanifold

A closed submanifold S ⊆ M read over an open U ⊆ M carries two analytic structures on the same carrier S ∩ U: the open subset U_S := inclusionMap ⁻¹' U of the bundled S ((hS.toAnalyticManifold).restrict U_S) and the bundling of S ∩ U as a closed submanifold of M.restrict U ((hS.restrictOpen U).toAnalyticManifold, via IsClosedSubmanifoldOn.restrict). They agree up to an analytic isomorphism over the identity of the carrier (restrictBundleDiffeomorph); with it a list of centres on the first is pushed forward to M.restrict U (BlowUpSequence.pushforwardRestrict, the PushforwardStage recursion of Pushforward.lean with the isomorphism as its iso field), and the push-forward is the ordinary one of the list transported along the isomorphism (pushforwardRestrict_eq). This is the bookkeeping behind the push-forward τ_* BMO_{n-1,1}(Y, J, 1, ∅) from a hypersurface of maximal contact in [Kol07, Theorem 103(3)], read over each open of a cover; the push-forward of a blow-up sequence is [Kol07, Definition 30.3], its behaviour under open embeddings [Kol07, 34.1]. Not in the sources; routine.

@[reducible, inline]

noncomputable abbrev Manifold.IsClosedSubmanifold.preimageOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (U : TopologicalSpace.Opens M.carrier) : TopologicalSpace.Opens hS.toAnalyticManifold.carrier

The open U_S := inclusionMap ⁻¹' U of the bundled submanifold — the instance at the closed embedding inclusionMap of the general preimageOpens φ hφ U, whose mem_preimageOpens reads p ∈ U_S ↔ (p : S).1 ∈ U.

Equations

• hS.preimageOpens U = Manifold.preimageOpens ⇑hS.inclusionMap ⋯ U

theorem Manifold.IsClosedSubmanifold.isCompact_closure_preimageOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : IsCompact (closure ↑(hS.preimageOpens U))

U_S is relatively compact in S when U is relatively compact in M (S is closed).

theorem Manifold.IsClosedSubmanifold.restrictOpen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (U : TopologicalSpace.Opens M.carrier) : IsClosedSubmanifold ψ (⇑(M.inclusion U) ⁻¹' S) s

S ∩ U as a closed submanifold of the open subset U (IsClosedSubmanifoldOn.restrict at isClosedSubmanifoldOn').

def Manifold.IsClosedSubmanifold.restrictBundleDiffeomorphOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (V : TopologicalSpace.Opens M.carrier) (W : TopologicalSpace.Opens hS.toAnalyticManifold.carrier) (hW : ↑W = ⇑hS.inclusionMap ⁻¹' ↑V) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (hS.toAnalyticManifold.restrict W).carrier ⋯.toAnalyticManifold.carrier ⊤

The bundling bridge (general form): for an open V ⊆ M and an open W of the bundled S whose underlying set is inclusionMap ⁻¹' V, the identity of the carrier S ∩ V as an analytic isomorphism from the open W of the bundled S to the bundled closed submanifold S ∩ V of M.restrict V (Kollár's remark that for all practical purposes Z_i^X = Z_i^S, [Kol07, Definition 30.3]).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Manifold.IsClosedSubmanifold.restrictBundleDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (U : TopologicalSpace.Opens M.carrier) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (hS.toAnalyticManifold.restrict (hS.preimageOpens U)).carrier ⋯.toAnalyticManifold.carrier ⊤

The bridge at the canonical open U_S := hS.preimageOpens U (V := U).

Equations

• hS.restrictBundleDiffeomorph U = hS.restrictBundleDiffeomorphOf U (hS.preimageOpens U) ⋯

noncomputable def Manifold.IsClosedSubmanifold.restrictStageOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (V : TopologicalSpace.Opens M.carrier) (W : TopologicalSpace.Opens hS.toAnalyticManifold.carrier) (hW : ↑W = ⇑hS.inclusionMap ⁻¹' ↑V) : PushforwardStage ψ s (hS.toAnalyticManifold.restrict W)

The push-forward stage of S ∩ V ⊆ M.restrict V read from the open W of the bundled S — the bridge fills the stage's iso ([Kol07, Definition 30.3]).

Equations

• hS.restrictStageOf V W hW = { space := M.restrict V, sub := ⇑(M.inclusion V) ⁻¹' S, isClosedSubmanifold := ⋯, iso := hS.restrictBundleDiffeomorphOf V W hW }

noncomputable def AnalyticManifold.BlowUpSequence.pushforwardRestrictOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (V : TopologicalSpace.Opens M.carrier) (W : TopologicalSpace.Opens hS.toAnalyticManifold.carrier) (hW : ↑W = ⇑hS.inclusionMap ⁻¹' ↑V) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.toAnalyticManifold.restrict W)) : BlowUpSequence ψ (M.restrict V)

The push-forward to M.restrict V of a list of centres on an open W of the bundled S whose underlying set is inclusionMap ⁻¹' V (the trace of V on S; the image of W is then closed in V, which a push-forward stage requires): [Kol07, Definition 30.3] over one open.

Equations

• AnalyticManifold.BlowUpSequence.pushforwardRestrictOf hS V W hW L = AnalyticManifold.BlowUpSequence.pushforwardAux (hS.restrictStageOf V W hW) L

@[reducible, inline]

noncomputable abbrev AnalyticManifold.BlowUpSequence.pushforwardRestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (U : TopologicalSpace.Opens M.carrier) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.toAnalyticManifold.restrict (hS.preimageOpens U))) : BlowUpSequence ψ (M.restrict U)

The push-forward over one open at the canonical open U_S := hS.preimageOpens U ([Kol07, Definition 30.3]).

Equations

• AnalyticManifold.BlowUpSequence.pushforwardRestrict hS U L = AnalyticManifold.BlowUpSequence.pushforwardRestrictOf hS U (hS.preimageOpens U) ⋯ L

theorem AnalyticManifold.BlowUpSequence.pushforwardRestrictOf_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (V : TopologicalSpace.Opens M.carrier) (W : TopologicalSpace.Opens hS.toAnalyticManifold.carrier) (hW : ↑W = ⇑hS.inclusionMap ⁻¹' ↑V) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.toAnalyticManifold.restrict W)) : pushforwardRestrictOf hS V W hW L = pushforward ⋯ (L.pullback ⟨⇑(hS.restrictBundleDiffeomorphOf V W hW).symm, ⋯⟩ ⋯)

The per-open push-forward is the ordinary push-forward (BlowUpSequence.pushforward) of the list transported along the bridge.