The order clause along the pull-back by a local analytic isomorphism

The compatible-family form of Step 2.1 (Step21Fam.lean) restricts sequences of centres along the open inclusions M.restrict V → M.restrict W of a shrinking chain, local analytic isomorphisms that are not surjective. The transport of the clauses of [Kol07, Definition 66] along a pull-back proved in Functor/PullbackSequence.lean (isOfOrderGe_of_pullback) goes the other way and needs surjectivity, because the reduced boundary red(π⁻¹E ∪ π⁻¹Z) of the successions (IdealSheaf.reducedTransform; clause (iii) of [Hir64, Main Theorem II′(N)]) is defined by a global case split on the existence of local generators, which descends only along surjections. Forward, under the normal-crossings clause (3′) itself, no case split is needed: the boundary at every stage is the reduced ideal sheaf of a family with simple normal crossings (reducedTransform_eq_idealSheaf_totalTransform), such families pull back along local isomorphisms (isSnc_comap), their reduced ideal sheaves are the pull-backs (idealSheaf_comap_of_isSnc), and the total transform of a family pulls back along the lift (totalTransform_comap_liftStep). This is the local nature of the functoriality package noted in [Kol07, 104, Step 2.3] ("the functoriality package is local").

• BlowUpSequence.isOfOrderGe_pullback — a sequence of order ≥ m for (𝓘, m, red E) pulls back along any local analytic isomorphism h to a sequence of order ≥ m for (h^* 𝓘, m, red h⁻¹E); AnalyticTriple.isOfOrderGe_pullback is its form for triples;
• BlowUpSequence.isOfOrderGe_shrinkAppend — the shrink-and-append step of the chain (FamilyChain.lean) keeps the order clause for the restricted triple;
• AnalyticTriple.pullback_inclusion_restrictLE, pullback_eq_of_eq — restricting a restricted triple, and pull-backs along equal maps.

These are the order clauses carried by the chain of Step21Fam.lean and by Step 2.2 in the compatible-family form (Step22Fam.lean).

theorem Manifold.HypersurfaceFamily.idealSheaf_comap_of_isSnc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ₀ F) : (comap (⇑h) F).idealSheaf = IdealSheaf.pullback ⇑h ⋯ F.idealSheaf

The reduced ideal sheaf of h⁻¹(E) is the pull-back of the reduced ideal sheaf of E, for a family E with simple normal crossings and a local analytic isomorphism h (no surjectivity is needed): both sides fall under the first branch of the definition (the vanishing stalks of such a family have local generators, IsSnc.hasLocalGenerators_vanishingStalk_support), and the vanishing stalks correspond along the bijective germ maps. Not in the sources.

theorem AnalyticManifold.BlowUpSequence.isOfOrderGe_pullback {𝕜 : 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) (I : M.IdealSheaf) (m : ℕ) {F : Manifold.HypersurfaceFamily M.carrier} : Manifold.HypersurfaceFamily.IsSnc ψ₀ F → L.toSuccession.IsOfOrderGe I m F.idealSheaf → (L.pullback h hh).toSuccession.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑h ⋯ I) m (Manifold.HypersurfaceFamily.comap (⇑h) F).idealSheaf

The order clause pulls back along any local analytic isomorphism (the local nature of [Kol07, 34.1]): a sequence of order ≥ m for (𝓘, m, red E), E with simple normal crossings, pulls back to a sequence of order ≥ m for (h^* 𝓘, m, red h⁻¹E). By recursion on the sequence through isOfOrderGe_cons_iff: the normal-crossings clause and the order clause at the first centre transport along h (comap_of_isLocalDiffeomorph, ordAlongIdeal_comap_of_isLocalDiffeomorphAt); for the tail, the boundary after the first blow-up is the reduced ideal sheaf of the total transform of E, a family with simple normal crossings, on both sides (reducedTransform_eq_idealSheaf_totalTransform), the controlled transform pulls back along the lift (birationalTransform_comap_liftStep), and the total transform of h⁻¹E is the pull-back of the total transform of E (totalTransform_comap_liftStep).

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

The order clause pulls back, for triples: a sequence of order ≥ m starting with T pulls back along any local analytic isomorphism to a sequence of order ≥ m starting with the pulled-back triple.

theorem Manifold.AnalyticTriple.pullback_eq_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) {f g : AnalyticMap N M} (e : f = g) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) : T.pullback f hf = T.pullback g hg

Pulling back along equal maps gives equal triples.

theorem Manifold.AnalyticTriple.pullback_inclusion_restrictLE {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) {V W : TopologicalSpace.Opens M.carrier} (hVW : V ≤ W) : (T.pullback (M.inclusion W) ⋯).pullback (M.restrictLE hVW) ⋯ = T.pullback (M.inclusion V) ⋯

Restricting the restriction of a triple to W further to V ≤ W is its restriction to V (inclusion W ∘ restrictLE = inclusion V).

theorem AnalyticManifold.BlowUpSequence.inclusion_comp_liftCorestrict {𝕜 : 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) : ContMDiffMap.comp ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) (L.liftCorestrict h hh) = L.pullbackLiftLast h hh

The inclusion of the lifted range after the corestriction is the lift itself.

theorem AnalyticManifold.BlowUpSequence.isOfOrderGe_shrinkAppend {𝕜 : 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) (T : Manifold.AnalyticTriple ψ₀ M) (m : ℕ) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) (L' : BlowUpSequence ψ₀ ((L.stage (Fin.last L.length)).restrict (L.liftRange h hh))) (hL' : L'.toSuccession.IsOfOrderGe ((T.induced m L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).I m ((T.induced m L hL).pullback ((L.stage (Fin.last L.length)).inclusion (L.liftRange h hh)) ⋯).F.idealSheaf) : (L.shrinkAppend h hh L').toSuccession.IsOfOrderGe (T.pullback h hh).I m (T.pullback h hh).F.idealSheaf

The shrink-and-append step of the chain keeps the order clause: the sequence so far pulled back to the smaller open is of order ≥ m for the restricted triple (isOfOrderGe_pullback), and the appended value, of order ≥ m for the induced triple restricted to the reading open, pulls back along the corestricted lift to a sequence of order ≥ m for the induced triple of the restricted sequence (induced_pullback), so the concatenation is of order ≥ m (isOfOrderGe_concat).