The separation step of the marked order reduction: the invariant and the separating ideal

The second step of Kollár's proof of the marked order reduction theorem [Kol07, Theorem 107] separates the cosupport of (I, m) from the cosupport of the nonmonomial part N(I) [Kol07, 111, Step 2]. With s the maximal order of N(I) along cosupp(I, m) = {x | ord_x I ≥ m}, one applies the order reduction BO_{n, ms} [Kol07, Theorem 68] to the single ideal N(I)^m + I^s, by the observation

ord_Z J₁ ≥ s and ord_Z J₂ ≥ m ⇔ ord_Z (J₁^m + J₂^s) ≥ ms,

so that every smooth blow-up sequence of order ms for N(I)^m + I^s is one of order s for N(I) and one of order m for I; then s has dropped and one continues with s − 1, until s = 0, i.e. cosupp(I, m) ∩ cosupp N(I) = ∅.

On an analytic manifold the rounds of this descent are links of a chain over shrinking relatively compact opens (ChainState), and Kollár's s is carried as an invariant of the state rather than read as a supremum: SepOrdLe S m s says ord N(𝓘) ≤ s at every point of cosupp(𝓘, m). The descent starts at the bound s = t − 1 with which the first step exits (NonmonomialOrdLe) and runs through s = t − 1, …, 1; a round at a bound above the actual separation order is empty up to the deletion of empty blow-ups [Kol07, 32]. This module provides:

• the observation along a smooth centre (IdealSheaf.le_ordAlongIdeal_pow_add_pow_iff), from the characterisation of the order along a centre by the pointwise orders at the nearby points of the centre (IdealSheaf.le_ordAlongIdeal_iff_eventually_le_ord) and the pointwise form IdealSheaf.le_ord_pow_add_pow_iff; and the additivity of pull-back, IdealSheaf.pullback_add;
• the transform identity modulo N, NonmonomialTransformIdentityMod: the predicate, which the assembly takes as a parameter and which nonmonomialTransformIdentityMod_inhabitant proves;
• the separation invariant SepOrdLe, the two exit facts at s = 0, the separating ideal and triple sepIdealAt and sepTripleAt at an explicit s, the order bound ord_sepIdealAt_le, and the class SepClass m s of triples whose separating triple lies in the domain of BO_{n, ms};
• the order reduction read at the separating triple, sepFunctor, a family functor on SepClass m s which commutes with local analytic isomorphisms and is indifferent to empty boundary members, so that the transport lemmas for values at induced triples apply to the links of the separation step.

The scheme-theoretic counterparts are Hironaka.BMO.sepTriple and AlgebraicGeometry.Scheme.IdealSheafData.leOrdAlong_pow_sup_pow_iff.

The observation of the separation step along a smooth centre

theorem Manifold.IdealSheaf.le_ordAlongIdeal_iff_eventually_le_ord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) {a : M} (ha : a ∈ Y) (p : ℕ) : ↑p ≤ hY.idealSheaf.ordAlongIdeal I a ↔ ∀ᶠ (y : ↑Y) in nhds ⟨a, ha⟩, ↑p ≤ I.ord ↑y

The order of I along a smooth centre Y at a point a ∈ Y is ≥ p iff the pointwise order of I is ≥ p at all points of Y near a. Forwards: the order along Y is locally constant on Y (isLocallyConstant_ordAlong) and bounds the pointwise order from below (ordAlong_le_ord); backwards: stalkIdeal_le_pow_of_eventually_le_ord.

theorem Manifold.IdealSheaf.le_ordAlongIdeal_pow_add_pow_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y : Set M} {c : ℕ} [FiniteDimensional 𝕜 E] (hY : IsClosedSubmanifold ψ Y c) (J₁ J₂ : IdealSheaf (structureSheaf 𝕜 E M)) {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) {a : M} (ha : a ∈ Y) : ↑(m * s) ≤ hY.idealSheaf.ordAlongIdeal (J₁ ^ m + J₂ ^ s) a ↔ ↑s ≤ hY.idealSheaf.ordAlongIdeal J₁ a ∧ ↑m ≤ hY.idealSheaf.ordAlongIdeal J₂ a

