The chaining of the closed-embedding commutation, IV: codimension zero and the two towers

The predicate AnalyticFamilyFunctor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (s := s) at s = 0 is the second degenerate codimension the printed reduction ([Kol07, 108], the chain of hypersurfaces) does not mention: a closed submanifold of codimension 0 is a clopen set (isClosedSubmanifold_zero_iff'), so

• IsClosedSubmanifold.zeroDiffeomorph, IsClosedSubmanifold.isLocalDiffeomorph_inclusionMap_zero: the bundled codimension-zero submanifold is the open submanifold and its inclusion is a local analytic isomorphism;
• (E2) AnalyticFamilyFunctor.commutesWithClosedEmbeddingsOfEmptyDivisorFam_zero: a functor at the standard model that commutes with local isomorphisms (CommutesWithLocalIsos) and whose centres lie over the cosupport of the restricted ideal (FiniteSuccession.CentersOver, [Kol07, Definition 66, (4′)]) commutes with codimension-zero closed embeddings through itself: its value on U ∩ S is the pull-back of its value on U along the open inclusion, and the push-forward of that pull-back along the clopen S ∩ U is the value on U itself (Hironaka.Resolution.Analytic.Restrict.FlagPushforward; pushforwardRestrict_eq, pullback_comp, the eraseEmpty lemmas);
• (E3′) BMOanFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam_all, BMOmodFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam_all: the two towers, for the marked order-reduction records BMOanFam 𝕜 n 1 ([Kol07, Theorem 35, (5)], [Kol07, Claim 71.2]) and the modified marked resolution records BMOmodFam 𝕜 n ([Wlo09, §7.1]): the tower lemma (E3) of Hironaka.Resolution.Analytic.Functor.ChainClosedEmbeddingChain on the marked class BMOClass 1, with (E2) discharging the codimension-zero clause through the order clause isOfOrderGe of the records (CentersOver.of_isOfOrderGe).

The codimension-zero inclusion is a local analytic isomorphism

def Manifold.IsClosedSubmanifold.toOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : IsClosedSubmanifold ψ S 0) : TopologicalSpace.Opens M.carrier

A closed submanifold of codimension 0 (a clopen set, isClosedSubmanifold_zero_iff') as an open subset.

Equations

• hS.toOpens = { carrier := S, is_open' := ⋯ }

def Manifold.IsClosedSubmanifold.zeroDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : IsClosedSubmanifold ψ S 0) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 0) → 𝕜)) (modelWithCornersSelf 𝕜 E) hS.toAnalyticManifold.carrier (M.restrict hS.toOpens).carrier ⊤

The bundled codimension-zero submanifold IS the open submanifold: the identity of the carrier is an analytic isomorphism between the two structures (contMDiff_codRestrict_opens one way, IsClosedSubmanifold.contMDiff_codRestrict the other).

Equations

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

theorem Manifold.IsClosedSubmanifold.isLocalDiffeomorph_inclusionMap_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : IsClosedSubmanifold ψ S 0) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 0) → 𝕜)) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hS.inclusionMap

The inclusion of a codimension-zero closed submanifold is a local analytic isomorphism: it is the open inclusion (isLocalDiffeomorph_inclusion) composed with zeroDiffeomorph.

(E2)

theorem Hironaka.Manifold.AnalyticFamilyFunctor.commutesWithClosedEmbeddingsOfEmptyDivisorFam_zero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {Dom : {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} → Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M → Prop} (B : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Dom) (hB : B.CommutesWithLocalIsos) (hcen : ∀ {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Dom T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((B.fam T hT).seqOn U hU).toSuccession.CentersOver (Manifold.IdealSheaf.support (T.pullback (M.inclusion U) ⋯).I)) : B.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B

(E2), the degenerate case s = 0: a functor at the standard model that commutes with local isomorphisms and whose every centre lies over the cosupport of the restricted ideal commutes with codimension-zero closed embeddings through itself.

(E3′) the two towers

theorem Hironaka.Manifold.BMOanFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam_all {𝕜 : Type} [RCLike 𝕜] (bmo : (n : ℕ) → BMOanFam 𝕜 n 1) (h1 : ∀ (m : ℕ), 0 < m → (bmo m).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmo (m - 1)).functor) (n s : ℕ) : (bmo n).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmo (n - s)).functor

The marked tower ([Kol07, Theorem 35, (5)], [Kol07, Claim 71.2], [Kol07, 108]): for bmo : ∀ n, BMOanFam 𝕜 n 1 with the codimension-one inputs at every positive level, the commutation at every codimension. The tower lemma (E3) on the marked class BMOClass 1 (closed under pull-back, bmoClass_pullback; the restricted empty-divisor triple lies in it, bmoClass_one_of_isEmpty), with the codimension-zero clause from (E2) and CentersOver from the order clause BMOanFam.isOfOrderGe at mark 1 (CentersOver.of_isOfOrderGe).

theorem Hironaka.Manifold.BMOmodFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam_all {𝕜 : Type} [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (h1 : ∀ (m : ℕ), 0 < m → (bmod m).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmod (m - 1)).functor) (n s : ℕ) : (bmod n).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmod (n - s)).functor

The modified tower ([Wlo09, §7.1]; [Kol07, Theorem 35, (5)]): for bmod : ∀ n, BMOmodFam 𝕜 n with the codimension-one inputs at every positive level, the commutation at every codimension. The same assembly as the marked tower; CentersOver from the order clause BMOmodFam.isOfOrderGe (which coincides with center_mem_support at mark 1).