Deleting the empty blow-ups of a concatenation #
The second step of the proof of [Kol07, Theorem 103] concatenates the sequence built so far with a
sequence on its last stage, and the functors of this library delete the empty blow-ups
([Kol07, 34.1]: delete and reindex). To read the deletion through the concatenation one needs,
as for schemes (AlgebraicGeometry.eraseEmpty_concat of
Hironaka.Scheme.BlowUpSequence.EraseEmptyConcat), the isomorphism between the last stage of a list
and the last stage of the cleaned list, the composite of the lifts of the isomorphisms Bl_∅ ≃ M of
the deleted empty blowings-up, and the identity
(A ++ B).eraseEmpty = A.eraseEmpty ++ (B transported along that isomorphism).eraseEmpty.
This file builds that isomorphism, BlowUpSequence.eraseEmptyLast, proves that it lies over the
base (stageMap_last_eraseEmptyLast, the analogue of eraseEmptyLastHom_comp_composite of
Hironaka.Resolution.Algebraic.Kol07.EraseEmptyInduced), and proves
BlowUpSequence.eraseEmpty_concat and eraseEmpty_concat_eraseEmpty, with the general transport
tools it needs: the last-stage isomorphism mapLast of a transported list, the functoriality of
map (map_refl, map_map, map_concat), and its commutation with the deletion of empty blow-ups
(eraseEmpty_map). The casts along the two computation rules of eraseEmpty (stageOfEq) are
unavoidable: eraseEmpty decides Y = ∅ classically, so (cons hY rest).eraseEmpty does not
reduce definitionally (the version for schemes uses eqToHom for the same reason).
The last stage of a transported list #
The isomorphism of last stages induced by the transport map g of a list along g : M ≃ N:
the composite of the lifts liftDiffeomorph (the analogue of pullbackLastHom for schemes).
Equations
Instances For
The last-stage isomorphism of a transported list lies over g: Π' ∘ g_r = g ∘ Π for the
composite blow-downs Π, Π' of the list and of its transport.
Functoriality of the transport along diffeomorphisms #
The transport along the identity is the identity (via map_eq_pullback_symm and
pullback_id).
The transport along a composite is the composite of the transports (via
map_eq_pullback_symm and pullback_comp).
The transport of a concatenation is the concatenation of the transports, the second piece
transported along the last-stage isomorphism mapLast of the first (the analogue of
pullback_concat for schemes).
Deleting the empty blow-ups commutes with the transport along a diffeomorphism (the surjective
case of eraseEmpty_pullback, read through map_eq_pullback_symm).
Casts along an equality of lists #
The identification of the last stages of two equal lists (the analogue of eqToHom (congrArg BlowUpSequence.last e) for schemes).
Equations
Instances For
Transport of the second piece of a concatenation along an equality of first pieces: the cast
is absorbed (concat_pullback_eqToHom).
The last-stage isomorphism of the deletion of empty blow-ups #
One step of eraseEmptyLast (the shape of eraseEmptyCons): given the last-stage isomorphism
T of the tail, the last-stage isomorphism of cons hY rest — at an empty step T followed by
the lift mapLast of Bl_∅ M ≃ M (the transport eraseEmpty performs), at a nonempty step T
itself; each followed by the cast along the computation rule of eraseEmpty at that step.
Equations
- One or more equations did not get rendered due to their size.
Instances For
[Kol07, 34.1], the analogue of eraseEmptyLastHom for schemes: the isomorphism from
the last stage of a list to the last stage of its cleaned list — by recursion, one step
eraseEmptyLastCons per centre.
Equations
- One or more equations did not get rendered due to their size.
- (AnalyticManifold.BlowUpSequence.cons hY rest).eraseEmptyLast = AnalyticManifold.BlowUpSequence.eraseEmptyLastCons hY rest rest.eraseEmptyLast
Instances For
The last-stage isomorphism of the deletion lies over the base: the composite blow-down of the
cleaned list after it is the composite blow-down of the list (eraseEmptyLastHom_comp_composite
for schemes; [Kol07, 34.1], the deleted blowings-up are isomorphisms Bl_∅ M ≃ M over M).
Deleting the empty blow-ups of a concatenation #
[Kol07, 32] and [Kol07, 34.1] for the concatenation in the second step of the proof of
[Kol07, Theorem 103]; the analogue of eraseEmpty_concat for schemes: deleting the empty blow-ups
of a concatenation is deleting them in the first list, then in the second transported along the
last-stage isomorphism of the first.
Deleting the empty blow-ups of a concatenation whose second piece is already clean is deleting
them from the concatenation itself (eraseEmpty_concat_eraseEmpty).