src/topology/instances/matrix.lean

/-
Copyright (c) 2021 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash, Eric Wieser
-/
import topology.algebra.infinite_sum.basic
import topology.algebra.ring.basic
import topology.algebra.star
import linear_algebra.matrix.nonsingular_inverse
import linear_algebra.matrix.trace

/-!
# Topological properties of matrices

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

This file is a place to collect topological results about matrices.

## Main definitions:

* `matrix.topological_ring`: square matrices form a topological ring

## Main results

* Continuity:
  * `continuous.matrix_det`: the determinant is continuous over a topological ring.
  * `continuous.matrix_adjugate`: the adjugate is continuous over a topological ring.
* Infinite sums
  * `matrix.transpose_tsum`: transpose commutes with infinite sums
  * `matrix.diagonal_tsum`: diagonal commutes with infinite sums
  * `matrix.block_diagonal_tsum`: block diagonal commutes with infinite sums
  * `matrix.block_diagonal'_tsum`: non-uniform block diagonal commutes with infinite sums
-/

open matrix
open_locale matrix

variables {X α l m n p S R : Type*} {m' n' : l → Type*}

instance [topological_space R] : topological_space (matrix m n R) := Pi.topological_space

instance [topological_space R] [t2_space R] : t2_space (matrix m n R) := Pi.t2_space

/-! ### Lemmas about continuity of operations -/
section continuity
variables [topological_space X] [topological_space R]

instance [has_smul α R] [has_continuous_const_smul α R] :
  has_continuous_const_smul α (matrix m n R) :=
pi.has_continuous_const_smul

instance [topological_space α] [has_smul α R] [has_continuous_smul α R] :
  has_continuous_smul α (matrix m n R) :=
pi.has_continuous_smul

instance [has_add R] [has_continuous_add R] : has_continuous_add (matrix m n R) :=
pi.has_continuous_add

instance [has_neg R] [has_continuous_neg R] : has_continuous_neg (matrix m n R) :=
pi.has_continuous_neg

instance [add_group R] [topological_add_group R] : topological_add_group (matrix m n R) :=
pi.topological_add_group

/-- To show a function into matrices is continuous it suffices to show the coefficients of the
resulting matrix are continuous -/
@[continuity]
lemma continuous_matrix [topological_space α] {f : α → matrix m n R}
  (h : ∀ i j, continuous (λ a, f a i j)) : continuous f :=
continuous_pi $ λ _, continuous_pi $ λ j, h _ _

lemma continuous.matrix_elem {A : X → matrix m n R} (hA : continuous A) (i : m) (j : n) :
  continuous (λ x, A x i j) :=
(continuous_apply_apply i j).comp hA

@[continuity]
lemma continuous.matrix_map [topological_space S] {A : X → matrix m n S} {f : S → R}
   (hA : continuous A) (hf : continuous f) :
  continuous (λ x, (A x).map f) :=
continuous_matrix $ λ i j, hf.comp $ hA.matrix_elem _ _

@[continuity]
lemma continuous.matrix_transpose {A : X → matrix m n R} (hA : continuous A) :
  continuous (λ x, (A x)ᵀ) :=
continuous_matrix $ λ i j, hA.matrix_elem j i

lemma continuous.matrix_conj_transpose [has_star R] [has_continuous_star R] {A : X → matrix m n R}
  (hA : continuous A) : continuous (λ x, (A x)ᴴ) :=
hA.matrix_transpose.matrix_map continuous_star

instance [has_star R] [has_continuous_star R] : has_continuous_star (matrix m m R) :=
⟨continuous_id.matrix_conj_transpose⟩

@[continuity]
lemma continuous.matrix_col {A : X → n → R} (hA : continuous A) : continuous (λ x, col (A x)) :=
continuous_matrix $ λ i j, (continuous_apply _).comp hA

@[continuity]
lemma continuous.matrix_row {A : X → n → R} (hA : continuous A) : continuous (λ x, row (A x)) :=
continuous_matrix $ λ i j, (continuous_apply _).comp hA

@[continuity]
lemma continuous.matrix_diagonal [has_zero R] [decidable_eq n] {A : X → n → R} (hA : continuous A) :
  continuous (λ x, diagonal (A x)) :=
continuous_matrix $ λ i j, ((continuous_apply i).comp hA).if_const _ continuous_zero

@[continuity]
lemma continuous.matrix_dot_product [fintype n] [has_mul R] [add_comm_monoid R]
  [has_continuous_add R] [has_continuous_mul R]
  {A : X → n → R} {B : X → n → R} (hA : continuous A) (hB : continuous B) :
  continuous (λ x, dot_product (A x) (B x)) :=
