Włodarczyk's extension relation: its calculus

FiniteSuccession.IsExtensionOf T S ([Wlo09, Definition 3.2.6]) says that T is a sequence of blow-ups and isomorphisms whose blow-ups are those of S: a block index blk, identifications e k over the base, the maps intertwined through the composites stageMapLE between two stages, the centres carried at the jumps, empty at the non-jumps. This module proves what the limit construction of the compatible families needs of it:

• the two computation rules of stageMapLE (Nat.leRecOn_self, Nat.leRecOn_succ): from stage 0 it is the composite blow-down (stageMapLE_zero_left), on cons between later stages it is the tail's (stageMapLE_cons), and the stage lifts of a pull-back intertwine it (stageMapLE_pullbackLift);
• reflexivity (IsExtensionOf.refl) and the composition with a stage-wise isomorphism over the base on the left (IsExtensionOf.of_stageEquiv_left);
• the remark following [Wlo09, Definition 3.2.6], with [Kol07, 32] and [Kol07, 34.1]: a list's succession is an extension of its cleaned list's succession (isExtensionOf_toSuccession_eraseEmpty); a nonempty first centre is a jump (isExtensionOf_toSuccession_cons), an empty one a non-jump whose identification is Bl_∅ M ≃ M (isExtensionOf_toSuccession_cons_of_eq_empty);
• [Wlo09, Theorem 2.0.3, (4)]: the restriction of a list's succession to an open U₁ ≤ U₂ is stage-wise isomorphic over U₁ to its pull-back along the open inclusion, hence an extension of whatever the pull-back is an extension of (isExtensionOf_restrict_toSuccession_of_pullback; val_stageMap_restrict reads its composite blow-down in M).

The auxiliaries stageMapLE and centerAt of the definition are used directly.

The composite stageMapLE between two stages

theorem AnalyticManifold.FiniteSuccession.stageMapLE_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (a : Fin (S.length + 1)) (h : a ≤ a) : S.stageMapLE h = ContMDiffMap.id

At equal indices the composite σ_{a+1} ∘ ⋯ ∘ σ_a is the identity.

theorem AnalyticManifold.FiniteSuccession.stageMapLE_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {a : Fin (S.length + 1)} {b : Fin S.length} (h : a ≤ b.succ) (h' : a ≤ b.castSucc) : S.stageMapLE h = ContMDiffMap.comp (S.stageMapLE h') (S.map b)

One more step: the composite to b + 1 is the composite to b after σ_{b+1}.

theorem AnalyticManifold.FiniteSuccession.stageMapLE_zero_left_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (m : ℕ) (hm : m < S.length + 1) (h : 0 ≤ ⟨m, hm⟩) : S.stageMapLE h = S.stageMap ⟨m, hm⟩

ℕ-indexed.

