The determinant of continuous linear maps is analytic; the Jacobian determinant of an analytic map

Calculus shared by the analytic strands: the determinant is a polynomial on E →L[𝕜] E (contDiff_det), so x ↦ det (DF x) is C^ω on an open set on which F is C^ω (contDiffOn_det_fderiv) and analytic on an open set on which F is analytic (analyticOnNhd_det_fderiv, through AnalyticOnNhd.contDiffOn_of_completeSpace, ContDiffOn.analyticOn and IsOpen.analyticOn_iff_analyticOnNhd). Multiplicativity of the determinant of continuous linear maps (det_clm_comp) sits beside them. Not in the sources as such: it is what makes the Jacobian of a blowing-up an analytic function and its zero set a divisor, as in the remark after [BM97, Theorem 1.10] ("if J ⊆ 𝒪_{M_k} denotes the ideal generated by the Jacobian determinant of π, then J · π⁻¹(I) is a normal-crossings divisor"). Used by the Jacobian computations of the analytic manifolds (Hironaka/Manifold/Jacobian).

theorem Analytic.det_clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (A B : E →L[𝕜] E) : (A ∘SL B).det = A.det * B.det

The determinant of a composite of continuous linear maps is the product of the determinants (Mathlib's LinearMap.det_comp through the coercion E →L[𝕜] E → E →ₗ[𝕜] E).

theorem Analytic.contDiff_det {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {n : WithTop ℕ∞} : ContDiff 𝕜 n fun (L : E →L[𝕜] E) => L.det

The determinant is analytic on E →L[𝕜] E. With a finite basis b, det L = det (toMatrix b b L) is a polynomial (Leibniz's formula) in the entries b.repr (L (b j)) i, continuous linear functions of L; without one, det = 1.

theorem Analytic.contDiffOn_det_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] {F : E → E} {s : Set E} (hF : ContDiffOn 𝕜 ⊤ F s) (hs : IsOpen s) : ContDiffOn 𝕜 ⊤ (fun (x : E) => (fderiv 𝕜 F x).det) s

x ↦ det (DF x) is C^ω on an open set on which F is C^ω (ContDiffOn.fderiv_of_isOpen with ω + 1 = ω, then contDiff_det).

theorem Analytic.analyticOnNhd_det_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] [CompleteSpace E] {F : E → E} {V : Set E} (hV : IsOpen V) (hF : AnalyticOnNhd 𝕜 F V) : AnalyticOnNhd 𝕜 (fun (x : E) => (fderiv 𝕜 F x).det) V

The Jacobian determinant of an analytic map is analytic on an open set: analytic is C^ω (AnalyticOnNhd.contDiffOn_of_completeSpace), C^ω on an open set is analytic (ContDiffOn.analyticOn, IsOpen.analyticOn_iff_analyticOnNhd).