The two stop clauses as predicates on a succession, and their transports

The structure BMOmodFam (Functor/ModifiedMarkedFam.lean) has two fields about the stop predicate IsSmoothTransversalIdealAt: output_isSmoothSubmanifoldIdeal, at every point of the support of the last marked transform of (𝓘, 1) that transform is the ideal of a smooth submanifold transversal to the total boundary, and stopped_never_blownUp, a point of a stage on no member of the boundary at which the predicate holds is never blown up later. They are the two properties of the modified algorithm of [Wlo09, Theorem 7.4.1]: the form of its output (coordinates transversal to the exceptional divisors) and the stop rule of its modified first step. The value of the modified functor on an open U is built from local runs by pull-back along local analytic isomorphisms, deletion of the empty blow-ups, concatenation along the induced triple and descent along the maximal-contact cover (ComposeInduced.lean, StepBGlobal.lean, GlobalizeFam.lean), so the two properties have to be carried across each of these operations. This module isolates them as predicates on a finite succession from a pair (𝓘, F) (OutputClause, StoppedClause: the two fields word for word, with S := L.toSuccession and (𝓘, F) the restricted triple's) and on a family functor per open (OutputClauseFam, StoppedClauseFam), and proves the transports used by the modules Clause*.lean that follow. Throughout, "the output clause" is OutputClause and "the stopped clause" is StoppedClause.

• Pull-back along a local analytic isomorphism h ([Kol07, Definition 30, 30.1]). BlowUpSequence.totalTransformSeqFrom_pullback (the boundary at every stage of h^* L is the pull-back along the lift h_i; totalTransform_comap_liftStep at each step) and BlowUpSequence.stageMapAdd_pullbackLift (the composite blow-downs intertwine with the lifts); both clauses pull back (outputClause_pullback, stoppedClause_pullback, by IsSmoothTransversalIdealAt.comap) and descend along a surjective h (outputClause_of_pullback_of_surjective, stoppedClause_of_pullback_of_surjective): a point lifts along the surjective lift and the predicate comes back along a local inverse (IsSmoothTransversalIdealAt.of_comap, the converse of comap: the chart with simple normal crossings is transported by transportChart, the stalk read through the bijective germ map).
• Deletion of the empty blow-ups ([Kol07, 32]; the second condition of [Kol07, 34.1]). The output clause by the last-stage identifications markedTransformSeq_last_eraseEmpty and boundaryCorr_eraseEmpty (outputClause_eraseEmpty); the stopped clause by induction on the list (stoppedClause_eraseEmpty), a cons being read as the clause at stage 0 together with the tail's clause from the head triple (stoppedClause_cons_iff, stoppedClause_cons_of_forall_notMem); an empty first step is deleted and the rest carried along the diffeomorphism of the empty blow-up (map_eq_pullback_symm), the boundary reached being T.F with one empty member (StoppedClause.of_isEmptyExtension).
• Concatenation along the induced triple (Induced.lean): outputClause_cons_iff, outputClause_concat, stoppedClause_concat, by induction on the first list with induced_cons and induced_nil; a centre of the second list over a predicate point off the boundary lies over a predicate point of the join off the boundary (IsSmoothTransversalIdealAt.stageMapAdd_of_forall_notMem_center: the predicate persists along a fibre no centre meets, the analogue for the predicate of notMem_totalTransformSeqFrom_of_forall_notMem_center), which is excluded at stage 0 (StoppedClause.notMem_center_of_stageMap_eq, stageMapAdd_zero_left).
• Descent along the maximal-contact cover ([Kol07, Theorem 103, Step 3]): outputClauseFam_of_agreeFam, stoppedClauseFam_of_agreeFam, the analogues of isOfOrderGe_of_agreeFam.
• Two lemmas on the predicate and the members of the boundary, IsSmoothTransversalIdealAt.emptyMember and IsSmoothTransversalIdealAt.of_emptyMember_of_notMem: a chart with simple normal crossings at a point constrains only the members through the point, so the predicate ignores a member not through it; they let the descent and lift of StopRestrict.lean be applied with the boundary minus the maximal-contact member.

The mathematics is [Kol07, Definition 30, 30.1], [Kol07, 32], [Kol07, 34.1], the descent of [Kol07, Theorem 103, Step 3] and the persistence lemmas of StopPersistence.lean; the statements themselves are not in the sources.

def AnalyticManifold.FiniteSuccession.OutputClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (I : M.IdealSheaf) (F : Manifold.HypersurfaceFamily M.carrier) : Prop

The output clause for a succession S from the pair (𝓘, F) (the field output_isSmoothSubmanifoldIdeal of BMOmodFam, read on L.toSuccession from the restricted triple): at every point of the support {ord ≥ 1} of the marked transform of (𝓘, 1) at the last stage, that transform is locally the ideal of a smooth submanifold with coordinates transversal to the total boundary.

Equations

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

def AnalyticManifold.FiniteSuccession.StoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (I : M.IdealSheaf) (F : Manifold.HypersurfaceFamily M.carrier) : Prop

The stopped clause for a succession S from (𝓘, F) (the field stopped_never_blownUp of BMOmodFam): a point x of a stage i on no member of the boundary at which the marked transform is a smooth submanifold ideal transversal to the boundary is never blown up: no later centre contains a point over x.

Equations

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

theorem AnalyticManifold.FiniteSuccession.stageMapAdd_zero_left {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (k : ℕ) (hk : 0 + k < S.length + 1) (y : (S.stage ⟨0 + k, hk⟩).carrier) : (S.stageMapAdd 0 k hk) y = (S.stageMap ⟨0 + k, hk⟩) y

The composite blow-down from stage 0 over k steps is the succession's stageMap at stage 0 + k (the bridge between stageMapAdd and stageMapAux, two recursions peeling the last blow-up).

theorem AnalyticManifold.FiniteSuccession.StoppedClause.notMem_center_of_stageMap_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I : M.IdealSheaf} {F : Manifold.HypersurfaceFamily M.carrier} (hS : StoppedClause ψ₀ S I F) (m : ℕ) (hm : m < S.length) {x : (S.stage ⟨0, ⋯⟩).carrier} (hP : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ₀ F I x) (hx : ∀ (j : F.ι), x ∉ F.hyp j) (y : (S.stage ⟨m, ⋯⟩).carrier) (hy : (S.stageMap ⟨m, ⋯⟩) y = x) : y ∉ Manifold.IdealSheaf.support (S.center ⟨m, hm⟩)

The stopped clause read at stage 0 with stageMap: no centre of the succession lies over a predicate point of the start off the boundary (the stage number generalised to 0 + k, stageMapAdd_zero_left).

theorem AnalyticManifold.FiniteSuccession.StoppedClause.of_isEmptyExtension {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I : M.IdealSheaf} {G G' : Manifold.HypersurfaceFamily M.carrier} {e₀ : G.ι ↪o G'.ι} (he : Manifold.HypersurfaceFamily.IsEmptyExtension e₀) (h : StoppedClause ψ₀ S I G') : StoppedClause ψ₀ S I G

The stopped clause descends along an empty extension G ↪ G' of the boundary family (IsEmptyExtension: the members of G are members of G' and the other members of G' are empty): stage by stage the boundaries stay in empty extension (isEmptyExtension_totalTransform), and the predicate and "on no member" transport along one, since an empty member is through no point (IsSmoothTransversalIdealAt.congr_nhds).

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

The output clause of a family functor on its class, per open: the value on U from the restricted triple satisfies OutputClause. For Dom := BMOClass 1 at the model refl 𝕜 (Fin n → 𝕜) this is the field output_isSmoothSubmanifoldIdeal of BMOmodFam with functor := B, definitionally.

Equations

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

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

The stopped clause of a family functor on its class, per open (the field stopped_never_blownUp of BMOmodFam with functor := B, definitionally).

Equations

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

Pull-back along a local analytic isomorphism

theorem AnalyticManifold.BlowUpSequence.totalTransformSeqFrom_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) (F : Manifold.HypersurfaceFamily M.carrier) (i : Fin (L.length + 1)) : (L.pullback h hh).toSuccession.totalTransformSeqFrom (Manifold.HypersurfaceFamily.comap (⇑h) F) ⟨↑i, ⋯⟩ = Manifold.HypersurfaceFamily.comap (⇑(L.pullbackLift h hh i)) (L.toSuccession.totalTransformSeqFrom F i)

The boundary families along h^* L at every stage (the all-stage form of totalTransformSeqFrom_last_pullbackLiftLast): the boundary from F.comap h at stage i of h^* L is the boundary from F at stage i of L pulled back along the lift h_i.

theorem AnalyticManifold.BlowUpSequence.stageMapAdd_pullbackLift {𝕜 : 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 k : ℕ) (hik : i + k < L.length + 1) (hik' : i + k < (L.pullback h hh).length + 1) (y : ((L.pullback h hh).toSuccession.stage ⟨i + k, hik'⟩).carrier) : (L.pullbackLift h hh ⟨i, ⋯⟩) (((L.pullback h hh).toSuccession.stageMapAdd i k hik') y) = (L.toSuccession.stageMapAdd i k hik) ((L.pullbackLift h hh ⟨i + k, hik⟩) y)

The composite blow-downs of h^* L between two stages are intertwined with those of L by the lifts (stageMapAdd along pullbackLift).

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.of_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M N : AnalyticManifold 𝕜 E} (F : HypersurfaceFamily M.carrier) (J : M.IdealSheaf) (g : AnalyticMap N M) {y : N.carrier} (hg : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑g) y) (h : IsSmoothTransversalIdealAt ψ₀ (HypersurfaceFamily.comap (⇑g) F) (IdealSheaf.pullback ⇑g ⋯ J) y) : IsSmoothTransversalIdealAt ψ₀ F J (g y)

