The composite of two family functors along induced triples: the link

The modified marked resolution of [Wlo09, Theorem 7.4.1] runs its phases in succession on every relatively compact open: the rounds on the nonmonomial part, the monomial phase, and the modified first step; each is a family functor with the two naturality properties, and each is applied to the triple induced by the value of the previous phase at its last stage (the triple (X_j, I_j, E_j) carried along a composite sequence in [Kol07, 104, Step 2.1]). This module is the generic link of such a composite, for two arbitrary family functors F : AnalyticFamilyFunctor ψ₀ Dom₁ and G : AnalyticFamilyFunctor ψ₀ Dom₂ whose classes are related by a transport hypothesis (hFG: the induced triple of a value of F lies in Dom₂). It is the link of the second step of the order reduction (ChainTransport.lean: linkValue, link_rel) with the family of one boundary member replaced by the functor G, whose transport lemmas are those of InducedValueFunctor.lean:

• alongList F G s hF hFG T hT W hW V hV hVW : CenterList ψ₀ (M.restrict V): the value of F on the outer open W, restricted to V ⊆ W (closure V ⊆ W), followed by the value of G at the induced triple, read on the lifted range of V (shrinkAppend); alongList_isOfOrderGe is the order clause at the mark s, from those of F and G (isOfOrderGe_shrinkAppend);
• alongList_rel, the relation of the link along a local analytic isomorphism h : N → M with h(W') ⊆ W, h(V') ⊆ V: the composite over (W', V') for the pulled-back triple, with empty blow-ups deleted, is the composite over (W, V) pulled back along h|_{V'} and cleaned (the second condition of [Kol07, 34.1], on each open). The list algebra is shrinkAppend_eraseEmpty_pullback; the two appended values are compared by inducedValue_rel (the two naturality properties of G at the induced triples); the values of F are related by its own commutation and compatibility (seqOn_pullback_eq_of_image_subset);
• ClassInducedEraseEmptyClosed s Dom, the property of the class of G which the relation needs beyond its closure under pull-back: the induced triple of the cleaned list lies in the class when the induced triple of the list does [Kol07, 32]; BMOClass m and BOClass m have it (bmoClass_induced_eraseEmpty, boClass_induced_eraseEmpty: the order read through eraseEmptyLast⁻¹, the nonempty members embedded by eraseEmptyIdx).

The functor itself, its compatibility (the relation at the identity along a common refinement of two canonical chains), commutation and indifference are in ComposeInducedFunctor.lean.

The class of the induced triple at the cleaned list

theorem Manifold.AnalyticTriple.ord_induced_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (s : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hLe : L.eraseEmpty.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (y : (L.eraseEmpty.stage (Fin.last L.eraseEmpty.length)).carrier) : IdealSheaf.ord (T.induced s L.eraseEmpty hLe).I y = IdealSheaf.ord (T.induced s L hL).I (L.eraseEmptyLast.symm y)

The order of the marked transform at the last stage of the cleaned list is its order at the last stage of the list, read through eraseEmptyLast⁻¹ (markedTransformSeq_last_eraseEmpty; the order of an inverse-image ideal sheaf at a point where the map is a local isomorphism) [Kol07, 34.1].

theorem Manifold.AnalyticTriple.finite_nonempty_induced_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (s : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hLe : L.eraseEmpty.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hfin : Finite { j : (T.induced s L hL).F.ι // (T.induced s L hL).F.hyp j ≠ ∅ }) : Finite { j : (T.induced s L.eraseEmpty hLe).F.ι // (T.induced s L.eraseEmpty hLe).F.hyp j ≠ ∅ }

Finitely many nonempty boundary members survive the deletion of empty blow-ups [Kol07, 32]: the nonempty members of the boundary of the cleaned list embed into those of the list through eraseEmptyIdx (hyp_eraseEmptyIdx: the member eraseEmptyIdx i, pulled back to the last stage of the cleaned list, is the member i).

theorem Manifold.AnalyticTriple.bmoClass_induced_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (s : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hLe : L.eraseEmpty.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {m : ℕ} (hT : BMOClass m (T.induced s L hL)) : BMOClass m (T.induced s L.eraseEmpty hLe)

The class of BMO_{n,m} (BMOClass m) at an induced triple is kept by the cleaning of the inducing list: the mark is the same, the nonempty members finite by finite_nonempty_induced_eraseEmpty.

theorem Manifold.AnalyticTriple.boClass_induced_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (s : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hLe : L.eraseEmpty.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {m : ℕ} (hT : BOClass m (T.induced s L hL)) : BOClass m (T.induced s L.eraseEmpty hLe)

The class of BO_{n,m} (BOClass m) at an induced triple is kept by the cleaning of the inducing list: the order bound through ord_induced_eraseEmpty, the finiteness through finite_nonempty_induced_eraseEmpty.

def Hironaka.Manifold.AnalyticFamilyFunctor.ClassInducedEraseEmptyClosed {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (s : ℕ) (Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop) : Prop

A class of triples closed under the deletion of empty blow-ups from the inducing list at the mark s: the induced triple of the cleaned list lies in the class when the induced triple of the list does ([Kol07, 32]). It supplies the class proof hDe₂ of inducedValue_rel in the relation of the link of the composite; BMOClass m and BOClass m have it (bmoClass_induced_eraseEmpty, boClass_induced_eraseEmpty).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.bmoClass_classPullbackClosed {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BMOClass m

BMOClass m is closed under pull-back along local analytic isomorphisms: the mark is kept, the nonempty members of the inverse image family are among the nonempty members.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.boClass_classPullbackClosed {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] (m : ℕ) : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BOClass m

BOClass m is closed under pull-back along local analytic isomorphisms (boClass_of_isPullbackOf at the pulled-back triple).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.bmoClass_classInducedEraseEmptyClosed {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (s m : ℕ) : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BMOClass m

BMOClass m is closed under the cleaning of the inducing list at every mark.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.boClass_classInducedEraseEmptyClosed {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (s m : ℕ) : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BOClass m

BOClass m is closed under the cleaning of the inducing list at every mark.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.AnalyticFamilyFunctor.firstTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (W : TopologicalSpace.Opens M.carrier) : Manifold.AnalyticTriple ψ₀ (M.restrict W)

The restricted triple over the outer open W.

Equations

• Hironaka.Manifold.AnalyticFamilyFunctor.firstTriple T W = T.pullback (M.inclusion W) ⋯

@[reducible, inline]

abbrev Hironaka.Manifold.AnalyticFamilyFunctor.firstList {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict W)

The value of F on the outer open W (the first factor of the link).

Equations

• F.firstList T hT W hW = (F.fam T hT).seqOn W hW

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.AnalyticFamilyFunctor.inducedOfFirst {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) : Manifold.AnalyticTriple ψ₀ ((F.firstList T hT W hW).stage (Fin.last (F.firstList T hT W hW).length))

The triple induced by the value of F at its last stage.

Equations

• F.inducedOfFirst s hF T hT W hW = (Hironaka.Manifold.AnalyticFamilyFunctor.firstTriple T W).induced s (F.firstList T hT W hW) ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.AnalyticFamilyFunctor.firstReadOpen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (V : TopologicalSpace.Opens M.carrier) (hVW : closure ↑V ⊆ ↑W) : TopologicalSpace.Opens ((F.firstList T hT W hW).stage (Fin.last (F.firstList T hT W hW).length)).carrier

The reading open of the link: the lifted range of V ⊆ W at the last stage of the value of F.

Equations

• F.firstReadOpen T hT W hW V hVW = (F.firstList T hT W hW).liftRange (M.restrictLE ⋯) ⋯

theorem Hironaka.Manifold.AnalyticFamilyFunctor.isCompact_closure_firstReadOpen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : IsCompact (closure ↑(F.firstReadOpen T hT W hW V hVW))

noncomputable def Hironaka.Manifold.AnalyticFamilyFunctor.appendValue {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : AnalyticManifold.BlowUpSequence ψ₀ (((F.firstList T hT W hW).stage (Fin.last (F.firstList T hT W hW).length)).restrict (F.firstReadOpen T hT W hW V hVW))

The appended value of the link: G at the triple induced by the value of F, read on the lifted range of V ⊆ W.

Equations

• F.appendValue G s hF hFG T hT W hW V hV hVW = (G.fam (F.inducedOfFirst s ⋯ T hT W hW) ⋯).seqOn (F.firstReadOpen T hT W hW V hVW) ⋯

noncomputable def Hironaka.Manifold.AnalyticFamilyFunctor.alongList {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict V)

The composite over (W, V): the value of F on W restricted to V, followed by the value of G at the induced triple on the lifted range (shrinkAppend).

Equations

• F.alongList G s hF hFG T hT W hW V hV hVW = (F.firstList T hT W hW).shrinkAppend (M.restrictLE ⋯) ⋯ (F.appendValue G s ⋯ ⋯ T hT W hW V hV hVW)

theorem Hironaka.Manifold.AnalyticFamilyFunctor.alongList_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (hG : ∀ {N : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ N) (hT' : Dom₂ T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((G.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I s (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) : (F.alongList G s ⋯ ⋯ T hT W hW V hV hVW).toSuccession.IsOfOrderGe (T.pullback (M.inclusion V) ⋯).I s (T.pullback (M.inclusion V) ⋯).F.idealSheaf

The order clause of the composite at the mark s, from those of F (hF) and G (hG): isOfOrderGe_shrinkAppend, the restricted triple rewritten by pullback_inclusion_restrictLE.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.firstList_pullback_rel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (hFc : F.CommutesWithLocalIsos) {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hT' : Dom₁ (T.pullback h hh)) {W : TopologicalSpace.Opens M.carrier} (hW : IsCompact (closure ↑W)) {W' : TopologicalSpace.Opens N.carrier} (hW' : IsCompact (closure ↑W')) (hWW' : ⇑h '' ↑W' ⊆ ↑W) : (F.firstList (T.pullback h hh) hT' W' hW').eraseEmpty = ((F.firstList T hT W hW).pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).eraseEmpty

The value of F on W' ⊆ N for the pulled-back triple, cleaned, is the value of F on W ⊇ h(W') pulled back along h|_{W'} and cleaned (the commutation and compatibility of F, seqOn_pullback_eq_of_image_subset; the deletion of empty blow-ups is idempotent).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.alongList_rel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) (hFc : F.CommutesWithLocalIsos) (hG : G.CommutesWithLocalIsos) (hG' : G.IndifferentToEmptyMembers) (hDom : ClassPullbackClosed fun {M : AnalyticManifold 𝕜 E} => Dom₂) (hDomE : ClassInducedEraseEmptyClosed s fun {M : AnalyticManifold 𝕜 E} => Dom₂) {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (T' : Manifold.AnalyticTriple ψ₀ N) (hT'g : T'.IsPullbackOf T h) (hT'' : Dom₁ T') {W : TopologicalSpace.Opens M.carrier} (hW : IsCompact (closure ↑W)) {W' : TopologicalSpace.Opens N.carrier} (hW' : IsCompact (closure ↑W')) (hWW' : ⇑h '' ↑W' ⊆ ↑W) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) {V' : TopologicalSpace.Opens N.carrier} (hV' : IsCompact (closure ↑V')) (hV'W' : closure ↑V' ⊆ ↑W') (hVV' : ⇑h '' ↑V' ⊆ ↑V) : (F.alongList G s ⋯ ⋯ T' hT'' W' hW' V' hV' hV'W').eraseEmpty = ((F.alongList G s ⋯ ⋯ T hT W hW V hV hVW).pullback (AnalyticMap.restrictMap h V' V hVV') ⋯).eraseEmpty

The second condition of [Kol07, 34.1] for one link of the composite: the composite over (W', V') for the pulled-back triple, cleaned, is the composite over (W, V) pulled back along h|_{V'} and cleaned, for h(W') ⊆ W, h(V') ⊆ V. This is link_rel with the family of one boundary member replaced by G: the list algebra shrinkAppend_eraseEmpty_pullback, the two appended values compared by inducedValue_rel (the naturality of G at the induced triples), the values of F related by firstList_pullback_rel.