The observation of [Kol07, 111, Step 2] along a smooth centre: for m, s ≥ 1 and a ∈ Y, ms ≤ ord_{Y,a} (J₁^m + J₂^s) iff s ≤ ord_{Y,a} J₁ and m ≤ ord_{Y,a} J₂. It is the pointwise statement IdealSheaf.le_ord_pow_add_pow_iff at the points of Y near a, through the characterisation le_ordAlongIdeal_iff_eventually_le_ord.

theorem Manifold.IdealSheaf.pullback_add {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (I J : IdealSheaf (structureSheaf 𝕜 E M)) : pullback φ hφ (I + J) = pullback φ hφ I + pullback φ hφ J

The pull-back of a sum of ideal sheaves is the sum of the pull-backs (stalkwise Ideal.map_sup).

The transform identity modulo N, as a predicate

def Hironaka.Manifold.BMO.NonmonomialTransformIdentityMod {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) : Prop

The transform identity modulo N along a list of centres: for a list of order ≥ m for (𝓘, m) and of order ≥ s for (N(𝓘), s), with m ≥ 1, no bound on the order of N(𝓘) and no relation between m and s, the nonmonomial part of the marked transform of (𝓘, m) is the nonmonomial part of the marked transform of (N(𝓘), s) at every stage, with respect to the transformed boundary. This is the observation at the end of [Kol07, 111, Step 1] (the two birational transforms differ by a product of powers of the exceptional divisors, hence only in their monomial part) read modulo the monomial part. The descent of the separation step uses it at s < m, where the identity at the exact order (NonmonomialTransformIdentity, which needs m ≤ d) does not apply. The assembly takes the predicate as a parameter; nonmonomialTransformIdentityMod_inhabitant proves it.

Equations

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

The separation invariant and the separating triple at an explicit s

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

The separation invariant: ord N(𝓘) ≤ s at every point where ord 𝓘 ≥ m. It carries Kollár's s, "the maximum order of N(I) along cosupp(I, m)" [Kol07, 111, Step 2], as an upper bound rather than as a supremum. SepOrdLe S m 0 is the disjointness cosupp(𝓘, m) ∩ cosupp N(𝓘) = ∅ (sepOrdLe_zero_iff).

Equations

• Hironaka.Manifold.BMO.SepOrdLe S m s = ∀ (x : ↑↧M.carrier), ↑m ≤ Manifold.IdealSheaf.ord S.I x → Manifold.IdealSheaf.ord (Hironaka.Manifold.BMO.nonmonomialTriple S).I x ≤ ↑s

theorem Hironaka.Manifold.BMO.SepOrdLe.weaken {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Manifold.AnalyticTriple ψ₀ M} {m s s' : ℕ} (h : SepOrdLe S m s) (hss : s ≤ s') : SepOrdLe S m s'

theorem Hironaka.Manifold.BMO.sepOrdLe_zero_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (m : ℕ) : SepOrdLe S m 0 ↔ ∀ (x : ↑↧M.carrier), ↑m ≤ Manifold.IdealSheaf.ord S.I x → x ∉ Manifold.IdealSheaf.support (nonmonomialTriple S).I

The separation bound 0 is the disjointness of the cosupports: no point of cosupp(𝓘, m) lies in cosupp N(𝓘) [Kol07, 111, Step 2].

theorem Hironaka.Manifold.BMO.SepOrdLe.ord_lt_of_mem_cosupport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Manifold.AnalyticTriple ψ₀ M} {m : ℕ} (h : SepOrdLe S m 0) {x : M.carrier} (hx : x ∈ Manifold.IdealSheaf.support (nonmonomialTriple S).I) : Manifold.IdealSheaf.ord S.I x < ↑m

At the exit of the separation step, ord 𝓘 < m at every point of cosupp N(𝓘); hence the centre of any further blow-up, which lies in cosupp(𝓘, m), misses cosupp N(𝓘) [Kol07, 111, Step 2].

theorem Hironaka.Manifold.BMO.stalkIdeal_eq_monomialPart_of_notMem_cosupport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) {x : M.carrier} (hx : x ∉ Manifold.IdealSheaf.support (nonmonomialTriple S).I) : Manifold.IdealSheaf.stalkIdeal S.I x = (monomialPart S.F ⋯ S.I).stalkIdeal x

Off cosupp N(𝓘) the stalk of 𝓘 is the stalk of its monomial part: 𝓘 = M(𝓘) · N(𝓘) (monomialPart_mul_nonmonomialPart) and N(𝓘)_x = 𝒪_x there. This is the pointwise form of "replace X by X ∖ cosupp N(I) and thus assume that I = M(I)" [Kol07, 111, Step 2].

