The stalk-level clauses of [Kol07, Definition 66] along a local analytic isomorphism

In the global case of the proof of [Kol07, Theorem 103] the functor BO_{n,m} is descended along the surjective cover g : X^* → X, and the clauses of [Kol07, Definition 66] are carried back along it (the proof remarks, at the end of its local case, that the functoriality package is local): the order of the marked transform along the centre and the normal-crossings condition of the boundary with the centre are conditions on the stalks at the points of the centre, carried both ways by the bijective germ map of a local analytic isomorphism at a point (germMap_bijective_of_isLocalDiffeomorphAt). This file states them pointwise, for an analytic map h : N → M that is a local analytic isomorphism at the point:

• IdealSheaf.ordAlongIdeal_comap_of_isLocalDiffeomorphAt: the order of J along the centre D transports (ordAlongIdeal_pullback_diffeomorph, at a point);
• IdealSheaf.genericOrdAlong_comap_of_isLocalDiffeomorph: the generic order along the centre Y transports (both sides ⊤ off the centre, genericOrdAlong_eq_ordAlong on it);
• NormalCrossingsData, the stalk-level content of HasOnlyNormalCrossingsWith at a point, and its transport along a bijective ring map (NormalCrossingsData.map); HasOnlyNormalCrossingsWith.comap_of_isLocalDiffeomorph (pull-back) and HasOnlyNormalCrossingsWith.of_comap_of_surjective (descent along a surjective local isomorphism: every point of the centre has a preimage, and the inverse germ map carries the data back);
• the vanishing ideals and local generators along a local isomorphism, the naturality of Hironaka's reduced transform red(f⁻¹(E) ∪ f⁻¹(D)) along a square with a surjective local isomorphism (reducedTransform_comap_of_surjective), and the transforms of one blowing-up along the lift of a local isomorphism (totalTransform_comap_liftStep, exceptionalIdealSheaf_comap_liftStep, birationalTransform_comap_liftStep, reducedTransform_comap_liftStep, weakTransform_comap_liftStep).

These are the stalkwise inputs of the stage-by-stage description of the pull-back of a list of centres in Hironaka.Resolution.Analytic.Functor.PullbackSequence.

The order along a centre

theorem Manifold.IdealSheaf.ordAlongIdeal_comap_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (D J : M.IdealSheaf) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) : (pullback ⇑h ⋯ D).ordAlongIdeal (pullback ⇑h ⋯ J) b = ordAlongIdeal D J (h b)

The order of J along the centre D transports along a local analytic isomorphism at a point: the stalk ideals are carried by the bijective germ map, which preserves inclusions and powers (ordAlongIdeal_pullback_diffeomorph, pointwise).

theorem Manifold.IdealSheaf.genericOrdAlong_eq_top_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (D J : M.IdealSheaf) {a : M.carrier} (ha : a ∉ support D) : genericOrdAlong D J a = ⊤

The generic order along a centre is ⊤ off the centre (the component is empty).

theorem Manifold.IdealSheaf.genericOrdAlong_comap_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (J : M.IdealSheaf) (b : N.carrier) : ⋯.idealSheaf.genericOrdAlong (pullback ⇑h ⋯ J) b = hY.idealSheaf.genericOrdAlong J (h b)

The generic order of J along the centre Y transports along a local analytic isomorphism: on the centre it is the order along the centre (genericOrdAlong_eq_ordAlong), which transports pointwise; off the centre both sides are ⊤.

Normal crossings at a point

def Hironaka.Manifold.NormalCrossingsData {R : Type u_2} [CommRing R] [IsLocalRing R] (I D : Ideal R) : Prop