continuous_finset_sum _ $ λ i _, ((continuous_apply i).comp hA).mul ((continuous_apply i).comp hB)

/-- For square matrices the usual `continuous_mul` can be used. -/
@[continuity]
lemma continuous.matrix_mul [fintype n] [has_mul R] [add_comm_monoid R] [has_continuous_add R]
  [has_continuous_mul R]
  {A : X → matrix m n R} {B : X → matrix n p R} (hA : continuous A) (hB : continuous B) :
  continuous (λ x, (A x).mul (B x)) :=
continuous_matrix $ λ i j, continuous_finset_sum _ $ λ k _,
  (hA.matrix_elem _ _).mul (hB.matrix_elem _ _)

instance [fintype n] [has_mul R] [add_comm_monoid R] [has_continuous_add R]
  [has_continuous_mul R] : has_continuous_mul (matrix n n R) :=
⟨continuous_fst.matrix_mul continuous_snd⟩

instance [fintype n] [non_unital_non_assoc_semiring R] [topological_semiring R] :
  topological_semiring (matrix n n R) :=
{}

instance [fintype n] [non_unital_non_assoc_ring R] [topological_ring R] :
  topological_ring (matrix n n R) :=
{}

@[continuity]
lemma continuous.matrix_vec_mul_vec [has_mul R] [has_continuous_mul R]
  {A : X → m → R} {B : X → n → R} (hA : continuous A) (hB : continuous B) :
  continuous (λ x, vec_mul_vec (A x) (B x)) :=
continuous_matrix $ λ i j, ((continuous_apply _).comp hA).mul ((continuous_apply _).comp hB)

@[continuity]
lemma continuous.matrix_mul_vec [non_unital_non_assoc_semiring R] [has_continuous_add R]
  [has_continuous_mul R] [fintype n]
  {A : X → matrix m n R} {B : X → n → R} (hA : continuous A) (hB : continuous B) :
  continuous (λ x, (A x).mul_vec (B x)) :=
continuous_pi $ λ i, ((continuous_apply i).comp hA).matrix_dot_product hB

@[continuity]
lemma continuous.matrix_vec_mul [non_unital_non_assoc_semiring R] [has_continuous_add R]
  [has_continuous_mul R] [fintype m]
  {A : X → m → R} {B : X → matrix m n R} (hA : continuous A) (hB : continuous B) :
  continuous (λ x, vec_mul (A x) (B x)) :=
continuous_pi $ λ i, hA.matrix_dot_product $ continuous_pi $ λ j, hB.matrix_elem _ _

@[continuity]
lemma continuous.matrix_submatrix
  {A : X → matrix l n R} (hA : continuous A) (e₁ : m → l) (e₂ : p → n) :
  continuous (λ x, (A x).submatrix e₁ e₂) :=
continuous_matrix $ λ i j, hA.matrix_elem _ _

@[continuity]
lemma continuous.matrix_reindex {A : X → matrix l n R}
  (hA : continuous A) (e₁ : l ≃ m) (e₂ : n ≃ p) :
  continuous (λ x, reindex e₁ e₂ (A x)) :=
hA.matrix_submatrix _ _

@[continuity]
lemma continuous.matrix_diag {A : X → matrix n n R} (hA : continuous A) :
  continuous (λ x, matrix.diag (A x)) :=
continuous_pi $ λ _, hA.matrix_elem _ _

-- note this doesn't elaborate well from the above
lemma continuous_matrix_diag : continuous (matrix.diag : matrix n n R → n → R) :=
show continuous (λ x : matrix n n R, matrix.diag x), from continuous_id.matrix_diag

@[continuity]
lemma continuous.matrix_trace [fintype n] [add_comm_monoid R] [has_continuous_add R]
  {A : X → matrix n n R} (hA : continuous A) :
  continuous (λ x, trace (A x)) :=
continuous_finset_sum _ $ λ i hi, hA.matrix_elem _ _

@[continuity]
lemma continuous.matrix_det [fintype n] [decidable_eq n] [comm_ring R] [topological_ring R]
  {A : X → matrix n n R} (hA : continuous A) :
  continuous (λ x, (A x).det) :=
begin
  simp_rw matrix.det_apply,
  refine continuous_finset_sum _ (λ l _, continuous.const_smul _ _),
  refine continuous_finset_prod _ (λ l _, hA.matrix_elem _ _),
end