theorem AnalyticManifold.FiniteSuccession.stageMapLE_zero_left {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (b : Fin (S.length + 1)) (h : 0 ≤ b) : S.stageMapLE h = S.stageMap b

From stage 0: the composite σ_1 ∘ ⋯ ∘ σ_b is the composite blow-down σ^b (stageMap) — so at a stage identified with stage 0 the intertwining clause of IsExtensionOf is its "over M" clause.

theorem AnalyticManifold.FiniteSuccession.stageMapLE_cons_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (R : (Manifold.blowUp ψ₀ hY).FiniteSuccession) (a : Fin (R.length + 1)) (d : ℕ) (hd : ↑a + d < R.length + 1) (h : a.succ ≤ ⟨↑a + d, hd⟩.succ) (h' : a ≤ ⟨↑a + d, hd⟩) : (cons ψ₀ hY R).stageMapLE h = R.stageMapLE h'

By the distance d between the two stages.

theorem AnalyticManifold.FiniteSuccession.stageMapLE_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (R : (Manifold.blowUp ψ₀ hY).FiniteSuccession) {a b : Fin (R.length + 1)} (h : a.succ ≤ b.succ) (h' : a ≤ b) : (cons ψ₀ hY R).stageMapLE h = R.stageMapLE h'

On cons hY R between two later stages the composite is R's composite.

The extension relation: reflexivity and composition with a stage-wise isomorphism

theorem AnalyticManifold.FiniteSuccession.comap_diffeomorph_refl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(Diffeomorph.refl (modelWithCornersSelf 𝕜 E) M.carrier ⊤) ⋯ J = J

The pull-back of an ideal sheaf along the identity diffeomorphism is the ideal sheaf.

theorem AnalyticManifold.FiniteSuccession.comap_diffeomorph_trans {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A B C : AnalyticManifold 𝕜 E} (e₁ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤) (e₂ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) B.carrier C.carrier ⊤) (J : C.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(e₁.trans e₂) ⋯ J = Manifold.IdealSheaf.pullback ⇑e₁ ⋯ (Manifold.IdealSheaf.pullback ⇑e₂ ⋯ J)

The pull-back along a composite of diffeomorphisms is the iterated pull-back.

theorem AnalyticManifold.FiniteSuccession.IsExtensionOf.refl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) : S.IsExtensionOf S

Every succession is an extension of itself (the block index the identity).

theorem AnalyticManifold.FiniteSuccession.IsExtensionOf.of_stageEquiv_left {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {T S R : M.FiniteSuccession} (hlen : T.length = S.length) (e : (k : Fin (T.length + 1)) → Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (T.stage k).carrier (S.stage (Fin.cast ⋯ k)).carrier ⊤) (hover : ∀ (k : Fin (T.length + 1)) (p : (T.stage k).carrier), (S.stageMap (Fin.cast ⋯ k)) ((e k) p) = (T.stageMap k) p) (hmap : ∀ (k : Fin T.length) (p : (T.stage k.succ).carrier), (S.map (Fin.cast hlen k)) ((e k.succ) p) = (e k.castSucc) ((T.map k) p)) (hcenter : ∀ (k : Fin T.length), T.center k = Manifold.IdealSheaf.pullback ⇑(e k.castSucc) ⋯ (S.center (Fin.cast hlen k))) (hSR : S.IsExtensionOf R) : T.IsExtensionOf R

A succession T stage-wise isomorphic OVER M to S (same length, the isomorphisms intertwining the maps and carrying the centres) is an extension of everything S is an extension of: compose the block index with the identity and the identifications.

The restriction to an open, read in M

theorem AnalyticManifold.FiniteSuccession.val_stageMap_restrict_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U₁ U₂ : TopologicalSpace.Opens M.carrier} (S : (M.restrict U₂).FiniteSuccession) (h : U₁ ≤ U₂) (m : ℕ) (hm : m + 1 < S.length + 1) (p : ((S.restrict h).stage ⟨m + 1, hm⟩).carrier) : ↑(((S.restrict h).stageMap ⟨m + 1, hm⟩) p) = ↑((S.stageMap ⟨m + 1, hm⟩) ↑p)

ℕ-indexed: the composite blow-down of the restriction at a later stage, in M.

theorem AnalyticManifold.FiniteSuccession.val_stageMap_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U₁ U₂ : TopologicalSpace.Opens M.carrier} (S : (M.restrict U₂).FiniteSuccession) (h : U₁ ≤ U₂) (k : Fin S.length) (p : ((S.restrict h).stage k.succ).carrier) : ↑(((S.restrict h).stageMap k.succ) p) = ↑((S.stageMap k.succ) ↑p)

The composite blow-down of the restriction at a later stage, read in M, is the composite blow-down of the succession at the point (the traces are open submanifolds and the restricted maps are the maps).

theorem AnalyticManifold.BlowUpSequence.stageMapLE_pullbackLift_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (a : Fin (L.length + 1)) (d : ℕ) (hd : ↑a + d < L.length + 1) (hab : a ≤ ⟨↑a + d, hd⟩) (hab' : ⟨↑a, ⋯⟩ ≤ ⟨↑a + d, ⋯⟩) (q : ((L.pullback h hh).stage ⟨↑a + d, ⋯⟩).carrier) : (L.toSuccession.stageMapLE hab) ((L.pullbackLift h hh ⟨↑a + d, hd⟩) q) = (L.pullbackLift h hh a) (((L.pullback h hh).toSuccession.stageMapLE hab') q)

