The mixed-pair transition of the common datum #
Two adjacent levels D₁, D₂ of the exhaustion are read on ONE common datum
S := sumPadData D₁ D₂ (the pieces of D₁ padded on the right by D₂.n coordinates, the pieces
of D₂ padded on the left by D₁.n, summed; CoproductSumData.lean), whose single run carries
the common labels ([Kol07, Proposition 37, proof]). At a point x of the domains of a piece i
of the first level and a piece j of the second, the mixed-pair transition is an isomorphism
over X between the parts over an open P ∋ x of the two padded pieces' local resolutions, under
which the common run's member of EVERY label on piece j pulls back to its member of the SAME
label on piece i — the agreement of the centres on the overlaps, (37.2) in
[Kol07, Proposition 37, proof].
The construction: restrict both pieces to the common open O' = pieceDom i ⊓ pieceDom j, take the
shear g of [Kol07, Lemma 39] between the padded restricted pieces at x
(exists_padded_equivalence_hom_point, LocalResolutionShear.lean, with its ideal identity hI,
its morphism identity hmor and its point clause hpt), read the shear's domain N₀ as ONE
admissible input T₀ with two open embeddings u = sigmaMk (inl i) ∘ ι₁⁺ ∘ ι_{W₁'} and
v = sigmaMk (inr j) ∘ ι₂⁺ ∘ ι_{W₂'} ∘ g into the sum's coproduct ambient — both pull the
coproduct triple back to T₀ (by hI) — and shrink to a relatively compact W₀ ∋ p₀. The
fixed-run device (FixedRunDevice.lean) identifies the local resolution Y₀ of T₀|W₀ with the
parts of the two pieces' local resolutions over P := domOpens (ι₁⁺ ι_{W₁'} W₀) through the two
open immersions localResolutionHomOn (isoOfRangeEq, the ranges by
MixedTransitionOpens.lean), the two spellings of the base open agree by ShearBaseOpens.lean,
and the members correspond by the device's synchronisation. The over-X clause is the
closed-subspace identity of ShearOverX.lean read through resIn_comp_localResolutionMapOn and
localResolutionHomOn_comp_map, the monomorphism homOfPullbackEq (restrictMap (sigmaMk …))
cancelled.
Three generic category lemmas do the associativity bookkeeping (comp_eq_of_over_ambient,
transition_over_eq_of_parts, comp_ofRestrict_eq_of_inv_comp). The transition is used by
CoproductGluedFamilyCompat.lean, CoproductLevelPair.lean and DoubledDatumLabels.lean. Not in
the sources beyond Kollár's proof; bookkeeping.
The compatibility of a device identification with the maps to the ambient closed subspaces,
before cancelling the monomorphism Hi — in any category.
The transition followed by the restriction and the open immersion is the first identification followed by the second device map.
The over-X clause of a transition assembled from two identifications of the parts with a
common space, the two maps to the ambient closed subspaces and the agreement of the read-down maps
— in any category.
The mixed-pair transition of the common datum ((37.2) in [Kol07, Proposition 37, proof];
[Kol07, Lemma 39] for the shear): at a point of the domains of a piece of the first level and a
piece of the second, an open P and an isomorphism over X between the parts over P of the two
padded pieces' local resolutions under which the common run's member of EVERY label on the second
piece pulls back to its member of the SAME label on the first.