noncomputable def Hironaka.Manifold.BMO.sepIdealAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (m s : ℕ) : M.IdealSheaf

The separating ideal N(𝓘)^m + 𝓘^s of [Kol07, 111, Step 2] at an explicit s; the sum is the sum of ideal sheaves, stalkwise the join.

Equations

• Hironaka.Manifold.BMO.sepIdealAt S m s = (Hironaka.Manifold.BMO.nonmonomialTriple S).I ^ m + S.I ^ s

@[simp]

theorem Hironaka.Manifold.BMO.stalkIdeal_sepIdealAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (m s : ℕ) (x : M.carrier) : Manifold.IdealSheaf.stalkIdeal (sepIdealAt S m s) x = Manifold.IdealSheaf.stalkIdeal (nonmonomialTriple S).I x ^ m ⊔ Manifold.IdealSheaf.stalkIdeal S.I x ^ s

theorem Hironaka.Manifold.BMO.isNonzeroEverywhere_sepIdealAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (m s : ℕ) : Manifold.IdealSheaf.IsNonzeroEverywhere (sepIdealAt S m s)

The separating ideal is nonzero at every point: its summand N(𝓘)^m is nonzero in the stalk, which is a domain (for m = 0 the summand is the unit ideal).

noncomputable def Hironaka.Manifold.BMO.sepTripleAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (m s : ℕ) : Manifold.AnalyticTriple ψ₀ M

The separating triple (M, N(𝓘)^m + 𝓘^s, E) of [Kol07, 111, Step 2] at an explicit s: the manifold and the boundary of S, with the separating ideal.

Equations

• Hironaka.Manifold.BMO.sepTripleAt S m s = { I := Hironaka.Manifold.BMO.sepIdealAt S m s, isNonzeroEverywhere := ⋯, F := S.F, isSnc := ⋯ }

@[simp]

theorem Hironaka.Manifold.BMO.sepTripleAt_I {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (m s : ℕ) : (sepTripleAt S m s).I = sepIdealAt S m s

@[simp]

theorem Hironaka.Manifold.BMO.sepTripleAt_F {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ M) (m s : ℕ) : (sepTripleAt S m s).F = S.F

theorem Hironaka.Manifold.BMO.ord_sepIdealAt_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Manifold.AnalyticTriple ψ₀ M} {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) (hsep : SepOrdLe S m s) (x : M.carrier) : Manifold.IdealSheaf.ord (sepIdealAt S m s) x ≤ ↑(m * s)

Under the separation invariant at s ≥ 1 (and m ≥ 1) the separating ideal has order at most ms at every point, so that the separating triple lies in the domain of BO_{n, ms} (Kollár's "which has order ≥ ms" [Kol07, 111, Step 2] is the lower bound at the centres; this is the upper bound the order reduction theorem needs). The order of a sum is the minimum of the orders and the order of a power is the multiple (the cosupport identities of [Kol07, Definition 59 (3), (4)], read on orders); on cosupp(𝓘, m) the bound comes from ord N(𝓘) ≤ s, off it from ord 𝓘 < m.

theorem Hironaka.Manifold.BMO.sepTripleAt_eq_of_isEmptyExtension {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (m s : ℕ) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') {e : F'.ι ↪o T.F.ι} (he : Manifold.HypersurfaceFamily.IsEmptyExtension e) : sepTripleAt { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } m s = { I := (sepTripleAt T m s).I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }

The separating triple of a triple whose boundary is replaced by an empty extension is the separating triple with the boundary replaced: the nonmonomial part ignores empty members (nonmonomialTriple_eq_of_isEmptyExtension). This is the input of the indifference property of the round.

theorem Hironaka.Manifold.BMOmod.NonmonomialOrdLe.sepOrdLe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Manifold.AnalyticTriple ψ₀ M} {d : ℕ} (h : NonmonomialOrdLe S d) (m : ℕ) : BMO.SepOrdLe S m d

The exit bound of the first step, ord N(𝓘) ≤ d everywhere, gives the separation invariant at d: the separation step starts at the bound the first step exits with (stepAChainState_bound), with no new supremum.

@[reducible, inline]