@[continuity]
lemma continuous.matrix_update_column [decidable_eq n] (i : n)
  {A : X → matrix m n R} {B : X → m → R} (hA : continuous A) (hB : continuous B) :
  continuous (λ x, (A x).update_column i (B x)) :=
continuous_matrix $ λ j k, (continuous_apply k).comp $
  ((continuous_apply _).comp hA).update i ((continuous_apply _).comp hB)

@[continuity]
lemma continuous.matrix_update_row [decidable_eq m] (i : m)
  {A : X → matrix m n R} {B : X → n → R} (hA : continuous A) (hB : continuous B) :
  continuous (λ x, (A x).update_row i (B x)) :=
hA.update i hB

@[continuity]
lemma continuous.matrix_cramer [fintype n] [decidable_eq n] [comm_ring R] [topological_ring R]
  {A : X → matrix n n R} {B : X → n → R} (hA : continuous A) (hB : continuous B) :
  continuous (λ x, (A x).cramer (B x)) :=
continuous_pi $ λ i, (hA.matrix_update_column _ hB).matrix_det

@[continuity]
lemma continuous.matrix_adjugate [fintype n] [decidable_eq n] [comm_ring R] [topological_ring R]
  {A : X → matrix n n R} (hA : continuous A) :
  continuous (λ x, (A x).adjugate) :=
continuous_matrix $ λ j k, (hA.matrix_transpose.matrix_update_column k continuous_const).matrix_det

/-- When `ring.inverse` is continuous at the determinant (such as in a `normed_ring`, or a
`topological_field`), so is `matrix.has_inv`. -/
lemma continuous_at_matrix_inv [fintype n] [decidable_eq n] [comm_ring R] [topological_ring R]
  (A : matrix n n R) (h : continuous_at ring.inverse A.det) :
  continuous_at has_inv.inv A :=
(h.comp continuous_id.matrix_det.continuous_at).smul continuous_id.matrix_adjugate.continuous_at

-- lemmas about functions in `data/matrix/block.lean`
section block_matrices

@[continuity]
lemma continuous.matrix_from_blocks
  {A : X → matrix n l R} {B : X → matrix n m R} {C : X → matrix p l R} {D : X → matrix p m R}
  (hA : continuous A) (hB : continuous B) (hC : continuous C) (hD : continuous D) :
  continuous (λ x, matrix.from_blocks (A x) (B x) (C x) (D x)) :=
continuous_matrix $ λ i j,
  by cases i; cases j; refine continuous.matrix_elem _ i j; assumption

@[continuity]
lemma continuous.matrix_block_diagonal [has_zero R] [decidable_eq p] {A : X → p → matrix m n R}
  (hA : continuous A) :
  continuous (λ x, block_diagonal (A x)) :=
continuous_matrix $ λ ⟨i₁, i₂⟩ ⟨j₁, j₂⟩,
  (((continuous_apply i₂).comp hA).matrix_elem i₁ j₁).if_const _ continuous_zero

@[continuity]
lemma continuous.matrix_block_diag {A : X → matrix (m × p) (n × p) R} (hA : continuous A) :
  continuous (λ x, block_diag (A x)) :=
continuous_pi $ λ i, continuous_matrix $ λ j k, hA.matrix_elem _ _