The predicate descends along a local analytic isomorphism (the converse of IsSmoothTransversalIdealAt.comap): the predicate for the pulled-back family and ideal at y gives the predicate for F and J at g y. The chart with simple normal crossings at y is transported along a local inverse Φ⁻¹ of g (transportChart, the mirror of the proof of comap; stalkIdeal_comap_eq_map_germMap, germMap_coord_eq_coord_transportChart). Used at the lifted point in outputClause_of_pullback_of_surjective and stoppedClause_of_pullback_of_surjective.

theorem AnalyticManifold.BlowUpSequence.outputClause_of_pullback_of_surjective {𝕜 : 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) (hs : Function.Surjective ⇑h) (T : Manifold.AnalyticTriple ψ₀ M) (hge : L.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hP : FiniteSuccession.OutputClause ψ₀ (L.pullback h hh).toSuccession (T.pullback h hh).I (T.pullback h hh).F) : FiniteSuccession.OutputClause ψ₀ L.toSuccession T.I T.F

The output clause descends along a surjective local analytic isomorphism: if h^* L from the pulled-back triple satisfies the clause, so does L from T. A point of the last stage of L lifts along the surjective last lift (markedTransformSeq_pullback, totalTransformSeqFrom_pullback), and the predicate comes back along the local isomorphism (IsSmoothTransversalIdealAt.of_comap).