abbrev Hironaka.Manifold.BMO.SepClass {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m s : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : Prop

The class of triples whose separating triple at (m, s) lies in the domain of BO_{n, ms} [Kol07, Theorem 68]: ms ≥ 1, order at most ms everywhere, finitely many nonempty boundary members. It is the domain of the round of the separation step.

Equations

• Hironaka.Manifold.BMO.SepClass m s T = Manifold.AnalyticTriple.BOClass (m * s) (Hironaka.Manifold.BMO.sepTripleAt T m s)

theorem Hironaka.Manifold.BMO.sepClass_of_sepOrdLe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {m s : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (hs : 1 ≤ s) (hsep : SepOrdLe T m s) : SepClass m s T

A triple of the marked class which satisfies the separation invariant at s ≥ 1 lies in SepClass m s: the mark ms ≥ 1, the order bound ord_sepIdealAt_le, and the finiteness of the nonempty members from BMOClass.

theorem Hironaka.Manifold.BMO.sepClass_of_isEmptyExtension {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {m s : ℕ} (hT : SepClass m s T) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') {e : F'.ι ↪o T.F.ι} (he : Manifold.HypersurfaceFamily.IsEmptyExtension e) : SepClass m s { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }

The class is indifferent to empty boundary members: deleting or adding empty members keeps the separating ideal (sepTripleAt_eq_of_isEmptyExtension) and the finiteness of the nonempty members.

The class of the round and the order-reduction family read at the separating triple

theorem Hironaka.Manifold.BMO.sepTripleAt_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (hcomp : BMOmod.NonmonomialComap ψ₀) (S : Manifold.AnalyticTriple ψ₀ M) (m s : ℕ) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : sepTripleAt (S.pullback h hh) m s = (sepTripleAt S m s).pullback h hh

The separating triple of a pull-back is the pull-back of the separating triple — the nonmonomial part commutes with pull-back (NonmonomialComap), and pull-back is additive and multiplicative (pullback_add, pullback_pow).

theorem Hironaka.Manifold.BMO.sepClass_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (hcomp : BMOmod.NonmonomialComap ψ₀) [FiniteDimensional 𝕜 E] {T : Manifold.AnalyticTriple ψ₀ M} {m s : ℕ} (hT : SepClass m s T) {N : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) : SepClass m s (T.pullback g hg)

The class is closed under pull-back along local analytic isomorphisms (sepTripleAt_pullback, boClass_of_isPullbackOf).

noncomputable def Hironaka.Manifold.BMO.sepFunctor {𝕜 : Type} [RCLike 𝕜] {n m s : ℕ} (bo : BOanFam 𝕜 n (m * s)) : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => SepClass m s

The order reduction BO_{n, ms} read at the separating triple, as a family functor on SepClass m s: the value of bo at (M, N(𝓘)^m + 𝓘^s, E), re-typed as a family for (M, 𝓘, E) (CompatibleFamily.changeTriple; the triple is not part of the data of a compatible family). This is "we apply order reduction to the ideal N(I)^m + I^s" [Kol07, 111, Step 2]. The link of the separation step is ChainState.linkWith at its value on the induced triple, so the transport lemmas for values at induced triples (AnalyticFamilyFunctor.inducedValue_rel) apply.

Equations

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

@[simp]

theorem Hironaka.Manifold.BMO.sepFunctor_fam_seqOn {𝕜 : Type} [RCLike 𝕜] {n m s : ℕ} (bo : BOanFam 𝕜 n (m * s)) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : SepClass m s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((sepFunctor bo).fam T hT).seqOn U hU = (bo.functor.fam (sepTripleAt T m s) hT).seqOn U hU

theorem Hironaka.Manifold.BMO.sepFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {n m s : ℕ} (bo : BOanFam 𝕜 n (m * s)) (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : (sepFunctor bo).CommutesWithLocalIsos

The family read at the separating triple commutes with local analytic isomorphisms ([Kol07, Theorem 103 (2)] for the composite): the separating triple of a pull-back is the pull-back of the separating triple (sepTripleAt_pullback), and bo commutes.

theorem Hironaka.Manifold.BMO.sepFunctor_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {n m s : ℕ} (bo : BOanFam 𝕜 n (m * s)) : (sepFunctor bo).IndifferentToEmptyMembers

The family read at the separating triple is indifferent to empty boundary members (the counterpart, for boundary members, of [Kol07, 32]): the separating triple of the triple with the replaced boundary is the separating triple with the boundary replaced (sepTripleAt_eq_of_isEmptyExtension), and bo is indifferent.