Lemma 102 in the compatible-family form: commutation with local analytic isomorphisms #
Clause (2) of [Kol07, Lemma 102], the commutation of BD_{n,m,j} with smooth morphisms, for the
values on relatively compact opens (BDanFam, BDFam.lean), in the one-clause form of the family
functors (AnalyticFamilyFunctor.CommutesWithLocalIsos, both clauses of [Kol07, 34.1] at once):
for a local analytic isomorphism g : N → M, the value of the pulled-back data on U' ⊆ N is the
value on the image g(U') ⊆ M pulled back along g|_{U'}, with its empty blow-ups deleted
(BDanFam_commutesWithLocalIsos). Kollár's argument, that pulling back by h and then restricting
to E^j_Y gives "the same result" as restricting to E^j and then pulling back by h|_{E^j_Y}, is
carried out on the cores.
Both sides are cores over transported values (BDFamTransport.lean). The left side is first
rewritten over the centre g^{-1}(Z_{-1}) and the transform (lift g)^{-1}(S_0)
(coreFamOn_eq_coreOfListOf_of_eq, along BD.Zminus1_comap); the restricted triple there is the
pull-back of the restricted triple of T along the restricted lift g|_S
(restrictedTripleOf_isPullbackOf, BDOf.lean), so the input family's own commutation applies at
the trace U'_S. The image of U'_S under g|_S is the trace g(U')_S
(imageOpens_liftRestrictS_eq: the lift of g|_{U'} is surjective, and a point over g(U') is in
the range of the lift of the inclusion), the lift of g ∘ (U' ⊆ N) is the lift of
(g(U') ⊆ M) ∘ g|_{U'} (uniqueness of lifts, liftStep_restrictMap_comm), and the behaviour of the
core over a sequence under pull-back (BDFamPullback.lean) identifies the two cores.
coreFamOn_eq_coreOfListOf_of_eq— the core on an open over the transported value (transportedValueOf,BDFamTransport.lean) over an arbitrary centre and transform;heq_pullback_seqOn_of_eq— pull-backs of the values of a compatible family on equal opens along pointwise equal maps agree;liftRestrictS,liftStep_restrictMap_comm,imageOpens_liftRestrictS_eq,transformSU_restrictMap_eq— the restricted lift ofgand the bookkeeping of the two lifts;coreFamOn_commutesWithLocalIsos,coreFamOn_congr,BDanFam_commutesWithLocalIsos.
This is the commutesWithLocalIsos field of Lemma 102's family data bdanFamDataOfInput in
BOanFamOfInput.lean.
The transported value over an arbitrary centre and transform #
The core on an open is the core over the transported value, read over any centre Z = Z_{-1}
and transform S' = S_0 (coreFamOn_eq_coreOfListOf over an arbitrary centre).
Two pull-backs of a family value on equal opens #
Pull-backs of the values of a compatible family on two equal opens, along maps from two equal closed hypersurfaces agreeing pointwise, are equal (as heterogeneous equality, the domains being equal only propositionally).
Commutation of the core on an open with a local analytic isomorphism #
The restriction g|_S : (lift g)^{-1}(S_0) → S_0 of the lift of g to the transforms of E^j
(Kollár's h|_{E^j_Y} in the proof of [Kol07, Lemma 102]).
Equations
- Hironaka.Manifold.BDan.liftRestrictS T s j g hg = ⋯.restrictMap ⋯ ⇑(AnalyticManifold.BlowUpSequence.liftStep g hg ⋯) ⋯ ⋯
Instances For
The restricted lift g|_S is a local analytic isomorphism.
The lift of g ∘ (U' ⊆ N) to the blowings-up is the lift of (g(U') ⊆ M) ∘ g|_{U'}
(uniqueness of lifts, eq_of_comm_blowUp).
liftStep_restrictMap_comm, pointwise.
The image of the trace U'_S under the restricted lift g|_S is the trace g(U')_S: the lift
of g|_{U'} is surjective (surjective_liftStep), and a point of S_0 over g(U') is in the
range
of the lift of the inclusion (exists_liftStep_eq).
The transform of E^j pulled back along the lift of g|_{U'} is the transform of the
restricted
pulled-back data (transformSU_pullback_eq along g).
Clause (2) of [Kol07, Lemma 102] for the core on an open: the core of the pulled-back data on
U' is the core on g(U') pulled back along g|_{U'}, with its empty blow-ups deleted. Both sides
are cores over transported values on the same centre and transform; the transported values agree
because the input family commutes with the restricted lift g|_S at the trace U'_S, whose image
is the trace g(U')_S, and the two lifts compose as liftStep_restrictMap_comm says.
The core on an open depends only on the triple (used to pass between the tuning of a pull-back and the pull-back of the tuning).
Clause (2) of [Kol07, Lemma 102], "BD_{n,m,j} commutes with smooth morphisms", for the values
on relatively compact opens: for a local analytic isomorphism g : N → M, the value of the
pulled-back data on U' is the value on g(U') pulled back along g|_{U'} with its empty
blow-ups deleted (both clauses of [Kol07, 34.1] in the one-clause form of the family functors).
This is coreFamOn_commutesWithLocalIsos at the tuned triple, the tuning commuting with pull-back
(tuned_pullback).