theorem AnalyticManifold.BlowUpSequence.outputClause_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) (T : Manifold.AnalyticTriple ψ₀ M) (hge : L.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hP : FiniteSuccession.OutputClause ψ₀ L.toSuccession T.I T.F) : FiniteSuccession.OutputClause ψ₀ (L.pullback h hh).toSuccession (T.pullback h hh).I (T.pullback h hh).F

The output clause pulls back along a local analytic isomorphism (IsSmoothTransversalIdealAt.comap).

theorem AnalyticManifold.BlowUpSequence.stoppedClause_of_pullback_of_surjective {𝕜 : 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) (hs : Function.Surjective ⇑h) (T : Manifold.AnalyticTriple ψ₀ M) (hge : L.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hP : FiniteSuccession.StoppedClause ψ₀ (L.pullback h hh).toSuccession (T.pullback h hh).I (T.pullback h hh).F) : FiniteSuccession.StoppedClause ψ₀ L.toSuccession T.I T.F

The stopped clause descends along a surjective local analytic isomorphism (center_pullback, totalTransformSeqFrom_pullback, stageMapAdd_pullbackLift, and the predicate brought back by IsSmoothTransversalIdealAt.of_comap).

theorem AnalyticManifold.BlowUpSequence.stoppedClause_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) (T : Manifold.AnalyticTriple ψ₀ M) (hge : L.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hP : FiniteSuccession.StoppedClause ψ₀ L.toSuccession T.I T.F) : FiniteSuccession.StoppedClause ψ₀ (L.pullback h hh).toSuccession (T.pullback h hh).I (T.pullback h hh).F

