Chart independence of the Jacobian determinant up to units

Bierstone–Milman's Jacobian ideal is "the ideal generated (locally, with respect to any coordinate system) by the Jacobian determinant" [BM97, Theorem 1.10, the sentence after it]: the Jacobian determinant of an analytic map f in two chart pairs differs by an analytic unit, so the ideal it generates in 𝒪_{M',a'} does not depend on the charts, and the stalks of the Jacobian ideal have local generators.

• The chain rule (fderiv_chartRep_eq): for chart pairs (χ, φ'), (χ', φ'') at a', χ' ∘ f ∘ φ''⁻¹ = (χ' ∘ χ⁻¹) ∘ (χ ∘ f ∘ φ'⁻¹) ∘ (φ' ∘ φ''⁻¹) near φ''(a'), so D(χ' ∘ f ∘ φ''⁻¹)(φ'' y) = D(χ' ∘ χ⁻¹)(χ(f y)) ∘ D(χ ∘ f ∘ φ'⁻¹)(φ' y) ∘ D(φ' ∘ φ''⁻¹)(φ'' y) (fderiv_comp twice, the two chart changes being analytic by contDiffOn_chartChange).
• Multiplicativity of the determinant gives J_{χ',φ''} = a · J_{χ,φ'} · b with a = det D(χ' ∘ χ⁻¹) ∘ χ ∘ f and b = det D(φ' ∘ φ''⁻¹) ∘ φ'' analytic near a' (Hironaka/Manifold/Jacobian/Analytic.lean), and nonvanishing at a': each chart change has the inverse chart change as a two-sided inverse, so det (Dg'(g x)) · det (Dg x) = 1 (det_fderiv_mul_det_fderiv_eq_one). A germ of 𝒪_{M',a'} is a unit iff its value at a' is nonzero (isUnit_stalk_iff), so the germ of a · b is the unit u of exists_unit_jacobianFun_germ_eq.
• Consequences. The stalk jacobianStalk f a' — the ideal generated by the germs whose function germ is the Jacobian determinant in the standard charts — is generated by one germ (exists_stalk_jacobianStalk_eq_span: the determinant is analytic, so its germ is the function germ of a section, and stalkToGerm is injective), by the determinant in any chart pair (exists_stalk_jacobianStalk_eq_span_of_charts: the unit u does not change the ideal, Ideal.span_singleton_mul_left_unit), and the stalks have local generators (hasLocalGenerators_jacobianStalk: near a' the single section det D(χ ∘ f ∘ φ'⁻¹) ∘ φ' for the standard charts χ, φ' at a' generates every stalk, by the any-chart form) — so the first branch of AnalyticMap.jacobianIdeal is always the one taken.
• Local diffeomorphisms. Where f is a local diffeomorphism its Jacobian determinant is a unit (isUnit_jacobianFun_of_isLocalDiffeomorphAt: the chart representative of Mathlib's localInverse is a left inverse of the chart representative of f) and the stalk of the Jacobian ideal is the unit ideal (jacobianStalk_eq_top_of_isLocalDiffeomorphAt) — the case of an isomorphism in the principalization theorem, and the off-centre case of the blowing-up (Hironaka/Manifold/Jacobian/BlowUp.lean).

@[reducible, inline]

abbrev Manifold.chartPairDomain {E : Type u_1} [NormedAddCommGroup E] {M : Type u} [TopologicalSpace M] {N : Type u} [TopologicalSpace N] (f : N → M) (χ χ' : OpenPartialHomeomorph M E) (φ' φ'' : OpenPartialHomeomorph N E) : Set N

The common domain of two chart pairs: φ'.source ∩ φ''.source ∩ f⁻¹(χ.source ∩ χ'.source).

Equations

• Manifold.chartPairDomain f χ χ' φ' φ'' = φ'.source ∩ φ''.source ∩ f ⁻¹' (χ.source ∩ χ'.source)

theorem Manifold.isOpen_chartPairDomain {𝕜 : Type} [RCLike 𝕜] {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} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) (χ χ' : OpenPartialHomeomorph M E) (φ' φ'' : OpenPartialHomeomorph N E) : IsOpen (chartPairDomain f χ χ' φ' φ'')

theorem Manifold.differentiableAt_chartChange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {χ χ' : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hχ' : χ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {x : M} (hx : x ∈ χ.source) (hx' : x ∈ χ'.source) : DifferentiableAt 𝕜 (↑χ' ∘ ↑χ.symm) (↑χ x)

A chart change χ' ∘ χ⁻¹ is differentiable at the image χ x of a point x of χ.source ∩ χ'.source.

theorem Manifold.differentiableAt_chartRep {𝕜 : Type} [RCLike 𝕜] {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} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {χ : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {φ' : OpenPartialHomeomorph N E} (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) {y : N} (hy : y ∈ φ'.source) (hfy : f y ∈ χ.source) : DifferentiableAt 𝕜 (↑χ ∘ f ∘ ↑φ'.symm) (↑φ' y)

The chart representative χ ∘ f ∘ φ'⁻¹ is differentiable at φ' y for y in φ'.source ∩ f⁻¹(χ.source).

theorem Manifold.fderiv_chartRep_eq {𝕜 : Type} [RCLike 𝕜] {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} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {χ χ' : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hχ' : χ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {φ' φ'' : OpenPartialHomeomorph N E} (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) (hφ'' : φ'' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) {y : N} (hy : y ∈ chartPairDomain f χ χ' φ' φ'') : fderiv 𝕜 (↑χ' ∘ f ∘ ↑φ''.symm) (↑φ'' y) = fderiv 𝕜 (↑χ' ∘ ↑χ.symm) (↑χ (f y)) ∘SL fderiv 𝕜 (↑χ ∘ f ∘ ↑φ'.symm) (↑φ' y) ∘SL fderiv 𝕜 (↑φ' ∘ ↑φ''.symm) (↑φ'' y)

The chain rule for the chart representatives: on the common domain, D(χ' ∘ f ∘ φ''⁻¹)(φ'' y) = D(χ' ∘ χ⁻¹)(χ (f y)) ∘ D(χ ∘ f ∘ φ'⁻¹)(φ' y) ∘ D(φ' ∘ φ''⁻¹)(φ'' y).

theorem Manifold.jacobianFun_eq_mul {𝕜 : Type} [RCLike 𝕜] {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} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {χ χ' : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hχ' : χ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {φ' φ'' : OpenPartialHomeomorph N E} (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) (hφ'' : φ'' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) {y : N} (hy : y ∈ chartPairDomain f χ χ' φ' φ'') : jacobianFun 𝕜 f χ' φ'' y = (fderiv 𝕜 (↑χ' ∘ ↑χ.symm) (↑χ (f y))).det * (jacobianFun 𝕜 f χ φ' y * (fderiv 𝕜 (↑φ' ∘ ↑φ''.symm) (↑φ'' y)).det)

The Jacobian determinants in two chart pairs differ by the Jacobians of the two chart changes: on the common domain, J_{χ',φ''}(y) = det D(χ' ∘ χ⁻¹)(χ(f y)) · J_{χ,φ'}(y) · det D(φ' ∘ φ''⁻¹)(φ'' y).

theorem Manifold.det_fderiv_chartChange_ne_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {χ χ' : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hχ' : χ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {x : M} (hx : x ∈ χ.source) (hx' : x ∈ χ'.source) : (fderiv 𝕜 (↑χ' ∘ ↑χ.symm) (↑χ x)).det ≠ 0

The Jacobian of a chart change is nonzero at the image of a point of both charts: the inverse chart change is a two-sided inverse, and det (Dg'(g x)) · det (Dg x) = 1.

noncomputable def Manifold.jacobianGerm {𝕜 : Type} [RCLike 𝕜] {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} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {χ : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {φ' : OpenPartialHomeomorph N E} (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) {a' : N} (ha' : a' ∈ φ'.source) (hfa' : f a' ∈ χ.source) : ↑((structureSheaf 𝕜 E N).presheaf.stalk a')

The stalk element with function germ the Jacobian determinant J_{χ,φ'} at a point of φ'.source ∩ f⁻¹(χ.source): the germ of the section J_{χ,φ'} over that open set.

Equations

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

theorem Manifold.stalkToGerm_jacobianGerm {𝕜 : Type} [RCLike 𝕜] {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} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {χ : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {φ' : OpenPartialHomeomorph N E} (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) {a' : N} (ha' : a' ∈ φ'.source) (hfa' : f a' ∈ χ.source) : (stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ N a') (jacobianGerm hf hχ hφ' ha' hfa') = ↑(jacobianFun 𝕜 f χ φ')

theorem Manifold.exists_unit_jacobianFun_germ_eq {𝕜 : Type} [RCLike 𝕜] {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} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {χ χ' : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hχ' : χ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {φ' φ'' : OpenPartialHomeomorph N E} (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) (hφ'' : φ'' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) {a' : N} (ha' : a' ∈ φ'.source) (ha'' : a' ∈ φ''.source) (hfa' : f a' ∈ χ.source) (hfa'' : f a' ∈ χ'.source) : ∃ (u : ↑((structureSheaf 𝕜 E N).presheaf.stalk a')), IsUnit u ∧ ↑(jacobianFun 𝕜 f χ' φ'') = (stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ N a') u * ↑(jacobianFun 𝕜 f χ φ')

The Jacobian determinants of f in two chart pairs at a' differ by an analytic unit (chain rule and multiplicativity of the determinant; "with respect to any coordinate system", [BM97, Theorem 1.10, the sentence after it]) — the product of the Jacobians of the two chart changes.

theorem Manifold.exists_stalk_jacobianStalk_eq_span {𝕜 : Type} [RCLike 𝕜] {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} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) (a' : N) : ∃ (s : ↑((structureSheaf 𝕜 E N).presheaf.stalk a')), (stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ N a') s = ↑(jacobianFun 𝕜 f (chartAt E (f a')) (chartAt E a')) ∧ jacobianStalk f a' = Ideal.span {s}

The stalk of the Jacobian ideal at a' is generated by a single germ, the germ of the Jacobian determinant in the standard charts (stalkToGerm is injective, so the generating set of jacobianStalk is that one germ).

theorem Manifold.exists_stalk_jacobianStalk_eq_span_of_charts {𝕜 : Type} [RCLike 𝕜] {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} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {χ : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {φ' : OpenPartialHomeomorph N E} (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) {a' : N} (ha' : a' ∈ φ'.source) (hfa' : f a' ∈ χ.source) : ∃ (s : ↑((structureSheaf 𝕜 E N).presheaf.stalk a')), (stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ N a') s = ↑(jacobianFun 𝕜 f χ φ') ∧ jacobianStalk f a' = Ideal.span {s}

The stalk of the Jacobian ideal at a' is generated by the germ of the Jacobian determinant in any chart pair at a' ("with respect to any coordinate system", [BM97, Theorem 1.10, the sentence after it]) — that germ is a unit times the standard one.

theorem Manifold.hasLocalGenerators_jacobianStalk {𝕜 : Type} [RCLike 𝕜] {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} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) : IdealSheaf.HasLocalGenerators (jacobianStalk f)

The stalks of the Jacobian ideal of an analytic map have local generators: near a', the single section J_{χ,φ'} for the standard charts χ, φ' at a' generates every stalk, by the any-chart form. This is the condition under which AnalyticMap.jacobianIdeal is the ideal sheaf with these stalks.

theorem Manifold.isUnit_jacobianFun_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {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} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {a' : N} (hloc : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f a') {χ : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {φ' : OpenPartialHomeomorph N E} (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) (ha' : a' ∈ φ'.source) (hfa' : f a' ∈ χ.source) : IsUnit (jacobianFun 𝕜 f χ φ' a')

Where f is a local diffeomorphism its Jacobian determinant is a unit: the chart representative φ' ∘ f⁻¹ ∘ χ⁻¹ of Mathlib's local inverse is a left inverse of χ ∘ f ∘ φ'⁻¹ near φ' a', so det D(χ ∘ f ∘ φ'⁻¹)(φ' a') ≠ 0.

theorem Manifold.jacobianStalk_eq_top_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {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} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {a' : N} (hloc : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f a') : jacobianStalk f a' = ⊤

Where f is a local diffeomorphism the stalk of the Jacobian ideal is the unit ideal (the case of an isomorphism in the principalization theorem, whose Jacobian ideal is the unit ideal; the off-centre case of the blowing-up).