Normalized determinants of loops of operators #
A continuous loop P of invertible complex-linear endomorphisms of a complex normed space has a
loop δ in the circle of normalized determinants, det (P t) = ‖det (P t)‖ δ t
(TauCeti.exists_path_det_eq_norm_mul). Its degree is the winding number of the loop of
determinants, the quantity that enters the product axiom of the Maslov index
(TauCeti.TotallyRealLoop.maslovIndex_map).
theorem
TauCeti.exists_path_det_eq_norm_mul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{P : ↑unitInterval → E →L[ℂ] E}
(hP : Continuous P)
(hP01 : P 0 = P 1)
(hdet : ∀ (t : ↑unitInterval), LinearMap.det ↑(P t) ≠ 0)
:
∃ (x : Circle) (δ : Path x x), ∀ (t : ↑unitInterval), LinearMap.det ↑(P t) = ↑‖LinearMap.det ↑(P t)‖ * ↑(δ t)
Every continuous loop P of invertible complex-linear endomorphisms has a circle loop δ of
normalized determinants, det (P t) = ‖det (P t)‖ δ t, as required by
TauCeti.TotallyRealLoop.maslovIndex_map.