English
The determinant map on the space of continuous linear maps E → E is continuous (under appropriate finite-dimensional hypotheses).
Русский
Определитель на пространстве непрерывных линейных отображений непрерывен при соответствующих условиях конечной размерности.
LaTeX
$$$ f \mapsto \det f $ is continuous on $E \to E$$$
Lean4
theorem continuous_det : Continuous fun f : E →L[𝕜] E => f.det :=
by
change
Continuous fun f : E →L[𝕜] E =>
LinearMap.det
(f : E →ₗ[𝕜] E)
-- TODO: this could be easier with `det_cases`
by_cases h : ∃ s : Finset E, Nonempty (Basis (↥s) 𝕜 E)
· rcases h with ⟨s, ⟨b⟩⟩
haveI : FiniteDimensional 𝕜 E := FiniteDimensional.of_fintype_basis b
classical
simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]
refine Continuous.matrix_det ?_
exact ((LinearMap.toMatrix b b).toLinearMap.comp (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional
· rw [LinearMap.det]
simpa only [h, MonoidHom.one_apply, dif_neg, not_false_iff] using continuous_const
