The push-forwards along a flag `S ⊂ Y ⊂ M` #

Kollár reduces the commutation of the order-reduction functor with a closed embedding S ⊂ M of codimension s + 1 to a flag S ⊂ Y ⊂ M with Y of codimension s and S a hypersurface of Y [Kol07, 108]; the push-forward of a blow-up sequence along a closed embedding is [Kol07, Definition 30.3]. This module is the push-forward bookkeeping of that reduction:

IsClosedSubmanifold.exists_diffeomorph_toAnalyticManifold_of_flag: for S ⊆ Y the two bundled structures on S — as a closed submanifold of M of codimension s + 1, as a hypersurface of the bundled Y — are carried by the identity of the carrier, an analytic isomorphism over M;
BlowUpSequence.noEmptyCenters_pushforwardRestrict': the per-open push-forward of a list without empty centres has none, at every codimension (noEmptyCenters_pushforwardRestrict of OrderReduction/ClosedEmbeddingFam.lean is the codimension-one case; the general one goes through pushforwardAux directly — the centres of the push-forward are the images of the centres under the closed embedding of each stage);
BlowUpSequence.pushforward_pushforward_of_flag: pushing a list forward from the hypersurface S of Y to Y and then from Y to M is pushing it forward from S to M. The first half is the nested stage PushforwardStage.nest: from a stage for Y ⊂ M (ambient X, strict transform Ỹ ⊆ X) and a stage for S ⊂ Y on its manifold (strict transform S̃ ⊆ T_Y), the stage for S ⊂ M with ambient X, sub j_Y(S̃) and the composed identification. The second half compares the next stages: the strict transform of j_Y(S̃) in Bl X is the image of the strict transform of S̃ in Bl Ỹ under the lifted closed embedding Bl Ỹ ↪ Bl X (image_incl_strictTransformSet), and the lifted inclusions agree by the uniqueness of lifts to a blowing-up (incl_nestStep; a blowing-up is unique up to an isomorphism commuting with the blow-down, [BM88, Definition 4.1]); this is the pull-back-stage invariant isPullbackStage_nestStep along the identity of Bl X, and the list induction pushforwardAux_nest follows through pushforwardAux_pullback;
BlowUpSequence.pushforward_pullback_inclusionMap_of_centersOver, the codimension-zero case: for S clopen in M with S ↪ M a local analytic isomorphism and a list whose centres lie over S (CentersOver, Principalization/IsoOff.lean), the push-forward along S of the pull-back along the inclusion is the list itself: the pushed-forward centres are the centres (Z ⊆ S), the lifted inclusion at each stage is THE lift of the inclusion (BlowUpSequence.eq_liftStep_of_comm), and the strict transform of the open S contains the whole preimage of S (IsBlowUp.dense_preimage_compl, at every codimension).

The internals are the stage blowUpStepOf (the next stage with the pushed-forward centre given as a datum W, so that the ambient of the next stage is blowUp ψ hW literally) with its subst-lemmas, and heq_pushforwardAux. Not in the sources beyond Kollár's reduction; the proofs are routine.

The push-forwards along a flag S ⊂ Y ⊂ M #

The two bundled structures on S ⊆ Y #

No empty centres through a push-forward, at every codimension #

The next stage with the pushed-forward centre as a datum #

Uniqueness of the lift of a local isomorphism #

The nested stage S ⊂ Y ⊂ M #

The next stage of the nested stage is the nested next stage #

The codimension-zero case #

The push-forwards along a flag `S ⊂ Y ⊂ M` #

The two bundled structures on `S ⊆ Y` #

The nested stage `S ⊂ Y ⊂ M` #