The stalk-level content of HasOnlyNormalCrossingsWith E D at a point (Hironaka's Definition 2, [Hir64, Ch. 0, §5, p. 141], as in the vocabulary of the main theorems): a regular system of parameters z containing an equation of each minimal prime of I and generating D.

Equations

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

theorem Hironaka.Manifold.NormalCrossingsData.map {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (e : R →+* S) (he : Function.Bijective ⇑e) {I D : Ideal R} (h : NormalCrossingsData I D) : NormalCrossingsData (Ideal.map e I) (Ideal.map e D)

The normal-crossings data transport along a bijective ring map (argument for the germ map of a diffeomorphism, made algebraic): the regular system of parameters, the minimal primes and the generators of D are carried by e.

theorem Hironaka.Manifold.NormalCrossingsData.of_map {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (e : R →+* S) (he : Function.Bijective ⇑e) {I D : Ideal R} (h : NormalCrossingsData (Ideal.map e I) (Ideal.map e D)) : NormalCrossingsData I D

The inverse transport: data for the images along a bijective ring map come from data for the ideals themselves.

theorem Hironaka.Manifold.hasOnlyNormalCrossingsWith_iff_normalCrossingsData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (E' D : M.IdealSheaf) : E'.HasOnlyNormalCrossingsWith D ↔ ∀ x ∈ Manifold.IdealSheaf.support D, NormalCrossingsData (Manifold.IdealSheaf.stalkIdeal E' x) (Manifold.IdealSheaf.stalkIdeal D x)

HasOnlyNormalCrossingsWith is the pointwise normal-crossings data at the points of the support of D.

theorem Hironaka.Manifold.HasOnlyNormalCrossingsWith.comap_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {E' D : M.IdealSheaf} (hE : E'.HasOnlyNormalCrossingsWith D) : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith (Manifold.IdealSheaf.pullback ⇑h ⋯ E') (Manifold.IdealSheaf.pullback ⇑h ⋯ D)

Hironaka's Definition 2 pulls back along a local analytic isomorphism (HasOnlyNormalCrossingsWith.pullback_diffeomorph, for a local isomorphism): the data at h b are carried to b by the bijective germ map.

theorem Hironaka.Manifold.HasOnlyNormalCrossingsWith.of_comap_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) {E' D : M.IdealSheaf} (hE : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith (Manifold.IdealSheaf.pullback ⇑h ⋯ E') (Manifold.IdealSheaf.pullback ⇑h ⋯ D)) : E'.HasOnlyNormalCrossingsWith D

Hironaka's Definition 2 descends along a surjective local analytic isomorphism: every point of the centre has a preimage, at which the data of the pull-backs are the images of the data at the point under the bijective germ map.

Vanishing ideals and local generators along a local isomorphism

theorem Hironaka.Manifold.Germ.vanishesOn_compTendsto_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) (Z : Set M.carrier) (k : (nhds (h b)).Germ 𝕜) : Manifold.Germ.VanishesOn (⇑h ⁻¹' Z) b (k.compTendsto ⇑h ⋯) ↔ Manifold.Germ.VanishesOn Z (h b) k

A function germ at h b vanishes on Z iff its composite with h vanishes on h⁻¹(Z) at b, for h a local analytic isomorphism at b (embedding lemma at a point: on the source of a local inverse h is a homeomorphism onto an open set, so it maps the trace of the neighbourhood filter on h⁻¹(Z) onto the trace on Z).

theorem Hironaka.Manifold.vanishingStalk_preimage_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {b : N.carrier} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) b) (Z : Set M.carrier) : Manifold.vanishingStalk (⇑h ⁻¹' Z) b = Ideal.map (Manifold.germMap ⇑h ⋯ b) (Manifold.vanishingStalk Z (h b))

The vanishing ideal of h⁻¹(Z) at b is the image of the vanishing ideal of Z at h b under the bijective germ map of the local analytic isomorphism h at b (vanishingStalk_preimage_diffeomorph, pointwise).

theorem Hironaka.Manifold.hasLocalGenerators_vanishingStalk_preimage_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (W : Set M.carrier) (hW : Manifold.IdealSheaf.HasLocalGenerators fun (y : M.carrier) => Manifold.vanishingStalk W y) : Manifold.IdealSheaf.HasLocalGenerators fun (x : N.carrier) => Manifold.vanishingStalk (⇑h ⁻¹' W) x

Local generators of the vanishing ideals pull back along a local analytic isomorphism.

theorem Manifold.IdealSheaf.HasLocalGenerators.of_map_germMap_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) (I : (x : M.carrier) → Ideal ↑((structureSheaf 𝕜 E M.carrier).presheaf.stalk x)) (hI : HasLocalGenerators fun (b : N.carrier) => Ideal.map (germMap ⇑h ⋯ b) (I (h b))) : HasLocalGenerators I

Local generators descend along a surjective local analytic isomorphism: for a family of stalk ideals I on M, if the pulled-back family b ↦ (germMap h b)(I (h b)) on N has local generators, so has I — at x = h q the generators near q are pushed forward along a local inverse of h (their germs at the points of the image open set are carried by the stalk map of the inverse, the two-sided inverse of the germ map of h).

The reduced transform along a surjective local isomorphism

theorem Hironaka.Manifold.reducedTransform_comap_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ M₂ N₁ N₂ : AnalyticManifold 𝕜 E} (h : AnalyticMap M₁ M₂) (f₁ : AnalyticMap N₁ M₁) (f₂ : AnalyticMap N₂ M₂) (ℓ : AnalyticMap N₁ N₂) (hℓ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ℓ) (hs : Function.Surjective ⇑ℓ) (hsq : ∀ (x : N₁.carrier), f₂ (ℓ x) = h (f₁ x)) (D B : M₂.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑ℓ ⋯ (AnalyticManifold.IdealSheaf.reducedTransform f₂ B D) = AnalyticManifold.IdealSheaf.reducedTransform f₁ (Manifold.IdealSheaf.pullback ⇑h ⋯ B) (Manifold.IdealSheaf.pullback ⇑h ⋯ D)

Hironaka's red(f⁻¹(E) ∪ f⁻¹(D)) (reducedTransform) is natural along a square f₂ ∘ ℓ = h ∘ f₁ of analytic maps with ℓ a surjective local analytic isomorphism (reducedTransform_pullback_of_comp_eq with the diffeomorphism replaced by a surjective local isomorphism): the closed sets correspond, the vanishing ideals along the bijective germ maps, and the local-generator condition pulls back and — this is where surjectivity enters — descends.

One step of the pull-back: the transforms along the lift of the blowing-up

theorem Hironaka.Manifold.totalTransform_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (J : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY) ⋯ (Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ hY) ⋯ J) = Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ ⋯) ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ J)