@[continuity]
lemma continuous.matrix_block_diagonal' [has_zero R] [decidable_eq l]
  {A : X → Π i, matrix (m' i) (n' i) R} (hA : continuous A) :
  continuous (λ x, block_diagonal' (A x)) :=
continuous_matrix $ λ ⟨i₁, i₂⟩ ⟨j₁, j₂⟩, begin
  dsimp only [block_diagonal'_apply'],
  split_ifs,
  { subst h,
    exact ((continuous_apply i₁).comp hA).matrix_elem i₂ j₂ },
  { exact continuous_const },
end

@[continuity]
lemma continuous.matrix_block_diag' {A : X → matrix (Σ i, m' i) (Σ i, n' i) R} (hA : continuous A) :
  continuous (λ x, block_diag' (A x)) :=
continuous_pi $ λ i, continuous_matrix $ λ j k, hA.matrix_elem _ _

end block_matrices

end continuity

/-! ### Lemmas about infinite sums -/
section tsum
variables [semiring α] [add_comm_monoid R] [topological_space R] [module α R]

lemma has_sum.matrix_transpose {f : X → matrix m n R} {a : matrix m n R} (hf : has_sum f a) :
  has_sum (λ x, (f x)ᵀ) aᵀ :=
(hf.map (matrix.transpose_add_equiv m n R) continuous_id.matrix_transpose : _)

lemma summable.matrix_transpose {f : X → matrix m n R} (hf : summable f) :
  summable (λ x, (f x)ᵀ) :=
hf.has_sum.matrix_transpose.summable

@[simp] lemma summable_matrix_transpose {f : X → matrix m n R} :
  summable (λ x, (f x)ᵀ) ↔ summable f :=
(summable.map_iff_of_equiv (matrix.transpose_add_equiv m n R)
    (@continuous_id (matrix m n R) _).matrix_transpose (continuous_id.matrix_transpose) : _)

lemma matrix.transpose_tsum [t2_space R] {f : X → matrix m n R} : (∑' x, f x)ᵀ = ∑' x, (f x)ᵀ :=
begin
  by_cases hf : summable f,
  { exact hf.has_sum.matrix_transpose.tsum_eq.symm },
  { have hft := summable_matrix_transpose.not.mpr hf,
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, transpose_zero] },
end

lemma has_sum.matrix_conj_transpose [star_add_monoid R] [has_continuous_star R]
  {f : X → matrix m n R} {a : matrix m n R} (hf : has_sum f a) :
  has_sum (λ x, (f x)ᴴ) aᴴ :=
(hf.map (matrix.conj_transpose_add_equiv m n R) continuous_id.matrix_conj_transpose : _)

lemma summable.matrix_conj_transpose [star_add_monoid R] [has_continuous_star R]
  {f : X → matrix m n R} (hf : summable f) :
  summable (λ x, (f x)ᴴ) :=
hf.has_sum.matrix_conj_transpose.summable

@[simp] lemma summable_matrix_conj_transpose [star_add_monoid R] [has_continuous_star R]
  {f : X → matrix m n R} :
  summable (λ x, (f x)ᴴ) ↔ summable f :=
(summable.map_iff_of_equiv (matrix.conj_transpose_add_equiv m n R)
  (@continuous_id (matrix m n R) _).matrix_conj_transpose (continuous_id.matrix_conj_transpose) : _)

lemma matrix.conj_transpose_tsum [star_add_monoid R] [has_continuous_star R] [t2_space R]
  {f : X → matrix m n R} : (∑' x, f x)ᴴ = ∑' x, (f x)ᴴ :=
begin
  by_cases hf : summable f,
  { exact hf.has_sum.matrix_conj_transpose.tsum_eq.symm },
  { have hft := summable_matrix_conj_transpose.not.mpr hf,
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, conj_transpose_zero] },
end

lemma has_sum.matrix_diagonal [decidable_eq n] {f : X → n → R} {a : n → R} (hf : has_sum f a) :
  has_sum (λ x, diagonal (f x)) (diagonal a) :=
(hf.map (diagonal_add_monoid_hom n R) $ continuous.matrix_diagonal $ by exact continuous_id : _)

lemma summable.matrix_diagonal [decidable_eq n] {f : X → n → R} (hf : summable f) :
  summable (λ x, diagonal (f x)) :=
hf.has_sum.matrix_diagonal.summable

@[simp] lemma summable_matrix_diagonal [decidable_eq n] {f : X → n → R} :
  summable (λ x, diagonal (f x)) ↔ summable f :=
(summable.map_iff_of_left_inverse
  (@matrix.diagonal_add_monoid_hom n R _ _) (matrix.diag_add_monoid_hom n R)
  (by exact continuous.matrix_diagonal continuous_id)
  continuous_matrix_diag
  (λ A, diag_diagonal A) : _)

lemma matrix.diagonal_tsum [decidable_eq n] [t2_space R] {f : X → n → R} :
  diagonal (∑' x, f x) = ∑' x, diagonal (f x) :=
begin
  by_cases hf : summable f,
  { exact hf.has_sum.matrix_diagonal.tsum_eq.symm },
  { have hft := summable_matrix_diagonal.not.mpr hf,
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft],
    exact diagonal_zero },
end

lemma has_sum.matrix_diag {f : X → matrix n n R} {a : matrix n n R} (hf : has_sum f a) :
  has_sum (λ x, diag (f x)) (diag a) :=
(hf.map (diag_add_monoid_hom n R) continuous_matrix_diag : _)

lemma summable.matrix_diag {f : X → matrix n n R} (hf : summable f) : summable (λ x, diag (f x)) :=
hf.has_sum.matrix_diag.summable

section block_matrices

lemma has_sum.matrix_block_diagonal [decidable_eq p]
  {f : X → p → matrix m n R} {a : p → matrix m n R} (hf : has_sum f a) :
  has_sum (λ x, block_diagonal (f x)) (block_diagonal a) :=
(hf.map (block_diagonal_add_monoid_hom m n p R) $
  continuous.matrix_block_diagonal $ by exact continuous_id : _)

lemma summable.matrix_block_diagonal [decidable_eq p] {f : X → p → matrix m n R} (hf : summable f) :
  summable (λ x, block_diagonal (f x)) :=
hf.has_sum.matrix_block_diagonal.summable

lemma summable_matrix_block_diagonal [decidable_eq p] {f : X → p → matrix m n R} :
  summable (λ x, block_diagonal (f x)) ↔ summable f :=
(summable.map_iff_of_left_inverse
  (matrix.block_diagonal_add_monoid_hom m n p R) (matrix.block_diag_add_monoid_hom m n p R)
  (by exact continuous.matrix_block_diagonal continuous_id)
  (by exact continuous.matrix_block_diag continuous_id)
  (λ A, block_diag_block_diagonal A) : _)

lemma matrix.block_diagonal_tsum [decidable_eq p] [t2_space R] {f : X → p → matrix m n R} :
  block_diagonal (∑' x, f x) = ∑' x, block_diagonal (f x) :=
begin
  by_cases hf : summable f,
  { exact hf.has_sum.matrix_block_diagonal.tsum_eq.symm },
  { have hft := summable_matrix_block_diagonal.not.mpr hf,
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft],
    exact block_diagonal_zero },
end

lemma has_sum.matrix_block_diag {f : X → matrix (m × p) (n × p) R}
  {a : matrix (m × p) (n × p) R} (hf : has_sum f a) :
  has_sum (λ x, block_diag (f x)) (block_diag a) :=
(hf.map (block_diag_add_monoid_hom m n p R) $ continuous.matrix_block_diag continuous_id : _)

lemma summable.matrix_block_diag {f : X → matrix (m × p) (n × p) R} (hf : summable f) :
  summable (λ x, block_diag (f x)) :=
hf.has_sum.matrix_block_diag.summable

lemma has_sum.matrix_block_diagonal' [decidable_eq l]
  {f : X → Π i, matrix (m' i) (n' i) R} {a : Π i, matrix (m' i) (n' i) R} (hf : has_sum f a) :
  has_sum (λ x, block_diagonal' (f x)) (block_diagonal' a) :=
(hf.map (block_diagonal'_add_monoid_hom m' n' R) $
  continuous.matrix_block_diagonal' $ by exact continuous_id : _)

lemma summable.matrix_block_diagonal' [decidable_eq l]
  {f : X → Π i, matrix (m' i) (n' i) R} (hf : summable f) :
  summable (λ x, block_diagonal' (f x)) :=
hf.has_sum.matrix_block_diagonal'.summable

lemma summable_matrix_block_diagonal' [decidable_eq l] {f : X → Π i, matrix (m' i) (n' i) R} :
  summable (λ x, block_diagonal' (f x)) ↔ summable f :=
(summable.map_iff_of_left_inverse
  (matrix.block_diagonal'_add_monoid_hom m' n' R) (matrix.block_diag'_add_monoid_hom m' n' R)
  (by exact continuous.matrix_block_diagonal' continuous_id)
  (by exact continuous.matrix_block_diag' continuous_id)
  (λ A, block_diag'_block_diagonal' A) : _)

lemma matrix.block_diagonal'_tsum [decidable_eq l] [t2_space R]
  {f : X → Π i, matrix (m' i) (n' i) R} :
  block_diagonal' (∑' x, f x) = ∑' x, block_diagonal' (f x) :=
begin
  by_cases hf : summable f,
  { exact hf.has_sum.matrix_block_diagonal'.tsum_eq.symm },
  { have hft := summable_matrix_block_diagonal'.not.mpr hf,
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft],
    exact block_diagonal'_zero },
end

lemma has_sum.matrix_block_diag' {f : X → matrix (Σ i, m' i) (Σ i, n' i) R}
  {a : matrix (Σ i, m' i) (Σ i, n' i) R} (hf : has_sum f a) :
  has_sum (λ x, block_diag' (f x)) (block_diag' a) :=
(hf.map (block_diag'_add_monoid_hom m' n' R) $ continuous.matrix_block_diag' continuous_id : _)

lemma summable.matrix_block_diag' {f : X → matrix (Σ i, m' i) (Σ i, n' i) R} (hf : summable f) :
  summable (λ x, block_diag' (f x)) :=
hf.has_sum.matrix_block_diag'.summable

end block_matrices

end tsum