The Jacobian ideal on bundled manifolds

AnalyticMap.jacobianIdeal f (the ideal sheaf of the Jacobian clause of the principalization theorem [BM97, Theorem 1.10, the sentence after it]) is the ideal sheaf ofStalks of the stalks jacobianStalk f when these have local generators, and the unit ideal sheaf otherwise. This module reads the two branches (jacobianIdeal_eq_of_hasLocalGenerators, jacobianIdeal_eq_top_of_not), notes that the first branch is always the one taken (hasLocalGenerators_jacobianStalk), so that the stalks of the Jacobian ideal are the jacobianStalks (jacobianIdeal_stalkIdeal), and identifies the Jacobian ideal of the blowing-up along a closed submanifold of codimension c with the (c − 1)-st power of the exceptional ideal sheaf I_F = π^*(𝓘_Y) (jacobianIdeal_blowUp_eq_pow; at the stalks, jacobianIdeal_blowUp_stalkIdeal): at a point p with π p ∈ Y, an adapted chart at π p and a blow-up chart through p (IsBlowUp.cover) give both stalks as (u_{σ i}^{c-1}) (jacobianStalk_blowUp, stalkIdeal_exceptionalIdealSheaf_eq_span_coord with Ideal.span_singleton_pow); off π⁻¹(Y) both stalks are the unit ideal — I_F's by stalkIdeal_exceptionalIdealSheaf_of_notMem, the Jacobian's because the blowing-up is a local diffeomorphism there (IsBlowUp.isLocalDiffeomorphOn_compl, jacobianStalk_eq_top_of_isLocalDiffeomorphAt). This last case is the whole of the identity when c = 0 or Y = ∅ (then no blow-up chart exists), and the exponent c − 1 = 0 gives the unit ideal sheaf on both sides for c ≤ 1. The identity is the input of the Jacobian clause along a sequence of blow-ups (Hironaka/Resolution/Analytic/Principalization/JacobianMonomial.lean).

theorem Manifold.jacobianIdeal_eq_of_hasLocalGenerators {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (h : IdealSheaf.HasLocalGenerators (jacobianStalk ⇑f)) : f.jacobianIdeal = IdealSheaf.ofStalks (structureSheaf 𝕜 E N'.carrier) (jacobianStalk ⇑f) h

The first branch of AnalyticMap.jacobianIdeal: when the stalks of the Jacobian ideal have local generators, the Jacobian ideal is the ideal sheaf with those stalks.

theorem Manifold.jacobianIdeal_eq_top_of_not {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (h : ¬IdealSheaf.HasLocalGenerators (jacobianStalk ⇑f)) : f.jacobianIdeal = ⊤

The second branch of AnalyticMap.jacobianIdeal (never taken: hasLocalGenerators_jacobianStalk).

theorem Manifold.jacobianIdeal_stalkIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (a' : N'.carrier) : IdealSheaf.stalkIdeal f.jacobianIdeal a' = jacobianStalk (⇑f) a'

The stalks of the Jacobian ideal are the ideals generated by the germ of the Jacobian determinant of f in the standard charts ([BM97, Theorem 1.10, the sentence after it]).

theorem Manifold.jacobianIdeal_blowUp_stalkIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N N' : AnalyticManifold 𝕜 E} (π : AnalyticMap N' N) {Y : Set N.carrier} {c : ℕ} (h : IsBlowUp ψ Y c ⇑π) {φ : OpenPartialHomeomorph N.carrier E} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) {i : Fin c} {Φ : OpenPartialHomeomorph N'.carrier E} (hΦ : IsBlowUpChart ψ (⇑π) φ σ i Φ) {p : N'.carrier} (hp : p ∈ Φ.source) : IdealSheaf.stalkIdeal π.jacobianIdeal p = Ideal.span {coord E ψ Φ ⋯ hp (σ i) ^ (c - 1)}

For the blowing-up, at the stalks: in a blow-up chart of index i the stalk of the Jacobian ideal is (u_{σ i}^{c-1}).

theorem Manifold.jacobianIdeal_blowUp_eq_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N N' : AnalyticManifold 𝕜 E} (π : AnalyticMap N' N) {Y : Set N.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c ⇑π) : π.jacobianIdeal = IdealSheaf.pullback ⇑π ⋯ hY.idealSheaf ^ (c - 1)

The Jacobian ideal of the blowing-up of N along a closed submanifold Y of codimension c is the (c − 1)-st power of the exceptional ideal sheaf I_F = π^*(𝓘_Y) (the chart formulas of [BM88, Definition 4.1]; the Jacobian ideal of [BM97, Theorem 1.10, the sentence after it]). Stalk by stalk: through a blow-up chart at points over Y, and off π⁻¹(Y) both sides are the unit ideal, the blowing-up being a local diffeomorphism there.