By the distance between the two stages.

theorem AnalyticManifold.BlowUpSequence.stageMapLE_pullbackLift {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {a b : Fin (L.length + 1)} (hab : a ≤ b) (hab' : ⟨↑a, ⋯⟩ ≤ ⟨↑b, ⋯⟩) (q : ((L.pullback h hh).stage ⟨↑b, ⋯⟩).carrier) : (L.toSuccession.stageMapLE hab) ((L.pullbackLift h hh b) q) = (L.pullbackLift h hh a) (((L.pullback h hh).toSuccession.stageMapLE hab') q)

The stage lifts intertwine the composites stageMapLE between any two stages (map_pullbackLift along Nat.leRecOn).

A list's succession is an extension of its cleaned list's succession

theorem AnalyticManifold.BlowUpSequence.isExtensionOf_toSuccession_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) {rest R : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)} (hR : rest.toSuccession.IsExtensionOf R.toSuccession) : (cons hY rest).toSuccession.IsExtensionOf (cons hY R).toSuccession

(a jump). Prepending the same centre to both lists keeps the extension: the first step of cons hY rest is the first step of cons hY R, the identification there the identity.

theorem AnalyticManifold.BlowUpSequence.isExtensionOf_toSuccession_cons_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) {rest R : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)} (hR : rest.toSuccession.IsExtensionOf R.toSuccession) : (cons hY rest).toSuccession.IsExtensionOf (map (emptyBlowUpDiffeomorph hY hY₀) R).toSuccession

(a non-jump). Prepending an EMPTY centre to rest and transporting R back along the isomorphism Bl_∅ M ≃ M of the empty blowing-up (the step eraseEmpty performs) keeps the extension: the first step of cons hY rest is the non-jump e 1 = Bl_∅ M ≃ M, over M by emptyBlowUpDiffeomorph_apply; the later identifications are R's followed by the inverses of the stage lifts of g⁻¹ (map_eq_pullback_symm).

theorem AnalyticManifold.BlowUpSequence.isExtensionOf_toSuccession_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : L.toSuccession.IsExtensionOf L.eraseEmpty.toSuccession

The remark following [Wlo09, Definition 3.2.6], with [Kol07, 32] and [Kol07, 34.1]: a list's succession is an extension of its cleaned list's succession, by recursion on the list (isExtensionOf_toSuccession_cons, isExtensionOf_toSuccession_cons_of_eq_empty).

The restriction to an open against the pull-back along the open inclusion

theorem AnalyticManifold.BlowUpSequence.isExtensionOf_restrict_toSuccession_of_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {U₁ U₂ : TopologicalSpace.Opens M.carrier} (L : BlowUpSequence ψ₀ (M.restrict U₂)) (h : U₁ ≤ U₂) {R : (M.restrict U₁).FiniteSuccession} (hR : (L.pullback (M.restrictLE h) ⋯).toSuccession.IsExtensionOf R) : (L.toSuccession.restrict h).IsExtensionOf R

([Wlo09, Theorem 2.0.3] (4)). For a list L over U₂ and U₁ ≤ U₂, the restriction of its succession to U₁ is an extension of everything the succession of its pull-back along the open inclusion is an extension of — the two are stage-wise isomorphic over U₁: stage 0 is U₁ on both sides, and at a later stage the lift h_i of the inclusion is a diffeomorphism from the pull-back's stage onto the trace (pullbackLiftDiffeomorph).