Step 2.1 along a local analytic isomorphism: the induced triple and the member index

The functoriality of Step 2.1 of the proof of [Kol07, Theorem 103] is that of Lemma 102 ("functoriality in Step 2.1 by the corresponding functoriality in (102)", [Kol07, 104, Step 2.3]). Along a surjective local analytic isomorphism h the nonempty members of h⁻¹(E) and their order are those of E (nonemptyList_comap_of_surjective), and each step of the iteration pulls back: the triple induced by the pull-back is the pull-back of the induced triple along the lift of h to the last stage (induced_pullback, from the transport lemmas of ConcatPullback.lean), and the member index corresponds (originalIdx_last_pullback_heq, the transform of the same original member).

• FiniteSuccession.heq_toLex_inl, heq_originalIdx_congr, heq_originalIdxAux_cons_succ, BlowUpSequence.originalIdx_last_pullback_heq — the member index of the pulled-back family at the last stage is the member index of the family (a heterogeneous equality, the two index sets being propositionally equal).
• AnalyticTriple.induced_pullback, HypersurfaceFamily.nonemptyList_comap_of_surjective.

Step 2.1 in the compatible-family form uses them (Step21Fam.lean, InducedValue.lean).

theorem AnalyticManifold.FiniteSuccession.heq_toLex_inl {α β : Type u} (e : α = β) {x : α} {y : β} (hxy : x ≍ y) : toLex (Sum.inl x) ≍ toLex (Sum.inl y)

toLex ∘ Sum.inl respects heterogeneous equality across equal summand types.

theorem AnalyticManifold.BlowUpSequence.originalIdx_last_pullback_heq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (G : Manifold.HypersurfaceFamily M.carrier) (j : G.ι) : (L.pullback h hh).toSuccession.originalIdx (Manifold.HypersurfaceFamily.comap (⇑h) G) (Fin.last (L.pullback h hh).toSuccession.length) j ≍ L.toSuccession.originalIdx G (Fin.last L.toSuccession.length) j

The index of the transform of a member in the pulled-back family at the last stage of h^* L is its index in the family at the last stage of L; the two index sets are propositionally equal (totalTransformSeqFrom_last_pullbackLiftLast), so the statement is a heterogeneous equality.

theorem Manifold.AnalyticTriple.induced_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (s : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hL' : (L.pullback h hh).toSuccession.IsOfOrderGe (T.pullback h hh).I s (T.pullback h hh).F.idealSheaf) : (T.induced s L hL).pullback (L.pullbackLiftLast h hh) ⋯ = (T.pullback h hh).induced s (L.pullback h hh) hL'

The triple induced by the pull-back of a sequence is the pull-back of the induced triple along the lift of h to the last stage: the controlled transform and the boundary family at the last stage both pull back (ConcatPullback.lean). This is the step-by-step form of the functoriality argument in [Kol07, 104, Step 2.3].

theorem Manifold.HypersurfaceFamily.nonemptyList_comap_of_surjective {M N : Type u} (F : HypersurfaceFamily M) (h : N → M) (hs : Function.Surjective h) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) (hF' : Finite { j : (comap h F).ι // (comap h F).hyp j ≠ ∅ }) : (comap h F).nonemptyList hF' = F.nonemptyList hF

Along a surjective map the nonempty members of the inverse-image family, in the order of the index set, are those of the family.