Determinants of continuous linear maps: relative determinants and the cofactor contraction

For continuous linear equivalences T U : M ≃L[R] N and a continuous linear map S : M →L[R] N, the determinants on M of T⁻¹ ∘ U, U⁻¹ ∘ S and T⁻¹ ∘ S satisfy det (T⁻¹ ∘ U) * det (U⁻¹ ∘ S) = det (T⁻¹ ∘ S), and for endomorphisms A of M and B of N, det (T⁻¹ ∘ B ∘ S ∘ A) = det B * det (T⁻¹ ∘ S) * det A. These relative determinants compare the volumes of the images of a fixed body under maps into N without choosing a volume on N.

For a continuous linear automorphism L of ι → R, write (L⁻¹)ⱼᵢ = L.symm (Pi.single i 1) j for the (j, i) entry of the matrix of L⁻¹, so that det L • L⁻¹ is the cofactor (adjugate) matrix of L. Contracting a family of continuous linear maps F' i precomposed with L against this matrix and taking the trace recovers det L times the trace of F':

∑ j, (det L • ∑ i, (L⁻¹)ⱼᵢ • F' i ∘ L) (Pi.single j 1) = det L • ∑ i, F' i (Pi.single i 1),

because ∑ j, (L⁻¹)ⱼᵢ • L (Pi.single j 1) = L (L⁻¹ (Pi.single i 1)) = Pi.single i 1. With F' i the derivative of the i-th component of a flux field, this is the pointwise Piola identity of the affine cofactor pullback, ContinuousLinearEquiv.sum_fderiv_affineFluxPullback.

Main declarations

• ContinuousLinearMap.det_id, ContinuousLinearMap.det_smul: the determinant of the identity and of a scalar multiple.
• ContinuousLinearMap.exists_le_norm_det_id_sub_smul: over ℝ or ℂ, the second-order lower bound 1 - δ re (trace H) - P δ² ≤ ‖det (1 - δ H)‖ for 0 ≤ δ ≤ 1.
• ContinuousLinearEquiv.det_symm_comp_mul_det_symm_comp: relative determinants multiply.
• ContinuousLinearEquiv.det_symm_comp_comp_comp: composing with endomorphisms on either side multiplies the relative determinant by their determinants.
• ContinuousLinearEquiv.sum_cofactor_comp_apply_single: the cofactor contraction identity.

@[simp]

theorem ContinuousLinearMap.det_id {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] : (ContinuousLinearMap.id R M).det = 1

The identity has determinant one.

@[simp]

theorem ContinuousLinearMap.det_smul {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousConstSMul R M] [Module.Free R M] (c : R) (f : M →L[R] M) : (c • f).det = c ^ Module.finrank R M * f.det

Multiplying a map by a scalar c multiplies its determinant by c ^ finrank R M.

theorem ContinuousLinearMap.exists_le_norm_det_id_sub_smul {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [FiniteDimensional 𝕜 E] (H : E →L[𝕜] E) : ∃ (P : ℝ), ∀ δ ∈ Set.Icc 0 1, 1 - δ * RCLike.re ((LinearMap.trace 𝕜 E) ↑H) - P * δ ^ 2 ≤ ‖(ContinuousLinearMap.id 𝕜 E - ↑δ • H).det‖

A second-order lower bound for ‖det (1 - δ H)‖ on 0 ≤ δ ≤ 1, from the expansion det (1 + r M) = 1 + r trace M + O(r²) of Matrix.det_one_add_smul.

theorem ContinuousLinearEquiv.det_symm_comp_mul_det_symm_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalSpace N] [AddCommGroup N] [Module R N] (T U : M ≃L[R] N) (S : M →L[R] N) : (↑T.symm ∘SL ↑U).det * (↑U.symm ∘SL S).det = (↑T.symm ∘SL S).det

Determinants relative to equivalences M ≃L[R] N multiply: comparing S with T is comparing U with T and then S with U.

theorem ContinuousLinearEquiv.det_symm_comp_comp_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalSpace N] [AddCommGroup N] [Module R N] (T : M ≃L[R] N) (B : N →L[R] N) (S : M →L[R] N) (A : M →L[R] M) : (↑T.symm ∘SL B ∘SL S ∘SL A).det = B.det * (↑T.symm ∘SL S).det * A.det

The determinant of S : M → N relative to T : M ≃L[R] N is multiplicative under composition with endomorphisms on either side: for A : M →L[R] M and B : N →L[R] N, the determinant of B ∘ S ∘ A relative to T is det B * det (T⁻¹ ∘ S) * det A.

theorem ContinuousLinearEquiv.sum_cofactor_comp_apply_single {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (L : (ι → R) ≃L[R] ι → R) (F' : ι → (ι → R) →L[R] M) : ∑ j : ι, (LinearMap.det ↑↑L • ∑ i : ι, L.symm (Pi.single i 1) j • F' i ∘SL ↑L) (Pi.single j 1) = LinearMap.det ↑↑L • ∑ i : ι, (F' i) (Pi.single i 1)

The cofactor contraction identity: the trace of the cofactor transform det L • ∑ i, (L⁻¹)ⱼᵢ • (F' i ∘ L) of a family F' of continuous linear maps is det L times the trace ∑ i, F' i (Pi.single i 1), as ∑ j, (L⁻¹)ⱼᵢ • L (Pi.single j 1) = L (L⁻¹ (Pi.single i 1)) = Pi.single i 1.