The fixed-run device: two local isomorphisms with the same pulled-back triple

Kollár descends the blow-up sequence of the disjoint union X' = ⊔ Uᵢ of an affine cover to X through the two surjective open immersions τ₁, τ₂ : X'' → X' from X'' = ⊔ Uᵢ ∩ Uⱼ: since the functor commutes with τ₁ and τ₂, the pulled-back centres agree, τ₁^* Z₀' = Z₀'' = τ₂^* Z₀' ((37.1) in [Kol07, Proposition 37, proof]), because the functor commutes with smooth surjections [Kol07, 34.1]. Here the synchronisation of two runs is obtained by running the functor on ONE input P with two SURJECTIVE local analytic isomorphisms a b : P → M onto the same fixed reading open — the device of seq_pullback_eq_eraseEmpty (Functor/LocalIsoTools.lean, the sequence level) at the FAMILY level, where bed.seqOn is what the runs are. The clause of the family functor is CommutesWithLocalIsos (Functor/Family.lean): the value on the pulled-back triple over U' is the pull-back along g|U' of the value over the image open with the empty blow-ups ERASED; for a SURJECTION onto the fixed reading open the erasure is a no-op (eraseEmpty_pullback_of_surjective, Functor/PullbackInj.lean; the first bullet of [Kol07, 34.1]), so the identity holds as an equality of WHOLE CenterLists, stage by stage — the same fact CommutesWithSurjectiveLocalIsos (Functor/Basic.lean; its consequence commutesWith in Functor/SigmaTriple.lean) states at the sequence level.