The stopped clause pulls back along a local analytic isomorphism.

Deletion of the empty blow-ups ([Kol07, 32], [Kol07, 34.1])

theorem AnalyticManifold.BlowUpSequence.outputClause_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (T : Manifold.AnalyticTriple ψ₀ M) (hge : L.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hP : FiniteSuccession.OutputClause ψ₀ L.toSuccession T.I T.F) : FiniteSuccession.OutputClause ψ₀ L.eraseEmpty.toSuccession T.I T.F

The output clause survives the deletion of the empty blow-ups (markedTransformSeq_last_eraseEmpty and boundaryCorr_eraseEmpty at the last stage, the predicate transported along eraseEmptyLast).

theorem AnalyticManifold.BlowUpSequence.stoppedClause_cons_of_forall_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (L' : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (T : Manifold.AnalyticTriple ψ₀ M) (hh : (cons hY (nil (Manifold.blowUp ψ₀ hY))).toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hR : FiniteSuccession.StoppedClause ψ₀ L'.toSuccession (T.headTriple 1 hY hh).I (T.headTriple 1 hY hh).F) (hxY : ∀ (x : M.carrier), Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ₀ T.F T.I x → (∀ (j : T.F.ι), x ∉ T.F.hyp j) → x ∉ Y) : FiniteSuccession.StoppedClause ψ₀ (cons hY L').toSuccession T.I T.F

The stopped clause for cons hY L' from the stopped clause of L' for the head triple and the stage-0 content (a predicate point off the boundary is not in Y): a centre of L' over such a point lies over a predicate point of the head stage off its boundary (the predicate and the absence from the boundary persist under one blow-up off the centre, the marking legitimate by the head's order clause), which is excluded at stage 0 by StoppedClause.notMem_center_of_stageMap_eq; the later stages are L''s, one stage in.

theorem AnalyticManifold.BlowUpSequence.stoppedClause_cons_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (T : Manifold.AnalyticTriple ψ₀ M) (hge : (cons hY rest).toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) : FiniteSuccession.StoppedClause ψ₀ (cons hY rest).toSuccession T.I T.F ↔ (∀ (k : ℕ) (h : k < rest.length + 1) (x : M.carrier), Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ₀ T.F T.I x → (∀ (j : T.F.ι), x ∉ T.F.hyp j) → ∀ (y : ((cons hY rest).toSuccession.stage ⟨k, ⋯⟩).carrier), ((cons hY rest).toSuccession.stageMap ⟨k, ⋯⟩) y = x → y ∉ Manifold.IdealSheaf.support ((cons hY rest).toSuccession.center ⟨k, h⟩)) ∧ FiniteSuccession.StoppedClause ψ₀ rest.toSuccession (T.headTriple 1 hY ⋯).I (T.headTriple 1 hY ⋯).F

The stopped clause is read one stage in: for cons hY rest it is the clause at stage 0 (no later centre over a predicate point of M off the boundary) together with the clause of rest from the head triple (the marked transform of (𝓘, 1) and the total transform of F under the first blow-up, AnalyticTriple.headTriple).

theorem AnalyticManifold.BlowUpSequence.stoppedClause_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (T : Manifold.AnalyticTriple ψ₀ M) (hge : L.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hP : FiniteSuccession.StoppedClause ψ₀ L.toSuccession T.I T.F) : FiniteSuccession.StoppedClause ψ₀ L.eraseEmpty.toSuccession T.I T.F

