The centres of codimension at most one lie in the exceptional divisor

Włodarczyk blows up only centres of codimension at least two Wlo09, Remark (2) after Theorem 2.0.3, and a centre of codimension one has an isomorphism as its blow-up and becomes a component of the exceptional divisor [Wlo09, Remark (1) after Theorem 2.0.3]. For a succession whose centres lie over the singular locus Sing(Y) of a reduced subspace Y and have simple normal crossings with the exceptional divisors, this module proves that every centre of codimension at most one lies in the exceptional divisor of its stage, and has codimension exactly one (FiniteSuccession.center_subset_support_totalTransformSeq_of_codim_le_one): at a point of the centre off the exceptional divisor the composite blow-down is a local analytic isomorphism (its germ map is bijective, germMap_stageMap_bijective_of_notMem_support), and transports the centre, a smooth hypersurface or an open set, into Sing(Y), which contains no such germ (IdealSheaf.not_subset_sing_of_isClosedSubmanifold_one, not_subset_sing_of_isOpen, Hironaka/Resolution/Analytic/Wlo09/SingularHypersurface.lean), read on the open complement of the exceptional divisor. A nonempty open centre has a point off the exceptional divisor: in an snc chart, a point with all the coordinates of the components through the centre's point nonzero (exists_notMem_support_of_isSncChartAt). Hence, in the simple normal crossings chart of the centre, a centre of codimension one is a coordinate hyperplane contained in the union of the coordinate hyperplanes of the exceptional components, so it is one of them, as Włodarczyk's Remark (1) says. The arguments are not in the sources.

Stalks along a bijective germ map

theorem AnalyticManifold.IdealSheaf.mem_support_pullback_iff_of_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (g : AnalyticMap N M) {b : N.carrier} (hb : Function.Bijective ⇑(Manifold.germMap ⇑g ⋯ b)) : b ∈ (Manifold.IdealSheaf.pullback ⇑g ⋯ J).support ↔ g b ∈ Manifold.IdealSheaf.support J

Where the germ map of g is bijective, b lies in the support of g^*J iff g b lies in the support of J.

theorem AnalyticManifold.IdealSheaf.isRegularLocalRing_quotient_stalkIdeal_pullback_iff_of_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (g : AnalyticMap N M) {b : N.carrier} (hb : Function.Bijective ⇑(Manifold.germMap ⇑g ⋯ b)) : IsRegularLocalRing (stalkRing N b ⧸ (Manifold.IdealSheaf.pullback ⇑g ⋯ J).stalkIdeal b) ↔ IsRegularLocalRing (stalkRing M (g b) ⧸ Manifold.IdealSheaf.stalkIdeal J (g b))

Where the germ map of g is bijective, the quotient of the stalk by g^*J is regular iff the quotient at the image point by J is.

theorem AnalyticManifold.IdealSheaf.isRadical_stalkIdeal_pullback_iff_of_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (g : AnalyticMap N M) {b : N.carrier} (hb : Function.Bijective ⇑(Manifold.germMap ⇑g ⋯ b)) : ((Manifold.IdealSheaf.pullback ⇑g ⋯ J).stalkIdeal b).IsRadical ↔ (Manifold.IdealSheaf.stalkIdeal J (g b)).IsRadical

Where the germ map of g is bijective, the stalk of g^*J is radical iff the stalk of J at the image point is.

A point of a chart off the components through its centre

theorem Manifold.HypersurfaceFamily.exists_notMem_support_of_isSncChartAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a c) {O : Set M} (hO : IsOpen O) (haO : a ∈ O) : ∃ a' ∈ O ∩ φ.source, a' ∉ F.support

An open neighbourhood of a point of an snc family contains a point off the family: in an snc chart at a, a point with every coordinate of the components through a moved off 0, inside the open set avoiding the components not through a.

The centres of codimension at most one

