feat(topology/algebra/matrix): the determinant is a continuous map (#…

…10503)

Formalized as part of the Sphere Eversion project.

src/linear_algebra/matrix/determinant.lean

@@ -86,10 +86,12 @@ end
 @[simp] lemma det_one : det (1 : matrix n n R) = 1 :=
 by rw [← diagonal_one]; simp [-diagonal_one]
 
-@[simp]
 lemma det_is_empty [is_empty n] {A : matrix n n R} : det A = 1 :=
 by simp [det_apply]
 
+@[simp] lemma coe_det_is_empty [is_empty n] : (det : matrix n n R → R) = function.const _ 1 :=
+by { ext, exact det_is_empty, }
+
 lemma det_eq_one_of_card_eq_zero {A : matrix n n R} (h : fintype.card n = 0) : det A = 1 :=
 begin
   haveI : is_empty n := fintype.card_eq_zero_iff.mp h,

src/topology/algebra/matrix.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2021 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import linear_algebra.determinant
+import topology.algebra.ring
+
+/-!
+# Topological properties of matrices
+
+This file is a place to collect topological results about matrices.
+
+## Main definitions:
+
+ * `continuous_det`: the determinant is continuous over a topological ring.
+-/
+
+open matrix
+
+variables {ι k : Type*} [topological_space k]
+
+instance : topological_space (matrix ι ι k) := Pi.topological_space
+
+variables [fintype ι] [decidable_eq ι] [comm_ring k] [topological_ring k]
+
+lemma continuous_det : continuous (det : matrix ι ι k → k) :=
+begin
+  suffices : ∀ (n : ℕ), continuous (λ A : matrix (fin n) (fin n) k, matrix.det A),
+  { have h : (det : matrix ι ι k → k) = det ∘ reindex (fintype.equiv_fin ι) (fintype.equiv_fin ι),
+    { ext, simp, },
+    rw h,
+    apply (this (fintype.card ι)).comp,
+    exact continuous_pi (λ i, continuous_pi (λ j, continuous_apply_apply _ _)), },
+  intros n,
+  induction n with n ih,
+  { simp_rw coe_det_is_empty,
+    exact continuous_const, },
+  simp_rw det_succ_column_zero,
+  refine continuous_finset_sum _ (λ l _, _),
+  refine (continuous_const.mul (continuous_apply_apply _ _)).mul (ih.comp _),
+  exact continuous_pi (λ i, continuous_pi (λ j, continuous_apply_apply _ _)),
+end

src/topology/constructions.lean

@@ -692,6 +692,12 @@ lemma continuous_apply [∀i, topological_space (π i)] (i : ι) :
   continuous (λp:Πi, π i, p i) :=
 continuous_infi_dom continuous_induced_dom
 
+@[continuity]
+lemma continuous_apply_apply {κ : Type*} {ρ : κ → ι → Type*}
+  [∀ j i, topological_space (ρ j i)] (j : κ) (i : ι) :
+  continuous (λ p : (Π j, Π i, ρ j i), p j i) :=
+(continuous_apply i).comp (continuous_apply j)
+
 lemma continuous_at_apply [∀i, topological_space (π i)] (i : ι) (x : Π i, π i) :
   continuous_at (λ p : Π i, π i, p i) x :=
 (continuous_apply i).continuous_at