The stopped clause survives the deletion of the empty blow-ups, by induction on the list with stoppedClause_cons_iff: a nonempty first centre stays (eraseEmpty_cons_of_ne_empty) and stoppedClause_cons_of_forall_notMem rebuilds the clause from the tail's; an empty one is deleted and the rest carried along the diffeomorphism of the empty blow-up (eraseEmpty_cons_of_eq_empty with map_eq_pullback_symm and stoppedClause_pullback), the head triple's data being T.I pulled back twice and T.F with one empty member, so that the clause comes back along StoppedClause.of_isEmptyExtension.

Concatenation along the induced triple

theorem AnalyticManifold.BlowUpSequence.outputClause_cons_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (T : Manifold.AnalyticTriple ψ₀ M) (hge : (cons hY rest).toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) : FiniteSuccession.OutputClause ψ₀ (cons hY rest).toSuccession T.I T.F ↔ FiniteSuccession.OutputClause ψ₀ rest.toSuccession (T.headTriple 1 hY ⋯).I (T.headTriple 1 hY ⋯).F

The output clause is read one stage in: for cons hY rest it is the clause of rest from the head triple (the last stage and its transforms are rest's from the head triple, cons_markedTransformSeq_last, cons_totalTransformSeqFrom_last).

theorem AnalyticManifold.BlowUpSequence.outputClause_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (L₁ : BlowUpSequence ψ₀ M) (L₂ : BlowUpSequence ψ₀ (L₁.stage (Fin.last L₁.length))) (T : Manifold.AnalyticTriple ψ₀ M) (hge₁ : L₁.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hP₂ : FiniteSuccession.OutputClause ψ₀ L₂.toSuccession (T.induced 1 L₁ hge₁).I (T.induced 1 L₁ hge₁).F) : FiniteSuccession.OutputClause ψ₀ (L₁.concat L₂).toSuccession T.I T.F

The output clause of a concatenation is the output clause of the appended list from the induced triple, by induction on the first list with induced_cons and induced_nil (the recursion of boClass_induced_concat_aux); at a cons the two rewrites of outputClause_cons_iff, cons_markedTransformSeq_last and cons_totalTransformSeqFrom_last, with the head clause of hge₁. outputClause_cons_iff itself asks for the order clause of the whole cons list, which a concatenation does not carry, so it is not applied directly.

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.stageMapAdd_of_forall_notMem_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I : M.IdealSheaf} {F : HypersurfaceFamily M.carrier} (hge : S.IsOfOrderGe I 1 F.idealSheaf) (hF : IsSnc ψ₀ F) (i k : ℕ) (h : i + k < S.length + 1) {x : (S.stage ⟨i, ⋯⟩).carrier} (hx : ∀ (j : (S.totalTransformSeqFrom F ⟨i, ⋯⟩).ι), x ∉ (S.totalTransformSeqFrom F ⟨i, ⋯⟩).hyp j) (hP : IsSmoothTransversalIdealAt ψ₀ (S.totalTransformSeqFrom F ⟨i, ⋯⟩) (S.markedTransformSeq I 1 ⟨i, ⋯⟩) x) (hcen : ∀ (l : ℕ) (hl : l < k) (z : (S.stage ⟨i + l, ⋯⟩).carrier), (S.stageMapAdd i l ⋯) z = x → z ∉ IdealSheaf.support (S.center ⟨i + l, ⋯⟩)) (y : (S.stage ⟨i + k, h⟩).carrier) (hy : (S.stageMapAdd i k h) y = x) : IsSmoothTransversalIdealAt ψ₀ (S.totalTransformSeqFrom F ⟨i + k, h⟩) (S.markedTransformSeq I 1 ⟨i + k, h⟩) y

The predicate persists along a fibre no centre meets (the analogue for the predicate of notMem_totalTransformSeqFrom_of_forall_notMem_center): a point x of stage i off the boundary at which the marked transform is a smooth submanifold ideal transversal to the boundary, none of whose images at the stages i, …, i + k − 1 lies in the centre blown up there, keeps the predicate at every point y over it at stage i + k. At each step the blow-up is a local isomorphism off the centre and the marking is legitimate by the order clause (IsSmoothTransversalIdealAt.totalTransform_of_notMem).

