Functoriality of localResolutionHomOn along a composite

The sequence functor commutes with open embeddings, whose pull-back lifts them stage by stage ([Kol07, Definition 30.1]; [Kol07, 34.1]); the lift is unique in the library's sense — a continuous map over the embedding that pulls dense opens back to dense sets is the lift (eq_of_stageMap_last_comp_eq, OrderReduction/LiftUnique.lean; not in the sources). Applied to a COMPOSITE g ∘ k of two open embeddings of admissible inputs this gives the functoriality of the lift and the open immersion of LocalResolutionOn.lean:

• BEDanFamStar.liftOn_comp: liftOn (g ∘ k) = liftOn g ∘ liftOn k on the last stages — both are continuous lifts of g ∘ k pulling dense opens back to dense sets (isLocalDiffeomorph_liftOn), and they agree after the last blow-down (stageMap_last_liftOn' three times);
• BEDanFamStar.localResolutionHomOn_comp: localResolutionHomOn g ∘ localResolutionHomOn k = localResolutionHomOn (g ∘ k) (≫) — homOfPullbackEq_comp_of_comp_eq (ShearOverX.lean) at liftOn_comp;
• the congruences liftOn_congr, localResolutionHomOn_congr in the embedding (the first has no user and is stated for the symmetry with the second);
• the INSTANCES LocalEmbeddingData.resIn_sumPadData_inl / _inr: for the common padded datum S = sumPadData D₁ D₂, S.resIn (inl i) = sumInlResIn ∘ D₁⁺.resIn i (and inr) — the composites sumPadInlAmbient ∘ sigmaMk i = sigmaMk (inl i) and sumInrAmbient ∘ sigmaMk j = sigmaMk (inr j) (sumPadInlAmbient_comp_sigmaMk, sumInrAmbient_comp_sigmaMk). Both instances are equations of morphisms of analytic spaces (≫) with the piece spelled once, as the sum's; the identities to use are comap_resIn_sumPadData_inl / _inr, where the two spellings of the piece meet as ideal sheaves.

These identities let the members of the common run pulled back along S.resIn (inl i) be read through sumInlResIn and then through the padded piece's resIn i, which the comparison of two adjacent levels (CoproductLevelPair.lean) and the compatibility of the piece traces (CoproductGluedFamilyCompat.lean) need. Not in the sources beyond the pull-back of blow-up sequences; bookkeeping.

theorem Hironaka.Manifold.BEDanFamStar.liftOn_congr {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) (g' : AnalyticMap N M) (hg' : Manifold.IsAnalyticOpenEmbedding g') (hpb' : T'.IsPullbackOf T g') (hle' : ⇑g' '' ↑W' ⊆ ↑W) (hgg' : g = g') : bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed = bed.liftOn T hT W hW T' hT' g' hg' hpb' W' hW' hle' hbed

The lift depends on the embedding only through its value — congruence in g (the proofs are irrelevant).

theorem Hironaka.Manifold.BEDanFamStar.localResolutionHomOn_congr {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) (g' : AnalyticMap N M) (hg' : Manifold.IsAnalyticOpenEmbedding g') (hpb' : T'.IsPullbackOf T g') (hle' : ⇑g' '' ↑W' ⊆ ↑W) (hgg' : g = g') : bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed = bed.localResolutionHomOn T hT W hW T' hT' g' hg' hpb' W' hW' hle' hbed

The open immersion depends on the embedding only through its value — congruence in g.

theorem Hironaka.Manifold.BEDanFamStar.liftOn_comp {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) {P : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T'' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) P) (hT'' : DomBEDan 𝕜 T'') (k : AnalyticMap P N) (hk : Manifold.IsAnalyticOpenEmbedding k) (hpbk : T''.IsPullbackOf T' k) (W'' : TopologicalSpace.Opens P.carrier) (hW'' : IsCompact (closure ↑W'')) (hlek : ⇑k '' ↑W'' ⊆ ↑W') (hgk : Manifold.IsAnalyticOpenEmbedding (ContMDiffMap.comp g k)) (hpbgk : T''.IsPullbackOf T (ContMDiffMap.comp g k)) (hlegk : ⇑(ContMDiffMap.comp g k) '' ↑W'' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : ⇑(bed.liftOn T hT W hW T'' hT'' (ContMDiffMap.comp g k) hgk hpbgk W'' hW'' hlegk hbed) = ⇑(bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) ∘ ⇑(bed.liftOn T' hT' W' hW' T'' hT'' k hk hpbk W'' hW'' hlek hbed)

The lift of a composite of open embeddings is the composite of the lifts ([Kol07, Definition 30.1]) — both are continuous maps of the last stages over g ∘ k that pull dense opens back to dense sets (local analytic isomorphisms, isLocalDiffeomorph_liftOn), and they agree after the last blow-down (stageMap_last_liftOn'), so the uniqueness of the lift (eq_of_stageMap_last_comp_eq) identifies them.

theorem Hironaka.Manifold.BEDanFamStar.localResolutionHomOn_comp {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) {P : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T'' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) P) (hT'' : DomBEDan 𝕜 T'') (k : AnalyticMap P N) (hk : Manifold.IsAnalyticOpenEmbedding k) (hpbk : T''.IsPullbackOf T' k) (W'' : TopologicalSpace.Opens P.carrier) (hW'' : IsCompact (closure ↑W'')) (hlek : ⇑k '' ↑W'' ⊆ ↑W') (hgk : Manifold.IsAnalyticOpenEmbedding (ContMDiffMap.comp g k)) (hpbgk : T''.IsPullbackOf T (ContMDiffMap.comp g k)) (hlegk : ⇑(ContMDiffMap.comp g k) '' ↑W'' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : CategoryTheory.CategoryStruct.comp (bed.localResolutionHomOn T' hT' W' hW' T'' hT'' k hk hpbk W'' hW'' hlek hbed) (bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) = bed.localResolutionHomOn T hT W hW T'' hT'' (ContMDiffMap.comp g k) hgk hpbgk W'' hW'' hlegk hbed

Functoriality of the open immersion of local resolutions along a composite of open embeddings ([Kol07, Definition 30.1]) — localResolutionHomOn at g ∘ k is the composite of the two; homOfPullbackEq_comp_of_comp_eq at liftOn_comp.

theorem Hironaka.Manifold.LocalEmbeddingData.resIn_sumPadData_inl {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (bed : BEDanFamStar 𝕜) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D₁.ι) : (D₁.sumPadData D₂).resIn bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ hbed (Sum.inl i) = CategoryTheory.CategoryStruct.comp (bed.localResolutionHomOn (D₁.padLeftData D₂.n).sigmaTriple ⋯ ((D₁.padLeftData D₂.n).ambImage W₁) ⋯ ((D₁.sumPadData D₂).embedding (Sum.inl i)).ambientTriple ⋯ (Manifold.sigmaMk (fun (i : (D₁.padLeftData D₂.n).ι) => pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G) i) ⋯ ⋯ (D₁.sumPadOpens D₂ W₁ W₂ (Sum.inl i)) ⋯ ⋯ hbed) (D₁.sumInlResIn D₂ W₁ W₂ bed hW₁ hW₂ hbed)

The common datum's open immersion at an inl piece factors through the first padded level's ([Kol07, Definition 30.1]; [Kol07, 34.1]) — S.resIn (inl i) = sumInlResIn ∘ (D₁⁺.resIn i read at the sum's piece), the functoriality localResolutionHomOn_comp along sigmaMk (inl i) = sumPadInlAmbient ∘ sigmaMk i (sumPadInlAmbient_comp_sigmaMk, the datum's specific inl inclusion). The second factor is D₁⁺.resIn i with the piece spelled as the sum's ((sumPadData D₁ D₂).embedding (Sum.inl i), sumPadOpens … (Sum.inl i)): the statement keeps ONE spelling of the piece, and the identity to use is comap_resIn_sumPadData_inl, where the two spellings meet as ideal sheaves.

theorem Hironaka.Manifold.LocalEmbeddingData.resIn_sumPadData_inr {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (bed : BEDanFamStar 𝕜) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (j : D₂.ι) : (D₁.sumPadData D₂).resIn bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ hbed (Sum.inr j) = CategoryTheory.CategoryStruct.comp (bed.localResolutionHomOn (D₂.padRightData D₁.n).sigmaTriple ⋯ ((D₂.padRightData D₁.n).ambImage W₂) ⋯ ((D₁.sumPadData D₂).embedding (Sum.inr j)).ambientTriple ⋯ (Manifold.sigmaMk (fun (j : (D₂.padRightData D₁.n).ι) => pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G) j) ⋯ ⋯ (D₁.sumPadOpens D₂ W₁ W₂ (Sum.inr j)) ⋯ ⋯ hbed) (D₁.sumInrResIn D₂ W₁ W₂ bed hW₁ hW₂ hbed)

The common datum's open immersion at an inr piece factors through the second padded level's — S.resIn (inr j) = sumInrResIn ∘ (D₂⁺.resIn j read at the sum's piece) (sumInrAmbient_comp_sigmaMk); the spelling as for inl.

theorem Hironaka.Manifold.LocalEmbeddingData.comap_resIn_sumPadData_inl {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (bed : BEDanFamStar 𝕜) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D₁.ι) (M : Manifold.IdealSheaf (bed.localResolutionOn (D₁.sumPadData D₂).sigmaTriple ⋯ ((D₁.sumPadData D₂).ambImage (D₁.sumPadOpens D₂ W₁ W₂)) ⋯).𝒪) : AnalyticSpace.QuotientSpace.comap (↑((D₁.sumPadData D₂).resIn bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ hbed (Sum.inl i))) M = AnalyticSpace.QuotientSpace.comap (↑((D₁.padLeftData D₂.n).resIn bed W₁ hW₁ hbed i)) (AnalyticSpace.QuotientSpace.comap (↑(D₁.sumInlResIn D₂ W₁ W₂ bed hW₁ hW₂ hbed)) M)

The pull-back form at inl — pulling a closed subspace of the common run's local resolution back along S.resIn (inl i) is pulling it back along sumInlResIn and then along D₁⁺.resIn i (resIn_sumPadData_inl, QuotientSpace.comap_comp; the two spellings of the piece meet here, as ideal sheaves, where they are definitionally equal at once).

theorem Hironaka.Manifold.LocalEmbeddingData.comap_resIn_sumPadData_inr {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (bed : BEDanFamStar 𝕜) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (j : D₂.ι) (M : Manifold.IdealSheaf (bed.localResolutionOn (D₁.sumPadData D₂).sigmaTriple ⋯ ((D₁.sumPadData D₂).ambImage (D₁.sumPadOpens D₂ W₁ W₂)) ⋯).𝒪) : AnalyticSpace.QuotientSpace.comap (↑((D₁.sumPadData D₂).resIn bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ hbed (Sum.inr j))) M = AnalyticSpace.QuotientSpace.comap (↑((D₂.padRightData D₁.n).resIn bed W₂ hW₂ hbed j)) (AnalyticSpace.QuotientSpace.comap (↑(D₁.sumInrResIn D₂ W₁ W₂ bed hW₁ hW₂ hbed)) M)

The pull-back form at inr — pulling back along S.resIn (inr j) is pulling back along sumInrResIn and then along D₂⁺.resIn j.