The normalized determinant of a complex-linear automorphism

The determinant of a complex-linear automorphism A is a nonzero complex number, so it is ‖det A‖ times the point det A / ‖det A‖ of the unit circle (ContinuousLinearEquiv.normalizedDet). The normalized determinant depends continuously on A, so a loop of automorphisms gives a loop on the circle; its degree is the winding number of the loop of determinants.

Main declarations

• ContinuousLinearEquiv.normalizedDet: the point det A / ‖det A‖ of the circle.
• ContinuousLinearEquiv.det_eq_norm_mul_normalizedDet: det A = ‖det A‖ * normalizedDet A.
• Continuous.normalizedDet: a continuous family of automorphisms has continuous normalized determinant.

noncomputable def ContinuousLinearEquiv.normalizedDet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E ≃L[ℂ] E) : Circle

The normalized determinant det A / ‖det A‖ of a complex-linear automorphism, a point of the circle.

@[simp]

theorem ContinuousLinearEquiv.coe_normalizedDet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E ≃L[ℂ] E) : ↑A.normalizedDet = LinearMap.det ↑↑A / ↑‖LinearMap.det ↑↑A‖

The normalized determinant, as a complex number.

theorem ContinuousLinearEquiv.det_eq_norm_mul_normalizedDet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E ≃L[ℂ] E) : LinearMap.det ↑↑A = ↑‖LinearMap.det ↑↑A‖ * ↑A.normalizedDet

The determinant of an automorphism is its modulus times its normalized determinant.

theorem Continuous.normalizedDet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {A : X → E ≃L[ℂ] E} (hA : Continuous fun (x : X) => ↑(A x)) : Continuous fun (x : X) => (A x).normalizedDet

A continuous family of complex-linear automorphisms has a continuous family of normalized determinants.