The chaining of the closed-embedding commutation, I: the degenerate codimensions

[Kol07, 108] reduces the commutation of the order-reduction functors with closed embeddings to the hypersurface case along a flag Y = Y₀ ⊂ Y₁ ⊂ ⋯ ⊂ Y_c = X. The predicate AnalyticFamilyFunctor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (s := s) has two degenerate codimensions the printed reduction (the chain of hypersurfaces) does not mention: s > n, where every closed submanifold of codimension s of an n-dimensional manifold is empty, and s = 0 (the codimension-zero clause, Hironaka.Resolution.Analytic.Functor.ChainClosedEmbeddingZero). This module proves the first:

• BlowUpSequence.eq_nil_of_isEmpty: a list of centres without empty centres on an empty manifold is nil (a first centre would be a nonempty subset of the empty carrier);
• AnalyticFamilyFunctor.commutesWithClosedEmbeddingsOfEmptyDivisorFam_of_lt: at a codimension s > n the predicate holds through any partner functor, given the codimension-zero clause of the outer functor (through some partner) and the restriction of its domain to the empty submanifold. The closed submanifold is empty (IsClosedSubmanifold.codim_le'), so the right side of the per-open identity is the push-forward of a list on the empty manifold, nil; the left side is the value of the functor on a triple whose ideal contains the unit ideal of the empty submanifold, which the codimension-zero clause at the empty submanifold (a closed submanifold of every codimension, isClosedSubmanifold_empty'; its reduced ideal is independent of the codimension, idealSheaf_eq_of_set) reads as the push-forward of a list on the empty manifold, nil again.

The tower lemma uses this case at every s ≥ n, where its codimension-one hypothesis h1 ((F m).CommutesWithClosedEmbeddingsOfEmptyDivisorFam (s := 1) (F (m - 1)) for 0 < m) is not available at m = n - s = 0.

theorem AnalyticManifold.BlowUpSequence.eq_nil_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (hM : IsEmpty M.carrier) (L : BlowUpSequence ψ₀ M) (hL : L.NoEmptyCenters) : L = nil M

A list of centres without empty centres on an empty manifold is the empty list — a first centre would be a nonempty subset of the empty carrier.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.commutesWithClosedEmbeddingsOfEmptyDivisorFam_of_lt {𝕜 : 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) {Dom₀ : {M₀ : AnalyticManifold 𝕜 (Fin (n - 0) → 𝕜)} → Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 0) → 𝕜)) M₀ → Prop} (B₀ : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 0) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 0) → 𝕜)} => Dom₀) {s : ℕ} {Dom' : {M' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} → Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) M' → Prop} (B' : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} => Dom') (hlt : n < s) (h0 : B.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B₀) (hDom0 : ∀ {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (hJ : (Manifold.IdealSheaf.pullback ⇑⋯.inclusionMap ⋯ I).IsNonzeroEverywhere), ⋯.idealSheaf ≤ I → Dom { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ } → Dom₀ { I := Manifold.IdealSheaf.pullback ⇑⋯.inclusionMap ⋯ I, isNonzeroEverywhere := hJ, F := Manifold.HypersurfaceFamily.empty ⋯.toAnalyticManifold.carrier, isSnc := ⋯ }) : B.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B'

The degenerate case s > n ([Kol07, 108] prints only the chain of hypersurfaces): at a codimension s > n every closed submanifold of an n-dimensional manifold is empty (IsClosedSubmanifold.codim_le'), so the predicate holds through ANY partner B', given the codimension-zero clause of B (through some B₀) and the restriction of the domain to the empty submanifold: both sides of the per-open identity are nil.