Simple normal crossings families and the boundary predicates along an analytic isomorphism

The simple-normal-crossings vocabulary of Hironaka/Manifold/Snc/Defs.lean — a family G : HypersurfaceFamily M being simple normal crossings in a chart isomorphism ψ₀ : E ≃L[𝕜] (Fin n → 𝕜) (IsSnc), a set having simple normal crossings with it (HasSncWith), its reduced ideal sheaf (idealSheaf) — and the boundary predicates of the analytic main theorems in their family form (AnalyticManifold.IdealSheaf.IsSncBoundary, IsSncBoundaryWith; [Kol07, Definition 24], [Wlo09, Definition 3.2.4]) transport along an analytic isomorphism g : N ≃ M across the models (Diffeomorph 𝓘(𝕜, E') 𝓘(𝕜, E) N M ω), the family being pulled back as G.comap g.

• IsSnc and HasSncWith transport in one direction for any two chart isomorphisms ψ₀ : E ≃L (Fin n → 𝕜), ψ₁ : E' ≃L (Fin n → 𝕜): the model isomorphism ψ₀.trans ψ₁.symm and the chart device of Hironaka/Resolution/Analytic/ModelTransport/SquareChart.lean read an snc chart of G at g a as an snc chart of G.comap g at a (IsSncChartAt.of_square), the closed hypersurfaces pull back (IsClosedSubmanifold.preimage_of_square, re-read through IsClosedSubmanifold.congr_cle), local finiteness by Mathlib's LocallyFinite.preimage_continuous; the converse is the same direction along g⁻¹, with (G.comap g).comap g⁻¹ = G.
• The reduced ideal sheaf: both branches of the definition correspond — the vanishing stalks of g⁻¹(|G|) are the images of those of |G| under the stalk isomorphism of g and local generators are carried both ways (Hironaka/Resolution/Analytic/ModelTransport/Square.lean).
• The boundary predicates are existential in the chart isomorphism, so their transport takes the model isomorphism ψ : E ≃L[𝕜] E': the witness on the other model is ψ.trans ψ₁' towards M, ψ.symm.trans ψ₀ towards N, and the family is G.comap g⁻¹, G.comap g. In the main theorems ψ is the transport's ContinuousLinearEquiv.ofFinrankEq.
• The two predicates of Włodarczyk's embedded desingularization, the transversal boundary predicate IsSncBoundaryTransversalTo and the factorization predicate IsMulBoundaryMonomial ([Wlo09, Theorem 2.0.2 (3) and (6)]), pull back along g in the same way (IsSncBoundaryTransversalTo.pullbackDiffeomorph, IsMulBoundaryMonomial.pullbackDiffeomorph).
• isSnc_congr_chart: the corollary at g := Diffeomorph.refl — IsSnc does not depend on the chart isomorphism.

Bookkeeping: pull-backs of families, the two chart isomorphisms

@[simp]

theorem Manifold.HypersurfaceFamily.comap_id {X : Type u} (G : HypersurfaceFamily X) : comap id G = G

Pulling a family back along the identity is the identity.

theorem Manifold.HypersurfaceFamily.comap_symm_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (G : HypersurfaceFamily M.carrier) : comap (⇑g.symm) (comap (⇑g) G) = G

Pulling back along g and then along g⁻¹ is the identity.

theorem Hironaka.Manifold.Diffeomorph.symm_preimage_preimage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (S : Set M.carrier) : ⇑g.symm ⁻¹' ⇑g ⁻¹' S = S

g⁻¹ ⁻¹' (g ⁻¹' S) = S.

theorem Hironaka.Manifold.trans_symm_symm_trans_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (ψ₁ : E' ≃L[𝕜] Fin n → 𝕜) (v : E') : ((ψ₀.trans ψ₁.symm).symm.trans ψ₀) v = ψ₁ v

Through the model isomorphism ψ₁⁻¹ ∘ ψ₀ : E ≃ E', the chart isomorphism ψ₀ of E re-reads as ψ₁ on E' (pointwise).

theorem Manifold.IsClosedSubmanifold.congr_cle {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {n : ℕ} {ψ ψ' : E ≃L[𝕜] Fin n → 𝕜} (h : ∀ (v : E), ψ v = ψ' v) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : IsClosedSubmanifold ψ' Y c

The closed-submanifold predicate depends on the chart isomorphism only pointwise.

Simple normal crossings along g

theorem Manifold.HypersurfaceFamily.IsSncChartAt.of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (ψ₁ : E' ≃L[𝕜] Fin n → 𝕜) (G : HypersurfaceFamily M.carrier) {φ : OpenPartialHomeomorph M.carrier E} {a : N.carrier} {c : { j : G.ι // g a ∈ G.hyp j } → Fin n} (h : IsSncChartAt ψ₀ G φ (g a) c) : IsSncChartAt ψ₁ (comap (⇑g) G) (Hironaka.Manifold.chartOfSquare g (ψ₀.trans ψ₁.symm) φ) a c

An snc chart of G at g a in the chart isomorphism ψ₀ reads, through g and the model isomorphism ψ₁⁻¹ ∘ ψ₀, as an snc chart of G.comap g at a in ψ₁, with the same coordinate indices.

theorem Manifold.HypersurfaceFamily.isSnc_comap_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (ψ₁ : E' ≃L[𝕜] Fin n → 𝕜) (G : HypersurfaceFamily M.carrier) (hG : IsSnc ψ₀ G) : IsSnc ψ₁ (comap (⇑g) G)

The forward direction, for any two chart isomorphisms: an snc family pulled back along g is snc — the hypersurfaces by IsClosedSubmanifold.preimage_of_square re-read in ψ₁, local finiteness by LocallyFinite.preimage_continuous, the snc charts by IsSncChartAt.of_square.

theorem Manifold.HypersurfaceFamily.isSnc_comap_diffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (ψ₁ : E' ≃L[𝕜] Fin n → 𝕜) (G : HypersurfaceFamily M.carrier) : IsSnc ψ₁ (comap (⇑g) G) ↔ IsSnc ψ₀ G

An snc family pulled back along an analytic isomorphism across the models is snc, in any chart isomorphism of the target model, and conversely: the converse is the forward direction along g⁻¹.

theorem Manifold.HypersurfaceFamily.hasSncWith_comap_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (ψ₁ : E' ≃L[𝕜] Fin n → 𝕜) (G : HypersurfaceFamily M.carrier) {Y : Set M.carrier} {c : ℕ} (hG : HasSncWith ψ₀ G Y c) : HasSncWith ψ₁ (comap (⇑g) G) (⇑g ⁻¹' Y) c

The forward direction: HasSncWith along g — the adapted snc chart at g a reads as an adapted snc chart at a.

theorem Manifold.HypersurfaceFamily.hasSncWith_comap_diffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (ψ₁ : E' ≃L[𝕜] Fin n → 𝕜) (G : HypersurfaceFamily M.carrier) (Y : Set M.carrier) (c : ℕ) : HasSncWith ψ₁ (comap (⇑g) G) (⇑g ⁻¹' Y) c ↔ HasSncWith ψ₀ G Y c

HasSncWith along an analytic isomorphism across the models: g⁻¹(Y) has simple normal crossings with G.comap g in ψ₁ iff Y has with G in ψ₀.

theorem Manifold.HypersurfaceFamily.idealSheaf_comap_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (G : HypersurfaceFamily M.carrier) : (comap (⇑g) G).idealSheaf = AnalyticManifold.IdealSheaf.pullbackDiffeomorph g G.idealSheaf

The reduced ideal sheaf of a family along an analytic isomorphism across the models is the pull-back of the reduced ideal sheaf: both branches of the definition correspond — the vanishing stalks of g⁻¹(|G|) are the images of those of |G| under the stalk isomorphism of g, and local generators are carried both ways.

theorem Manifold.HypersurfaceFamily.isSnc_congr_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {n : ℕ} (ψ₀ ψ₀' : E ≃L[𝕜] Fin n → 𝕜) (G : HypersurfaceFamily M.carrier) : IsSnc ψ₀' G ↔ IsSnc ψ₀ G

IsSnc does not depend on the chart isomorphism: the corollary of isSnc_comap_diffeomorph_iff at g := Diffeomorph.refl.

The boundary predicates of the main theorems along g, with the model isomorphism

theorem AnalyticManifold.IdealSheaf.isSncBoundary_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (B : M.IdealSheaf) : (pullbackDiffeomorph g B).IsSncBoundary ↔ B.IsSncBoundary

The boundary predicate IsSncBoundary of the main theorems along an analytic isomorphism across the models, with the model isomorphism ψ: the snc family and its chart isomorphism are carried by isSnc_comap_diffeomorph and idealSheaf_comap_diffeomorph (ψ.trans ψ₁' towards M, ψ.symm.trans ψ₀ towards N).

theorem AnalyticManifold.IdealSheaf.isSncBoundaryWith_pullbackDiffeomorph_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') (B D : M.IdealSheaf) : (pullbackDiffeomorph g B).IsSncBoundaryWith (pullbackDiffeomorph g D) ↔ B.IsSncBoundaryWith D

The boundary-with-centre predicate IsSncBoundaryWith of the main theorems along an analytic isomorphism across the models, with the model isomorphism ψ: isSnc_comap_diffeomorph, hasSncWith_comap_diffeomorph (on (D.pullbackDiffeomorph g).support = g⁻¹(D.support)) and idealSheaf_comap_diffeomorph.

theorem AnalyticManifold.IdealSheaf.IsSncBoundaryTransversalTo.pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {B Y : M.IdealSheaf} (h : B.IsSncBoundaryTransversalTo Y) : (IdealSheaf.pullbackDiffeomorph g B).IsSncBoundaryTransversalTo (IdealSheaf.pullbackDiffeomorph g Y)

The transversal boundary predicate IsSncBoundaryTransversalTo of Włodarczyk's embedded desingularization along an analytic isomorphism across the models, with the model isomorphism ψ: the family is G.comap g (isSnc_comap_diffeomorph, idealSheaf_comap_diffeomorph), and at a point a of g⁻¹(Y) the adapted snc chart of G at g a is read through g (chartOfSquare, IsAdaptedChart.of_square, IsSncChartAt.of_square), the coordinate indices, hence the transversality, unchanged.

theorem AnalyticManifold.IdealSheaf.IsMulBoundaryMonomial.pullbackDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (ψ : E ≃L[𝕜] E') {J Y B : M.IdealSheaf} (h : J.IsMulBoundaryMonomial Y B) : (IdealSheaf.pullbackDiffeomorph g J).IsMulBoundaryMonomial (IdealSheaf.pullbackDiffeomorph g Y) (IdealSheaf.pullbackDiffeomorph g B)

The factorization predicate IsMulBoundaryMonomial of Włodarczyk's embedded desingularization along an analytic isomorphism across the models, with the model isomorphism ψ: the family is G.comap g, and at every point x the stalk identity at g x is carried by the stalk isomorphism of g, which maps products, powers and the vanishing ideals of the components of G to those of the components of G.comap g (vanishingStalk_preimage_pullbackDiffeomorph).