theorem AnalyticManifold.FiniteSuccession.center_subset_support_totalTransformSeq_of_codim_le_one {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (S : M.FiniteSuccession) (I : M.IdealSheaf) (hI : I.IsReduced) (hc : S.CentersOver (Manifold.IdealSheaf.support I \ I.regularLocus)) (i : Fin S.length) (hsnc : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (S.totalTransformSeq i.castSucc)) (hsncw : Manifold.HypersurfaceFamily.HasSncWith (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (S.totalTransformSeq i.castSucc) (Manifold.IdealSheaf.support (S.center i)) (S.codim i)) (hcod : S.codim i ≤ 1) (hne : (Manifold.IdealSheaf.support (S.center i)).Nonempty) : S.codim i = 1 ∧ Manifold.IdealSheaf.support (S.center i) ⊆ (S.totalTransformSeq i.castSucc).support

A centre of codimension at most one lies in the exceptional divisor, and has codimension one ([Wlo09, Remarks (1) and (2) after Theorem 2.0.3]), for a succession whose centres lie over the singular locus of a reduced Y and have simple normal crossings with the exceptional divisors: off the exceptional divisor the composite blow-down has bijective germ maps and carries the centre, a smooth hypersurface or an open set, into Sing(Y), which contains neither (IdealSheaf.not_subset_sing_of_isClosedSubmanifold_one, IdealSheaf.not_subset_sing_of_isOpen, read on the open complement of the exceptional divisor); a nonempty open centre has a point off the exceptional divisor (exists_notMem_support_of_isSncChartAt).

theorem AnalyticManifold.FiniteSuccession.boundarySeq_le_center_of_codim_le_one {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (S : M.FiniteSuccession) (I : M.IdealSheaf) (hI : I.IsReduced) (hc : S.CentersOver (Manifold.IdealSheaf.support I \ I.regularLocus)) (i : Fin S.length) (hsnc : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (S.totalTransformSeq i.castSucc)) (hsncw : Manifold.HypersurfaceFamily.HasSncWith (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (S.totalTransformSeq i.castSucc) (Manifold.IdealSheaf.support (S.center i)) (S.codim i)) (hbd : S.boundarySeq ⊤ i.castSucc = (S.totalTransformSeq i.castSucc).idealSheaf) (hne : (Manifold.IdealSheaf.support (S.center i)).Nonempty) {n' c : ℕ} (ψ' : (Fin n → 𝕜) ≃L[𝕜] Fin n' → 𝕜) (hc1 : c ≤ 1) (hC : Manifold.IsClosedSubmanifold ψ' (Manifold.IdealSheaf.support (S.center i)) c) : c = 1 ∧ ∀ (a : ↑↧(S.stage i.castSucc).carrier), Manifold.IdealSheaf.stalkIdeal (S.boundarySeq ⊤ i.castSucc) a ≤ Manifold.IdealSheaf.stalkIdeal (S.center i) a

The boundary of a stage lies in the ideal sheaf of a centre of codimension at most one, which has codimension one: the clause two_le_codim_or_boundarySeq_le_center of IsLocallyFinitelyDesingularizedBy for one step, in the form of two_le_codim_or_boundarySeq_le_center_iff, from center_subset_support_totalTransformSeq_of_codim_le_one, the identification of the boundary with the reduced ideal sheaf of the exceptional family (hbd), and the stalks of the centre's ideal sheaf, the vanishing ideals of the centre (isIdealSheafOf_center, Hadamard's lemma vanishingStalk_zeroSet_eq_span_coord). The codimension c of the hypothesis is the chosen one (IsClosedSubmanifold.codim_eq_of_nonempty).

The codimension of a nonempty centre

theorem AnalyticManifold.FiniteSuccession.two_le_codim_or_boundarySeq_le_center_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) (hne : S.center i ≠ ⊤) : (2 ≤ S.codim i ∨ S.codim i = 1 ∧ ∀ (x : ↑↧(S.stage i.castSucc).carrier), Manifold.IdealSheaf.stalkIdeal (S.boundarySeq ⊤ i.castSucc) x ≤ Manifold.IdealSheaf.stalkIdeal (S.center i) x) ↔ ∀ {n' c : ℕ} (ψ' : E ≃L[𝕜] Fin n' → 𝕜), c ≤ 1 → Manifold.IsClosedSubmanifold ψ' (Manifold.IdealSheaf.support (S.center i)) c → c = 1 ∧ ∀ (x : ↑↧(S.stage i.castSucc).carrier), Manifold.IdealSheaf.stalkIdeal (S.boundarySeq ⊤ i.castSucc) x ≤ Manifold.IdealSheaf.stalkIdeal (S.center i) x

The codimension condition on a nonempty centre, in two forms: the centre C_i has codimension at least two, or codimension one and lies in the exceptional divisor E_i of its stage (read through the chosen codimension S.codim i, with E_i stalkwise in the ideal sheaf of C_i), exactly when every codimension c ≤ 1 in which C_i is a closed submanifold, for any chart of the model space, is one, with E_i stalkwise in the ideal sheaf of C_i. A nonempty closed submanifold has one codimension (IsClosedSubmanifold.codim_eq_of_nonempty), and C_i ≠ ⊤ makes the centre nonempty (IdealSheaf.eq_top_of_support_eq_empty).