The padded local resolution is the local resolution of the slice preimage, over the piece #
Kollár's weak commutation with closed embeddings, j^* B(X, I_X, E) = B(Y, I_Y, E|_Y)
[Kol07, 34.4], at the padding E.padAlong σ of a piece embedding: the field bed.closedEmbedding
of BEDanFamStar (the commutation with closed embeddings of ambient manifolds,
[Wlo09, Theorem 2.0.2(4)]) reads the padded sequence over a relatively compact open U of the
padded ambient as the restricted push-forward of the sequence of the coordinate slice
S = {z_j = 0, j ∉ range σ} over S ∩ U; the slice is the piece through the zero extension
padExt (the diffeomorphism padExtDiffeomorph, PadSliceDiffeomorph.lean), and the dimension
cast BEDanFamStar.exists_diffeomorph_last_of_cast (DimensionCast.lean, from the commutation
with local isomorphisms) carries the piece's own sequence over s⁻¹ U to the slice sequence.
StrictSubspacePushforward.lean identifies the final strict transform of the padded ideal,
restricted to the carried slice, with the final strict transform of the slice ideal
[Kol07, Definition 30.3], so the morphisms of closed subspaces along the last inclusion and along
the diffeomorphisms give the isomorphism of closed subspaces Ỹ_E(s⁻¹ U) ≅ Ỹ_P(U), and the
squares of the composites its compatibility with the maps to the piece. This module provides:
AnalyticManifold.FiniteSuccession.stageMap_pushforwardIncl(the inclusionsS_i ↪ X_icommute with the composites) andpushforwardIncl_eq_incl;PieceEmbedding.emb_comp_embInv_padAlong(E.emb ∘ P.emb⁻¹ = padSliceHom);- the core
PieceEmbedding.exists_closedSubmanifold_localResolution_padAlong: a closed submanifoldS_rof the padded last stage with𝓘_{S_r} ≤ Ỹ_P, a diffeomorphismG : Ỹ_E's stage≅ S_rwithỸ_E = (Ỹ_P)|_{S_r}transported alongG, and the square of the composites over the zero extension; PieceEmbedding.exists_isIso_localResolution_padAlong: the isomorphism over the piece.
The general forms #
exists_closedSubmanifold_last_pushforwardRestrict_boundary and
localResolutionToPiece_comp_homOfPullbackEq_padAlong are the general forms of the core and of
the isomorphism's body; the statements above are their corollaries. The general forms expose the
last-stage boundary's trace identity along j_r ∘ G
(exists_orderIso_totalTransformSeq_pushforward, PushforwardBoundaryTrace.lean) under the
normal-crossings clause (3′) of [Kol07, Definition 66], and the compatibility
Π_P ∘ (m_I ∘ m_G) = Π_E for any carried slice; the padding identity of a datum at the coproduct
(CoproductPadIdentity.lean) uses the first.
Not in the sources beyond the commutation with closed embeddings; bookkeeping.
The inclusions j_i : S_i ↪ X_i commute with the composites σ^i, ℕ-indexed
([Kol07, Definition 30.3]): by induction on the stage with pushforwardIncl_map. Internal.
The inclusions j_i : S_i ↪ X_i commute with the composites σ^i : X_i → X_0,
σ^i ∘ j_i = j_0 ∘ σ^i_S.
The stage T_i is diffeomorphic to the carried slice S_i (the identification
e_i : T_i ≃ S_i carried by the recursion of pushforwardAux), the inclusion j_i being the
inclusion of S_i after the diffeomorphism — the stage datum's iso read on the range of j_i
(range_incl, diffeomorphOfEq), case by case on the index.
The GENERAL FORM of exists_closedSubmanifold_last_pushforwardRestrict, of which that theorem
is the corollary ([Kol07, Definitions 30.2–30.3]): its three clauses, and, UNDER clause (3′) of
L_P (the centres have only normal crossings with the boundary at every stage): the last-stage
boundary of L_P has simple normal crossings with the carried slice S_r properly, and an order
isomorphism o of the last-stage boundary index types with (j_r ∘ G)⁻¹(H^P_{r, o j}) = H^S_{r, j}
— exists_orderIso_totalTransformSeq_pushforward on the transported list T, read back on L_S
along the lift of the bundling bridge (totalTransformSeqFrom_last_pullbackLiftLast).
The final strict transform along a restricted push-forward, read on the carried slice
([Kol07, Definition 30.3]): for a list L_S on the trace S ∩ U of the bundled S (no empty
centres) and a list L_P on U equal to its restricted push-forward, the final stage of L_P
carries a closed submanifold S_r whose ideal lies in the final strict transform Ỹ_P of I|_U, a
diffeomorphism G of the final stage of L_S onto S_r with Ỹ_S = G^*(Ỹ_P|_{S_r}) for the final
strict transform Ỹ_S of (I|_S)|_{S ∩ U} along L_S, and the square of the composites. The
argument: pushforwardRestrictOf_eq and toSuccession_pushforward (the family value has no empty
centres) put L_P's succession in the form T.pushforward (S ∩ U); the containment and the
restriction identity of StrictSubspacePushforward.lean at the last stage; the bundling bridge's
lift (pullbackLiftLastDiffeomorph, strictTransformSubspaceSeq_last_pullbackLiftLast') and the
stage datum's iso identify the last stages.
The piece embedding followed by the inverse of the padded embedding is the slice morphism:
E.emb ∘ (E.padAlong σ).emb⁻¹ = padSliceHom σ 𝓘 (padAlong's emb := padSliceIso.inv ∘ E.emb).
The final strict transform of the piece over s⁻¹ U is the final strict transform of the
padding over U restricted to a carried slice (the weak commutation with closed embeddings,
[Kol07, 34.4], at the padding; [Kol07, Definition 30.3]): a closed submanifold S_r of the padded
last stage whose ideal lies in Ỹ_P, a diffeomorphism G of the piece's last stage onto S_r,
Ỹ_E = G^*(Ỹ_P|_{S_r}), and the square of the composites over the zero extension. The argument: the
field bed.closedEmbedding rewrites the padded sequence as the restricted push-forward of the
slice sequence; exists_closedSubmanifold_last_pushforwardRestrict reads its final strict
transform on the carried slice; the slice sequence is the piece's sequence over s⁻¹ U through the
dimension cast (exists_diffeomorph_last_of_cast at padExtDiffeomorph, from the commutation
with local isomorphisms of hbed).
The body of exists_isIso_localResolution_padAlong, in general form: the compatibility over
the piece of the two quotient isomorphisms — for ANY carried slice S_r with G : M_E ≃ S_r
satisfying the core's strict-transform identity and square, the morphism of closed subspaces along
the inclusion of S_r after the one along G is compatible with the maps to the piece,
Π_P ∘ (m_I ∘ m_G) = Π_E. Read through emb_comp_embInv_padAlong, the slice morphism's square,
toAnalyticSpaceι_comp_restrictedIdealHom, localResolutionMap_comp_ι, the two squares of the
closed-subspace morphisms and the core's square of the composites, closed by
Hom.ext_of_comp_quotientι. The isomorphism theorem obtains S_r, G from the core.
The padded resolution is the resolution of the slice preimage, over the piece (the weak
commutation with closed embeddings, [Kol07, 34.4], at the padding E.padAlong σ, with
[Kol07, Definition 30.3] and the dimension cast): for a relatively compact open U of the padded
ambient, the local resolution of E.padAlong σ over U is isomorphic over the piece to the local
resolution of E over s⁻¹ U — the morphism of closed subspaces along the inclusion of the
carried slice (isIso_homOfPullbackEq_inclusionMap, the core's 𝓘_{S_r} ≤ Ỹ_P) and along the
core's diffeomorphism G (isIso_homOfPullbackEq_of_diffeomorph); the compatibility with the
maps to the piece through emb_comp_embInv_padAlong, the slice morphism's square,
toAnalyticSpaceι_comp_restrictedIdealHom, localResolutionMap_comp_ι, the two squares of the
closed-subspace morphisms and the core's square of the composites, closed by
Hom.ext_of_comp_quotientι.