Włodarczyk's extension relation along the transport of a succession

Włodarczyk's extension relation between finite successions [Wlo09, Definition 3.2.6] (FiniteSuccession.IsExtensionOf) is carried along the transport transportAlong g ψ of Hironaka/Resolution/Analytic/ModelTransport/Succession.lean; the compatibility field of a transported compatible family (Family.lean) rests on it.

• IsExtensionOf.transportAlong: an extension T of S transports to an extension T.transportAlong g ψ of S.transportAlong g ψ — the same block index, the stage identifications conjugated by the stage identifications of the transports (transportAlongExtStage); the seven clauses follow from the identities of Succession.lean (the composite blow-downs stageMap_transportAlong, the blow-downs map_transportAlong, the centres center_transportAlong) and from the commutation of the composites between two stages (stageMapLE) with the identifications (stageMapLE_transportAlong, by the distance between the stages, as stageMapLE_pullbackLift of Hironaka/Resolution/Analytic/Functor/ExtensionOf.lean).
• isExtensionOf_restrict_transportAlong: the restriction of a transported succession to a smaller open is an extension of the transport of the restriction of the smaller succession — stage-wise isomorphic over the smaller open to the transport of the restriction (IsExtensionOf.of_stageEquiv_left): at stage 0 the identity, at a later stage the identity of the trace read from "re-model then restrict" to "restrict then re-model" (restrictTransportSwap; the two traces agree by stageMap_transportAlong), the blow-downs and centres of both being S's own read on the traces.

The auxiliaries of the restriction of a succession (stageMapLE, centerAt, the traces and data of FiniteSuccession.restrict) are used directly, as Hironaka/Resolution/Analytic/Functor/ExtensionOf.lean does.

The composites between two stages along the transport

theorem AnalyticManifold.FiniteSuccession.stageMapLE_transportAlong_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (a : Fin (S.length + 1)) (d : ℕ) (hd : ↑a + d < S.length + 1) (hab : a ≤ ⟨↑a + d, hd⟩) (q : ((transportAlong g ψ S).stage ⟨↑a + d, hd⟩).carrier) : (S.stageMapLE hab) ((transportAlongStage g ψ S ⟨↑a + d, hd⟩) q) = (transportAlongStage g ψ S a) (((transportAlong g ψ S).stageMapLE hab) q)

The composites σ_{a+1} ∘ ⋯ ∘ σ_b between two stages (stageMapLE) commute with the stage identifications, by the distance between the stages (as stageMapLE_pullbackLift_aux): the identity at distance 0, one more blow-down and the square map_transportAlong at each step.

theorem AnalyticManifold.FiniteSuccession.stageMapLE_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) {a b : Fin (S.length + 1)} (hab : a ≤ b) (q : ((transportAlong g ψ S).stage b).carrier) : (S.stageMapLE hab) ((transportAlongStage g ψ S b) q) = (transportAlongStage g ψ S a) (((transportAlong g ψ S).stageMapLE hab) q)

The composites between two stages commute with the stage identifications.

The extension relation along the transport

noncomputable def AnalyticManifold.FiniteSuccession.transportAlongExtStage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) {T : N.FiniteSuccession} (blk : Fin (T.length + 1) → Fin (S.length + 1)) (e : (k : Fin (T.length + 1)) → Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E') (T.stage k).carrier (S.stage (blk k)).carrier ⊤) (k : Fin (T.length + 1)) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ((transportAlong g ψ T).stage k).carrier ((transportAlong g ψ S).stage (blk k)).carrier ⊤

The stage identification of an extension, conjugated by the stage identifications of the transports: e'_k = (stage_S (blk k))⁻¹ ∘ e_k ∘ stage_T k.

Equations

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

theorem AnalyticManifold.FiniteSuccession.transportAlongStage_transportAlongExtStage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) {T : N.FiniteSuccession} (blk : Fin (T.length + 1) → Fin (S.length + 1)) (e : (k : Fin (T.length + 1)) → Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E') (T.stage k).carrier (S.stage (blk k)).carrier ⊤) (k : Fin (T.length + 1)) (p : ((transportAlong g ψ T).stage k).carrier) : (transportAlongStage g ψ S (blk k)) ((transportAlongExtStage g ψ S blk e k) p) = (e k) ((transportAlongStage g ψ T k) p)

The conjugated identification, read through the stage identification of S, is e_k after the stage identification of T.

theorem AnalyticManifold.FiniteSuccession.IsExtensionOf.transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) {T : N.FiniteSuccession} (h : T.IsExtensionOf S) : (FiniteSuccession.transportAlong g ψ T).IsExtensionOf (FiniteSuccession.transportAlong g ψ S)

Włodarczyk's extension relation [Wlo09, Definition 3.2.6] transports along g: the same block index, the identifications conjugated by the stage identifications; the "over the base" clause by stageMap_transportAlong on both sides, the intertwining clause by stageMapLE_transportAlong and map_transportAlong, the centres by center_transportAlong and the pull-back calculus, the empty centres by support_pullbackDiffeomorph.

The restriction of a transported succession

noncomputable def AnalyticManifold.FiniteSuccession.restrictTransportSwap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (ψ : E' ≃L[𝕜] E) {X : AnalyticManifold 𝕜 E'} (V : TopologicalSpace.Opens (X.transport ψ).carrier) (V' : TopologicalSpace.Opens X.carrier) (hV : ∀ (p : X.carrier), X.toTransport ψ p ∈ V ↔ p ∈ V') : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ((X.transport ψ).restrict V).carrier ((X.restrict V').transport ψ).carrier ⊤

The identity of a trace, from "re-model then restrict" to "restrict then re-model": an analytic isomorphism when the two opens are the same set (the typed identities of Hironaka/Resolution/Analytic/ModelTransport/Manifold.lean, contMDiff_codRestrict_opens).

Equations

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

theorem AnalyticManifold.FiniteSuccession.isExtensionOf_restrict_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ' : E ≃L[𝕜] E') {U₁ U₂ : TopologicalSpace.Opens M.carrier} (h : U₁ ≤ U₂) (S₂ : ((M.transport ψ').restrict U₂).FiniteSuccession) (S₁ : ((M.transport ψ').restrict U₁).FiniteSuccession) (hS : (S₂.restrict h).IsExtensionOf S₁) : ((transportAlong (M.restrictTransportDiffeomorph ψ' U₂) ψ'.symm S₂).restrict h).IsExtensionOf (transportAlong (M.restrictTransportDiffeomorph ψ' U₁) ψ'.symm S₁)

The restriction of the transported succession to a smaller open is an extension of the transport of the restricted smaller succession: the compatibility field of a transported compatible family (Family.lean). The restriction of the transport is stage-wise isomorphic over U₁ to the transport of the restriction (IsExtensionOf.of_stageEquiv_left): at stage 0 the identity of U₁, at a later stage restrictTransportSwap (the traces agree by stageMap_transportAlong), the composite blow-downs read in M by val_stageMap_restrict, the blow-downs and the centres of both being S₂'s own on the traces (definitionally, up to the pull-back calculus); then IsExtensionOf.transportAlong on the extension of the restriction.