The shrink-and-append step of a pulled-back list

The second general law behind the compatibility clause of the principalization family: the shrink-and-append step of the pulled-back list π^* L along j, up to empty rounds, is the step of L along the composite π ∘ j, whenever the two appended lists correspond along the last-stage lift of π restricted to the reading opens (pullbackLiftRestrict, the corestriction of pullbackLiftLast π). With shrinkAppend_pullback_eraseEmpty this reduces the comparison of the values of two disjoining lists related by a local analytic isomorphism to the commutation of the input family with local isomorphisms (CommutesWithLocalIsos; Kollár's functoriality for smooth morphisms [Kol07, 34.1], the pull-back of a blow-up sequence being [Kol07, 30.1]). Used by ValueNatural.lean.

theorem AnalyticManifold.BlowUpSequence.pullback_eraseEmpty_of_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X Y P : AnalyticManifold 𝕜 E} {R₁ : TopologicalSpace.Opens X.carrier} {R₂ : TopologicalSpace.Opens Y.carrier} (B₁ : BlowUpSequence ψ₀ (X.restrict R₁)) (B₂ : BlowUpSequence ψ₀ (Y.restrict R₂)) (l : AnalyticMap (X.restrict R₁) (Y.restrict R₂)) (hl : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑l) (hB : B₁.eraseEmpty = (B₂.pullback l hl).eraseEmpty) (c₁ : AnalyticMap P (X.restrict R₁)) (hc₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑c₁) (c₂ : AnalyticMap P (Y.restrict R₂)) (hc₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑c₂) (hcomp : ContMDiffMap.comp l c₁ = c₂) : (B₁.pullback c₁ hc₁).eraseEmpty = (B₂.pullback c₂ hc₂).eraseEmpty

The nil case in plain variables: the pull-backs of two lists corresponding along l agree up to empty rounds when the maps compose (eraseEmpty_pullback_eraseEmpty, pullback_comp, pullback_congr).

noncomputable def AnalyticManifold.BlowUpSequence.pullbackLiftRestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M X P : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (π : AnalyticMap X M) (hπ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑π) (j : AnalyticMap P X) (hj : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑j) (e : AnalyticMap P M) (he : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑e) (hcomp : ContMDiffMap.comp π j = e) : AnalyticMap (((L.pullback π hπ).stage (Fin.last (L.pullback π hπ).length)).restrict ((L.pullback π hπ).liftRange j hj)) ((L.stage (Fin.last L.length)).restrict (L.liftRange e he))

The last-stage lift of π, restricted to the reading open of j through π^* L and corestricted to the reading open of the composite π ∘ j through L (image_pullbackLiftLast_liftRange_subset).

Equations

• L.pullbackLiftRestrict π hπ j hj e he hcomp = Hironaka.Manifold.AnalyticMap.restrictMap (L.pullbackLiftLast π hπ) ((L.pullback π hπ).liftRange j hj) (L.liftRange e he) ⋯

theorem AnalyticManifold.BlowUpSequence.isLocalDiffeomorph_pullbackLiftRestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M X P : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (π : AnalyticMap X M) (hπ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑π) (j : AnalyticMap P X) (hj : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑j) (e : AnalyticMap P M) (he : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑e) (hcomp : ContMDiffMap.comp π j = e) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(L.pullbackLiftRestrict π hπ j hj e he hcomp)

theorem AnalyticManifold.BlowUpSequence.pullback_shrinkAppend_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M X P : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (π : AnalyticMap X M) (hπ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑π) (j : AnalyticMap P X) (hj : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑j) (e : AnalyticMap P M) (he : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑e) (hcomp : ContMDiffMap.comp π j = e) (B₁ : BlowUpSequence ψ₀ (((L.pullback π hπ).stage (Fin.last (L.pullback π hπ).length)).restrict ((L.pullback π hπ).liftRange j hj))) (B₂ : BlowUpSequence ψ₀ ((L.stage (Fin.last L.length)).restrict (L.liftRange e he))) : B₁.eraseEmpty = (B₂.pullback (L.pullbackLiftRestrict π hπ j hj e he hcomp) ⋯).eraseEmpty → ((L.pullback π hπ).shrinkAppend j hj B₁).eraseEmpty = (L.shrinkAppend e he B₂).eraseEmpty

The shrink-and-append step of a pulled-back list ([Kol07, 30.1; 34.1]). The step of π^* L along j, up to empty rounds, is the step of L along π ∘ j, whenever the appended lists correspond along the restricted last-stage lift of π (up to empty rounds). Induction on L; the cons step is liftStep_comp.