Step 2.1 on an open: independence of the chain, compatibility, functoriality

Three clauses of Step 2.1 of the proof of [Kol07, Theorem 103] in the compatible-family form (Step21Fam.lean), all from the two-chain lemma step21FamAux_filter_rel of ChainIndep.lean:

• step21FamOn_chain_indep — the value of Step 2.1 on U does not depend on the admissible chain of opens along which it is computed: the fixed chain of step21FamOn and any other, over the same member list, agree on U up to empty blow-ups;
• step21FamOn_compat — the compatibility under restriction of [Wlo09, Theorem 2.0.3 (4)]: for U ≤ V, the value on U is the value on V restricted to U with the empty blow-ups deleted (the independence of the chain for the chain of V, read on U);
• step21FamOn_commutesWithLocalIsos — the commutation with local analytic isomorphisms in the form of AnalyticFamilyFunctor.CommutesWithLocalIsos (the functoriality of Step 2.1 noted in [Kol07, 104, Step 2.3]): along a local analytic isomorphism g : N → M, the chain over N for the pulled-back triple over the member list filtered of the members emptied by g is, up to empty blow-ups, the chain over the full member list along a chain of opens carried into the chain of g(U') (step21FamAux_filter_rel; a member emptied by g contributes nothing, given that the family's value at an empty member is the trivial family, the hypothesis hnil), which is the pull-back of the chain over M link by link (step21FamAux_rel_along, link_rel).

The three clauses enter the compatible family of Step 2.1 and its functor in Step22Fam.lean.

theorem Hironaka.Manifold.nonemptyList_reverse_filter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) : List.filter (fun (j : T.F.ι) => decide (T.F.hyp j ≠ ∅)) (T.F.nonemptyList ⋯).reverse = (T.F.nonemptyList ⋯).reverse

The list of nonempty members has no empty member: filtering keeps it.

theorem Hironaka.Manifold.nonemptyList_reverse_hnil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (bd : BDanFamData ψ₀ s) (j : T.F.ι) : j ∈ (T.F.nonemptyList ⋯).reverse → T.F.hyp j = ∅ → ∀ {M' : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M') (hT' : Manifold.AnalyticTriple.BOClass s T') (j' : T'.F.ι), T'.F.hyp j' = ∅ → bd.fam T' hT' j' = CompatibleFamily.nil T'

The members of the list of nonempty members are nonempty, so the hypothesis on empty members of the two-chain lemma is never needed for it.

theorem Hironaka.Manifold.step21FamOn_chain_indep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (W : ℕ → TopologicalSpace.Opens M.carrier) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (hWsub : ∀ k < memberCount T s hT, closure ↑(W (k + 1)) ⊆ ↑(W k)) (hUW : U ≤ W (memberCount T s hT)) : ((step21FamAux T s bd hT W (memberCount T s hT) hW hWsub (T.F.nonemptyList ⋯).reverse ⋯).L.pullback (M.restrictLE hUW) ⋯).eraseEmpty = step21FamOn T s bd hT U hU

Step 2.1 on U does not depend on the chain of opens: the two-chain lemma (step21FamAux_filter_rel) for the given chain and the fixed one, over the list of nonempty members, read on U.

theorem Hironaka.Manifold.step21FamOn_compat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : step21FamOn T s bd hT U hU = ((step21FamOn T s bd hT V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

Compatibility of Step 2.1 under restriction ([Wlo09, Theorem 2.0.3 (4)]): for U ≤ V the value on U is the value on V restricted to U with the empty blow-ups deleted; the independence of the chain (step21FamOn_chain_indep) for the chain of V, read on U.

theorem Hironaka.Manifold.step21FamAux_rel_along {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (bd : BDanFamData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BOClass s (T.pullback g hg)) (W : ℕ → TopologicalSpace.Opens M.carrier) (r : ℕ) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k)) (W' : ℕ → TopologicalSpace.Opens N.carrier) (hW' : ∀ (k : ℕ), IsCompact (closure ↑(W' k))) (hWsub' : ∀ k < r, closure ↑(W' (k + 1)) ⊆ ↑(W' k)) (hWW' : ∀ (k : ℕ), ⇑g '' ↑(W' k) ⊆ ↑(W k)) (l : List T.F.ι) (hl : l.length ≤ r) : (step21FamAux (T.pullback g hg) s bd hT' W' r hW' hWsub' l hl).L.eraseEmpty = ((step21FamAux T s bd hT W r hW hWsub l hl).L.pullback (AnalyticMap.restrictMap g (W' l.length) (W l.length) ⋯) ⋯).eraseEmpty

Along g, the chain over N for the pulled-back triple is, up to empty blow-ups, the pull-back of the chain over M, link by link (link_rel), for chains of opens with g(W'_k) ⊆ W_k processing the same members (the functoriality of Step 2.1, [Kol07, 104, Step 2.3]).

theorem Hironaka.Manifold.step21FamOn_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (hnil : ∀ {M' : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M') (hT' : Manifold.AnalyticTriple.BOClass s T') (j : T'.F.ι), T'.F.hyp j = ∅ → bd.fam T' hT' j = CompatibleFamily.nil T') {N : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BOClass s (T.pullback g hg)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : step21FamOn (T.pullback g hg) s bd hT' U' hU' = ((step21FamOn T s bd hT (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

Step 2.1 commutes with local analytic isomorphisms on the opens (the functoriality of [Kol07, 104, Step 2.3] in the form of AnalyticFamilyFunctor.CommutesWithLocalIsos): the chain over N for the filtered member list is the chain over the full list along opens carried into the chain of g(U') (step21FamAux_filter_rel), which is the pull-back of that chain (step21FamAux_rel_along); restricting to U' and deleting the empty blow-ups gives the statement.