• seqOn_pullback_eq_of_isLocalDiffeomorph — seqOn_eq_of_isAnalyticOpenEmbedding (LocalResolutionOn.lean) for an arbitrary local analytic isomorphism a in place of an open embedding: the value on T.pullback a over U' is the erased pull-back along a|U' : U' → V of the value over any relatively compact V ⊇ a(U') (the clause at a and U', the family's restriction compatibility from a(U') up to V, eraseEmpty_pullback_eraseEmpty, pullback_comp — the same proof);
• seqOn_pullback_eq_of_pullback_eq — the device: two local isomorphisms a b : P → M with the SAME pulled-back triple (T.pullback a = T.pullback b) whose images of the reading open U' are BOTH the fixed open V (the reading-open hypothesis, in the binders) pull the run over V back to the SAME list. Nothing here is specific to a particular functor: the lemma holds for every bed under hbed : bed.IsEmbeddedDesing.
• the coproduct maps: AnalyticTriple.pullback_sigmaDescMap_sumDesc_eq — two local isomorphisms u v : N → M with the same pulled-back triple give the same pulled-back triple along sigmaDescMap (sumDesc u), sigmaDescMap (sumDesc v) : M ⊔ N → M (id on the M summand; an ideal sheaf on a disjoint union is determined by its restrictions to the summands, IdealSheaf.ext_of_comap_sigmaMk, stalkwise along the bijective germ maps of the inclusions), domBEDan_pullback_sigmaDescMap_sumDesc (the coproduct input is admissible), and BlowUpSequence.pullback_eq_of_pullback_sigmaDescMap_sumDesc_eq (the whole-list equality read on the N summand through sumInl, pullback_comp, sigmaDescMap_comp_sigmaMk).

The generic reading on a summand of N ⊔ M and the form with synchronised members — Kollár's (37.2) for the FIXED member of a stage — are in FixedRunDevice.lean; the instance with the shear g of exists_padded_equivalence_hom_point (u, v the two embeddings of the shear's domain into the common datum's coproduct ambient) is exists_mixedTransition_sumPadData in CoproductMixedTransition.lean. IsEmbeddedDesing enters only through hbed. Not in the sources beyond Kollár's descent; bookkeeping.

theorem Hironaka.Manifold.BEDanFamStar.seqOn_congr_triple {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T₁ T₂ : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (e : T₁ = T₂) (h₁ : DomBEDan 𝕜 T₁) (h₂ : DomBEDan 𝕜 T₂) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) : bed.seqOn T₁ h₁ W hW = bed.seqOn T₂ h₂ W hW

The value of the functor depends only on the triple — the transport along an equality of triples, DomBEDan being a proposition.

theorem Hironaka.Manifold.BEDanFamStar.seqOn_pullback_eq_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M P : AnalyticManifold 𝕜 (Fin n → 𝕜)} (hbed : IsEmbeddedDesing 𝕜 bed) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (a : AnalyticMap P M) (ha : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑a) (hTa : DomBEDan 𝕜 (T.pullback a ha)) (U' : TopologicalSpace.Opens P.carrier) (hU' : IsCompact (closure ↑U')) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hle : ⇑a '' ↑U' ⊆ ↑V) : bed.seqOn (T.pullback a ha) hTa U' hU' = ((bed.seqOn T hT V hV).pullback (AnalyticMap.restrictMap a U' V hle) ⋯).eraseEmpty

seqOn_eq_of_isAnalyticOpenEmbedding for a local isomorphism ([Kol07, 34.1]): for an arbitrary local analytic isomorphism a : P → M (not only an open embedding) the value on the pulled-back triple over U' is the pull-back along a|U' : U' → V of the value over V ⊇ a(U'), empty blow-ups erased — hbed's CommutesWithLocalIsos at a and U' (onto the image open a(U')), the family's restriction compatibility from a(U') up to V, eraseEmpty_pullback_eraseEmpty and pullback_comp (the proof of seqOn_eq_of_isAnalyticOpenEmbedding verbatim, hg.1 read as ha).

theorem Hironaka.Manifold.BEDanFamStar.surjective_restrictMap_of_subset_image {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M P : AnalyticManifold 𝕜 (Fin n → 𝕜)} (a : AnalyticMap P M) (U' : TopologicalSpace.Opens P.carrier) (V : TopologicalSpace.Opens M.carrier) (hle : ⇑a '' ↑U' ⊆ ↑V) (hge : ↑V ⊆ ⇑a '' ↑U') : Function.Surjective ⇑(AnalyticMap.restrictMap a U' V hle)

The restriction of a to U' is ONTO V when V ⊆ a(U').

theorem Hironaka.Manifold.BEDanFamStar.seqOn_pullback_eq_of_pullback_eq {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M P : AnalyticManifold 𝕜 (Fin n → 𝕜)} (hbed : IsEmbeddedDesing 𝕜 bed) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (a b : AnalyticMap P M) (ha : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑a) (hb : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑b) (hab : T.pullback a ha = T.pullback b hb) (hTP : DomBEDan 𝕜 (T.pullback a ha)) (U' : TopologicalSpace.Opens P.carrier) (hU' : IsCompact (closure ↑U')) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (haV : ⇑a '' ↑U' ⊆ ↑V) (haV' : ↑V ⊆ ⇑a '' ↑U') (hbV : ⇑b '' ↑U' ⊆ ↑V) (hbV' : ↑V ⊆ ⇑b '' ↑U') : (bed.seqOn T hT V hV).pullback (AnalyticMap.restrictMap a U' V haV) ⋯ = (bed.seqOn T hT V hV).pullback (AnalyticMap.restrictMap b U' V hbV) ⋯

The fixed-run device ((37.1) in [Kol07, Proposition 37, proof]; the commutation with smooth surjections, [Kol07, 34.1]) — two SURJECTIVE local isomorphisms a b : P → M whose pulled-back triples COINCIDE and whose images of the reading open U' are the SAME relatively compact open V pull the run over V back to the SAME list — the family clause at a and at b has the same left side, and both erasures are no-ops.

theorem Manifold.IdealSheaf.ext_of_comap_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (J₁ J₂ : (sigmaManifold N).IdealSheaf) (h : ∀ (i : σ), pullback ⇑(sigmaMk N i) ⋯ J₁ = pullback ⇑(sigmaMk N i) ⋯ J₂) : J₁ = J₂

An ideal sheaf on a disjoint union is determined by its restrictions to the summands — stalkwise, the germ map along the summand inclusion is bijective (germMap_bijective_of_isLocalDiffeomorphAt).

theorem Manifold.HypersurfaceFamily.preimage_eq_of_comap_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (F : HypersurfaceFamily M.carrier) {u v : N.carrier → M.carrier} (h : comap u F = comap v F) (j : F.ι) : u ⁻¹' F.hyp j = v ⁻¹' F.hyp j

Equal inverse images of a hypersurface family along u and v have equal preimages of every member.

theorem Manifold.AnalyticTriple.pullback_sigmaDescMap_sumDesc_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (u v : AnalyticMap N M) (hu : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑u) (hv : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑v) (huv : T.pullback u hu = T.pullback v hv) : T.pullback (sigmaDescMap (Hironaka.Manifold.sumDesc u)) ⋯ = T.pullback (sigmaDescMap (Hironaka.Manifold.sumDesc v)) ⋯

The device's INPUT — two local isomorphisms u v : N → M with the same pulled-back triple give the same pulled-back triple along the two coproduct maps sigmaDescMap (sumDesc u), sigmaDescMap (sumDesc v) : M ⊔ N → M (id on the M summand).

theorem Hironaka.Manifold.domBEDan_pullback_sigmaDescMap_sumDesc {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (u : AnalyticMap N M) (hu : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑u) : DomBEDan 𝕜 (T.pullback (Manifold.sigmaDescMap (sumDesc u)) ⋯)

The pulled-back triple along the coproduct map is in DomBEDan when T is — the divisor stays empty and the ideal reduced (isReduced_pullback_of_isLocalDiffeomorph).

theorem AnalyticManifold.BlowUpSequence.pullback_eq_of_pullback_sigmaDescMap_sumDesc_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (u v : AnalyticMap N M) (hu : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑u) (hv : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑v) (h : L.pullback (Manifold.sigmaDescMap (Hironaka.Manifold.sumDesc u)) ⋯ = L.pullback (Manifold.sigmaDescMap (Hironaka.Manifold.sumDesc v)) ⋯) : L.pullback u hu = L.pullback v hv

A whole-list equality of pull-backs along the two coproduct maps, read on the N summand (sumInl; pullback_comp, sigmaDescMap_comp_sigmaMk), is the equality of the pull-backs along u and v.