The Jacobian determinant of an analytic map in charts; the Jacobian ideal

The Jacobian ideal of an analytic map, the ideal sheaf of the Jacobian clause of the principalization theorem — Bierstone–Milman's "the ideal generated (locally, with respect to any coordinate system) by the Jacobian determinant of σ" [BM97, Theorem 1.10, the sentence after it].

• jacobianFun f χ φ' is the Jacobian determinant of f : N → M read in a chart χ of the target and a chart φ' of the source: y ↦ det D(χ ∘ f ∘ φ'⁻¹)(φ' y), with Mathlib's ContinuousLinearMap.det — coordinate-free on the model space E, no basis is chosen.
• jacobianStalk f a' is the ideal of 𝒪_{N,a'} generated by the germs of analytic functions whose function germ (stalkToGerm) is the germ at a' of that Jacobian determinant in the standard charts chartAt E (f a'), chartAt E a'. When the Jacobian determinant is analytic near a' — which holds for every analytic f between analytic manifolds (Hironaka/Manifold/Jacobian/Analytic.lean) — this generating set is a single germ (stalkToGerm is injective); the definition itself needs no analyticity proof.
• AnalyticMap.jacobianIdeal f, for an analytic map of bundled analytic manifolds, is the ideal sheaf ofStalks of these stalks when they have local generators, and the unit ideal sheaf otherwise.

The dependence on the charts is only up to units (chain rule and multiplicativity of the determinant, the Jacobians of the chart changes being units: Hironaka/Manifold/Jacobian/Units.lean), so the Jacobian ideal is Bierstone–Milman's "with respect to any coordinate system".

noncomputable def Manifold.jacobianFun (𝕜 : Type) [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] {N : Type u} [TopologicalSpace N] (f : N → M) (χ : OpenPartialHomeomorph M E) (φ' : OpenPartialHomeomorph N E) (y : N) : 𝕜

The Jacobian determinant of f : N → M in the charts χ (target) and φ' (source) at y, det D(χ ∘ f ∘ φ'⁻¹)(φ' y) — the determinant (ContinuousLinearMap.det, coordinate-free on E) of the derivative of the chart representative of f ("the Jacobian determinant of σ", [BM97, Theorem 1.10, the sentence after it]). The scalar field is explicit, as in fderiv 𝕜.

Equations

• Manifold.jacobianFun 𝕜 f χ φ' y = (fderiv 𝕜 (↑χ ∘ f ∘ ↑φ'.symm) (↑φ' y)).det

noncomputable def Manifold.jacobianStalk {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] (f : N → M) (a' : N) : Ideal ↑((structureSheaf 𝕜 E N).presheaf.stalk a')

The stalk at a' of the Jacobian ideal of f: the ideal of 𝒪_{N,a'} generated by the germs whose function germ (stalkToGerm) is the germ at a' of the Jacobian determinant of f in the standard charts chartAt E (f a') and chartAt E a'. The generating set is the single germ of that analytic function when it is analytic near a' (which holds for every analytic f), and empty otherwise.

Equations

• Manifold.jacobianStalk f a' = Ideal.span (⇑(Manifold.stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ N a') ⁻¹' {↑(Manifold.jacobianFun 𝕜 f (chartAt E (f a')) (chartAt E a'))})

noncomputable def AnalyticMap.jacobianIdeal {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M) : M'.IdealSheaf

The ideal sheaf generated locally, in any analytic coordinates on source and target, by the Jacobian determinant of f [BM97, Theorem 1.10, the sentence after it] — independent of the coordinates, since a chart change multiplies the determinant by a unit: the ideal sheaf whose stalk at a' is generated by the germ of the Jacobian determinant of f in the standard charts chartAt (f a') and chartAt a' (Manifold.jacobianStalk), when these stalks have local generators (they do for every analytic f: the Jacobian determinant is analytic and its germ at a nearby point is a unit multiple of the germ in the charts at that point, Hironaka/Manifold/Jacobian/), and the unit ideal sheaf otherwise.

Equations

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