The fixed-run device with synchronised members

Kollár's descent of the centres from the disjoint union of a cover: the centre of the disjoint union agrees on the overlaps, (37.2) in [Kol07, Proposition 37, proof], because the functor commutes with smooth surjections [Kol07, 34.1]. Two local analytic isomorphisms u v : N → M with the SAME pulled-back triple (T.pullback u = T.pullback v — the shear's ideal identity hI in the application) pull the functor's run over a reading open V ⊆ M back to the SAME list over any relatively compact open W' ⊆ N whose two images lie in V: this is seqOn_pullback_eq_of_pullback_eq (ExceptionalFamilyGlue.lean) on the coproduct P := N ⊔ M with the maps id ⊔ u, id ⊔ v (surjective, so both erasures are no-ops) at the reading open U' := W' ⊔ V of P, READ ON THE N-SUMMAND (the restricted summand inclusion N|W' → P|U', pullback_comp). With the synchronisation of RunFamilyRestrict.lean it follows that, when u, v are moreover open embeddings of one admissible input T', the two open immersions localResolutionHomOn of local resolutions pull every member of the run's boundary family back to the SAME closed subspace — the stage-σ member on one side IS the stage-σ member on the other, no label chosen (the label is a stage of the one run).

The user is the transition between a padded piece and a piece of the other embedding in the common datum sumPadData D₁ D₂ (CoproductSumData.lean, CoproductMixedTransition.lean): u := sigmaMk (inl i) ∘ …, v := sigmaMk (inr j) ∘ … ∘ g with the shear g of exists_padded_equivalence_hom_point. hbed is the only hypothesis. Not in the sources beyond Kollár's descent; bookkeeping.

def Hironaka.Manifold.sumOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (W' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) : TopologicalSpace.Opens (Manifold.sigmaManifold (sumFamily N M)).carrier

The reading open W' ⊔ V of the coproduct N ⊔ M — the union of the two summand images.

Equations

• Hironaka.Manifold.sumOpens W' V = { carrier := ⇑Hironaka.Manifold.sumInl '' ↑W' ∪ ⇑(Manifold.sigmaMk (Hironaka.Manifold.sumFamily N M) { down := false }) '' ↑V, is_open' := ⋯ }

theorem Hironaka.Manifold.image_sumInl_subset_sumOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (W' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) : ⇑sumInl '' ↑W' ⊆ ↑(sumOpens W' V)

The first summand's image lies in the coproduct's reading open sumOpens.

theorem Hironaka.Manifold.isCompact_closure_sumOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (W' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) (hW' : IsCompact (closure ↑W')) (hV : IsCompact (closure ↑V)) : IsCompact (closure ↑(sumOpens W' V))

Relatively compact summands give a relatively compact reading open of the coproduct.

theorem Hironaka.Manifold.image_sigmaDescMap_sumDesc_sumOpens_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (W' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) (w : AnalyticMap N M) (hwV : ⇑w '' ↑W' ⊆ ↑V) : ⇑(Manifold.sigmaDescMap (sumDesc w)) '' ↑(sumOpens W' V) ⊆ ↑V

id ⊔ w maps W' ⊔ V into V when w(W') ⊆ V.

theorem Hironaka.Manifold.subset_image_sigmaDescMap_sumDesc_sumOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (W' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) (w : AnalyticMap N M) : ↑V ⊆ ⇑(Manifold.sigmaDescMap (sumDesc w)) '' ↑(sumOpens W' V)

id ⊔ w maps W' ⊔ V ONTO V (the M-summand).

theorem Hironaka.Manifold.BEDanFamStar.seqOn_pullback_restrictMap_eq_of_pullback_eq {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (hbed : IsEmbeddedDesing 𝕜 bed) (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) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (huV : ⇑u '' ↑W' ⊆ ↑V) (hvV : ⇑v '' ↑W' ⊆ ↑V) : (bed.seqOn T hT V hV).pullback (AnalyticMap.restrictMap u W' V huV) ⋯ = (bed.seqOn T hT V hV).pullback (AnalyticMap.restrictMap v W' V hvV) ⋯

The fixed-run device read on a summand ((37.1)–(37.2) in [Kol07, Proposition 37, proof]; [Kol07, 34.1]) — two local analytic isomorphisms u v : N → M with the SAME pulled-back triple pull the run over V back to the SAME list over any relatively compact W' ⊆ N with u(W') ⊆ V, v(W') ⊆ V: seqOn_pullback_eq_of_pullback_eq on N ⊔ M with the surjective maps id ⊔ u, id ⊔ v at the reading open W' ⊔ V, then the restricted summand inclusion N|W' → (N ⊔ M)|W' ⊔ V (pullback_comp).

theorem Hironaka.Manifold.BEDanFamStar.comap_localResolutionHomOn_runMembers_eq_of_isPullbackOf {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (hbed : IsEmbeddedDesing 𝕜 bed) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (u v : AnalyticMap N M) (hu : Manifold.IsAnalyticOpenEmbedding u) (hv : Manifold.IsAnalyticOpenEmbedding v) (hpu : T'.IsPullbackOf T u) (hpv : T'.IsPullbackOf T v) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (huV : ⇑u '' ↑W' ⊆ ↑V) (hvV : ⇑v '' ↑W' ⊆ ↑V) (σ : (bed.runFamily T hT V hV).ι) : AnalyticSpace.QuotientSpace.comap (↑(bed.localResolutionHomOn T hT V hV T' hT' u hu hpu W' hW' huV hbed)) (bed.runMembers T hT V hV hbed σ) = AnalyticSpace.QuotientSpace.comap (↑(bed.localResolutionHomOn T hT V hV T' hT' v hv hpv W' hW' hvV hbed)) (bed.runMembers T hT V hV hbed σ)

The fixed-run device with synchronised members ((37.2) in [Kol07, Proposition 37, proof]) — two open embeddings u, v of ONE admissible input (T', W') into (T, V) pull every member of the run on T back along the two open immersions of local resolutions to the SAME closed subspace: the two pulled-back triples coincide (ext'), hence the two pulled-back runs (the device above), hence the members (comap_localResolutionHomOn_runMembers_eq_of_pullback_eq, RunFamilyRestrict.lean).