The total transform along the lift Bl_{h⁻¹Y} N → Bl_Y M of a local analytic isomorphism (liftStep): ℓ^* π^* J = π'^* h^* J (π ∘ ℓ = h ∘ π').

theorem Hironaka.Manifold.exceptionalIdealSheaf_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) : Manifold.IdealSheaf.pullback ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY) ⋯ (Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ hY) ⋯ hY.idealSheaf) = Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ ⋯) ⋯ ⋯.idealSheaf

The exceptional ideal sheaf along the lift: ℓ^* I_F = I_{F'} (comap_idealSheaf_of_isLocalDiffeomorph for the centre).

theorem Hironaka.Manifold.birationalTransform_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (J : Manifold.MarkedIdealSheaf (Manifold.structureSheaf 𝕜 E M.carrier)) (hm : ∀ a ∈ Y, ↑J.m ≤ hY.idealSheaf.ordAlongIdeal J.I a) : Manifold.IdealSheaf.pullback ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY) ⋯ (Manifold.MarkedIdealSheaf.birationalTransform hY ⋯ J).I = (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := Manifold.IdealSheaf.pullback ⇑h ⋯ J.I, m := J.m }).I

Kollár's marked transform ([Kol07, Definition 60, (60.1)]) along the lift of a local analytic isomorphism: for a marking m ≤ ν_Y(J) along the centre, ℓ^* (π)^{-1}_*(J, m) = (π')^{-1}_*(h^* J, m) — both are the unique ideal sheaves with the colon stalks, and the colon stalks correspond along the bijective germ map of ℓ (birationalTransform_pullback_of_comp_eq with the diffeomorphism replaced by the lift; the marking is legitimate for (h^* J, m) by the transport of the order along the centre).

theorem Hironaka.Manifold.reducedTransform_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (hs : Function.Surjective ⇑h) (E₀ : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY) ⋯ (AnalyticManifold.IdealSheaf.reducedTransform (Manifold.blowUpπ ψ hY) E₀ hY.idealSheaf) = AnalyticManifold.IdealSheaf.reducedTransform (Manifold.blowUpπ ψ ⋯) (Manifold.IdealSheaf.pullback ⇑h ⋯ E₀) ⋯.idealSheaf

The reduced transform of the boundary along the lift of a SURJECTIVE local analytic isomorphism: ℓ^* red(π⁻¹E ∪ π⁻¹Y) = red(π'⁻¹ h^*E ∪ π'⁻¹ h⁻¹Y) (reducedTransform_comap_of_surjective on the square π ∘ ℓ = h ∘ π').

theorem Hironaka.Manifold.weakTransform_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (J : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY) ⋯ (AnalyticManifold.IdealSheaf.weakTransform (Manifold.blowUpπ ψ hY) J hY.idealSheaf) = AnalyticManifold.IdealSheaf.weakTransform (Manifold.blowUpπ ψ ⋯) (Manifold.IdealSheaf.pullback ⇑h ⋯ J) ⋯.idealSheaf

Hironaka's weak transform (IdealSheaf.weakTransform) along the lift of a local analytic isomorphism: ℓ^* (π)_*^{-1} J = (π')_*^{-1} h^* J — both are the unique ideal sheaves with the colon stalks (π⁻¹J : I_F^ν), the exponent the generic order along the centre, which transports (genericOrdAlong_comap_of_isLocalDiffeomorph).

The reduced ideal sheaf of a pulled-back family

theorem Manifold.HypersurfaceFamily.idealSheaf_comap_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) (F : HypersurfaceFamily M.carrier) : (comap (⇑h) F).idealSheaf = IdealSheaf.pullback ⇑h ⋯ F.idealSheaf

Along a surjective local analytic isomorphism h, the reduced ideal sheaf of h⁻¹(E) is the pull-back of the reduced ideal sheaf of E — the vanishing stalks of the preimage are the images of the vanishing stalks under the bijective germ maps, and local generators descend along surjective local isomorphisms, so both branches of the if agree.