theorem AnalyticManifold.BlowUpSequence.stoppedClause_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (L₁ : BlowUpSequence ψ₀ M) (L₂ : BlowUpSequence ψ₀ (L₁.stage (Fin.last L₁.length))) (T : Manifold.AnalyticTriple ψ₀ M) (hge₁ : L₁.toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) (hP₁ : FiniteSuccession.StoppedClause ψ₀ L₁.toSuccession T.I T.F) (hP₂ : FiniteSuccession.StoppedClause ψ₀ L₂.toSuccession (T.induced 1 L₁ hge₁).I (T.induced 1 L₁ hge₁).F) : FiniteSuccession.StoppedClause ψ₀ (L₁.concat L₂).toSuccession T.I T.F

The stopped clause of a concatenation from the stopped clauses of the two lists, by induction on the first list with induced_cons and induced_nil: at a cons, stoppedClause_cons_iff reads the first list's clause as its stage-0 content plus the tail's clause for the head triple, the induction gives the tail's concatenation, and stoppedClause_cons_of_forall_notMem rebuilds the clause of the cons.

Descent along the maximal-contact cover ([Kol07, Theorem 103, Step 3])

theorem Hironaka.Manifold.AnalyticFamilyFunctor.outputClauseFam_of_agreeFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.LocalMCClass 1) (B' : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BOClass 1) (hagree : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass 1 T), B'.fam T ⋯ = B.fam T hL) (hB' : B'.CommutesWithLocalIsos) (hord : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass 1 T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)), ((B.fam T hL).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (N.inclusion U) ⋯).I 1 (T.pullback (N.inclusion U) ⋯).F.idealSheaf) (hB : OutputClauseFam ψ₀ B) : OutputClauseFam ψ₀ B'

The output clause descends per open (the analogue of isOfOrderGe_of_agreeFam): a functor B' on BOClass 1 agreeing with B on the local maximal-contact class and commuting with local isomorphisms inherits the output clause of B. On the finite shrunk maximal-contact cover k of closure U, the pull-back k^*(B'(T)|_U) is B at the pulled-back triple and satisfies the clause, which descends along the surjective k (outputClause_of_pullback_of_surjective).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.stoppedClauseFam_of_agreeFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.LocalMCClass 1) (B' : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BOClass 1) (hagree : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass 1 T), B'.fam T ⋯ = B.fam T hL) (hB' : B'.CommutesWithLocalIsos) (hord : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass 1 T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)), ((B.fam T hL).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (N.inclusion U) ⋯).I 1 (T.pullback (N.inclusion U) ⋯).F.idealSheaf) (hB : StoppedClauseFam ψ₀ B) : StoppedClauseFam ψ₀ B'

The stopped clause descends per open (the same descent with stoppedClause_of_pullback_of_surjective).

Two member lemmas on the predicate

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.emptyMember {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} {J : M.IdealSheaf} {x : M.carrier} (h : IsSmoothTransversalIdealAt ψ₀ F J x) (j : F.ι) : IsSmoothTransversalIdealAt ψ₀ (F.emptyMember j) J x

Emptying a member keeps the predicate (the chart with simple normal crossings, the member's coordinate forgotten; HypersurfaceFamily.emptyMember).

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.of_emptyMember_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} {J : M.IdealSheaf} {x : M.carrier} (j : F.ι) (hx : x ∉ F.hyp j) (h : IsSmoothTransversalIdealAt ψ₀ (F.emptyMember j) J x) : IsSmoothTransversalIdealAt ψ₀ F J x

A member not through x may be restored: the predicate for F.emptyMember j at a point x ∉ F.hyp j gives the predicate for F. A chart with simple normal crossings at x constrains only the members through x, and at x ∉ F.hyp j the two index subtypes {k // x ∈ (F.emptyMember j).hyp k} and {k // x ∈ F.hyp k} have the same predicate (the members of F.emptyMember j are if k = j then ∅ else F.hyp k, emptyMember_hyp_of_ne, emptyMember_hyp_self), so the same chart with cidx transported is such a chart for F at x. No closedness and no shrinking of the chart is needed.