feat(data/matrix/{basic, block}): missing lemmas on conj_transpose (#8303)

This also moves some imports around to make the star operator on vectors available in matrix/basic.lean

This is a follow up to #8291

Author: eric-wieser

src/algebra/star/algebra.lean

@@ -5,14 +5,15 @@ Authors: Scott Morrison
 -/
 import algebra.algebra.basic
 import algebra.star.basic
+import algebra.star.pi
 
 /-!
 # Star algebras
 
 Introduces the notion of a star algebra over a star ring.
 -/
 
-universes u v
+universes u v w
 
 /--
 A star algebra `A` over a star ring `R` is an algebra which is a star ring,
@@ -30,3 +31,16 @@ class star_algebra (R : Type u) (A : Type v)
   (r : R) (a : A) :
   star (r • a) = star r • star a :=
 star_algebra.star_smul r a
+
+namespace pi
+
+variable {I : Type u}     -- The indexing type
+variable {f : I → Type v} -- The family of types already equipped with instances
+
+instance {R : Type w}
+  [comm_semiring R] [Π i, semiring (f i)] [Π i, algebra R (f i)]
+  [star_ring R] [Π i, star_ring (f i)] [Π i, star_algebra R (f i)] :
+  star_algebra R (Π i, f i) :=
+{ star_smul := λ r x, funext $ λ _, star_smul _ _ }
+
+end pi

src/algebra/star/pi.lean

@@ -3,13 +3,17 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import algebra.star.algebra
+import algebra.star.basic
+import algebra.ring.pi
 
 /-!
 # `star` on pi types
 
 We put a `has_star` structure on pi types that operates elementwise, such that it describes the
 complex conjugation of vectors.
+
+Note that `pi.star_algebra` is in a different file to avoid pulling in everything from
+`algebra/algebra/basic`.
 -/
 
 universes u v w
@@ -33,10 +37,4 @@ instance [Π i, semiring (f i)] [Π i, star_ring (f i)] : star_ring (Π i, f i)
 { star_add := λ _ _, funext $ λ _, star_add _ _,
   ..(by apply_instance : star_monoid (Π i, f i)) }
 
-instance {R : Type w}
-  [comm_semiring R] [Π i, semiring (f i)] [Π i, algebra R (f i)]
-  [star_ring R] [Π i, star_ring (f i)] [Π i, star_algebra R (f i)] :
-  star_algebra R (Π i, f i) :=
-{ star_smul := λ r x, funext $ λ _, star_smul _ _ }
-
 end pi

src/data/matrix/basic.lean

@@ -7,7 +7,7 @@ import algebra.big_operators.pi
 import algebra.module.pi
 import algebra.module.linear_map
 import algebra.big_operators.ring
-import algebra.star.basic
+import algebra.star.pi
 import data.equiv.ring
 import data.fintype.card
 import data.matrix.dmatrix
@@ -315,6 +315,18 @@ by simp [dot_product, finset.smul_sum, smul_mul_assoc]
   dot_product v (x • w) = x • dot_product v w :=
 by simp [dot_product, finset.smul_sum, mul_smul_comm]
 
+lemma star_dot_product_star [semiring α] [star_ring α] (v w : m → α) :
+  dot_product (star v) (star w) = star (dot_product w v) :=
+by simp [dot_product]
+
+lemma star_dot_product [semiring α] [star_ring α] (v w : m → α) :
+  dot_product (star v) w = star (dot_product (star w) v) :=
+by simp [dot_product]
+
+lemma dot_product_star [semiring α] [star_ring α] (v w : m → α) :
+  dot_product v (star w) = star (dot_product w (star v)) :=
+by simp [dot_product]
+
 end dot_product
 
 /-- `M ⬝ N` is the usual product of matrices `M` and `N`, i.e. we have that
@@ -1172,9 +1184,14 @@ by { ext, refl }
 @[simp] lemma row_apply (v : m → α) (i j) : matrix.row v i j = v j := rfl
 
 @[simp]
-lemma transpose_col (v : m → α) : (matrix.col v).transpose = matrix.row v := by {ext, refl}
+lemma transpose_col (v : m → α) : (matrix.col v)ᵀ = matrix.row v := by { ext, refl }
 @[simp]
-lemma transpose_row (v : m → α) : (matrix.row v).transpose = matrix.col v := by {ext, refl}
+lemma transpose_row (v : m → α) : (matrix.row v)ᵀ = matrix.col v := by { ext, refl }
+
+@[simp]
+lemma conj_transpose_col [has_star α] (v : m → α) : (col v)ᴴ = row (star v) := by { ext, refl }
+@[simp]
+lemma conj_transpose_row [has_star α] (v : m → α) : (row v)ᴴ = col (star v) := by { ext, refl }
 
 lemma row_vec_mul [semiring α] (M : matrix m n α) (v : m → α) :
   matrix.row (matrix.vec_mul v M) = matrix.row v ⬝ M := by {ext, refl}
@@ -1232,6 +1249,22 @@ begin
   { rwa [update_column_ne h, if_neg h] }
 end
 
+lemma map_update_row [decidable_eq n] (f : α → β) :
+  map (update_row M i b) f = update_row (M.map f) i (f ∘ b) :=
+begin
+  ext i' j',
+  rw [update_row_apply, map_apply, map_apply, update_row_apply],
+  exact apply_ite f _ _ _,
+end
+
+lemma map_update_column [decidable_eq m] (f : α → β) :
+  map (update_column M j c) f = update_column (M.map f) j (f ∘ c) :=
+begin
+  ext i' j',
+  rw [update_column_apply, map_apply, map_apply, update_column_apply],
+  exact apply_ite f _ _ _,
+end
+
 lemma update_row_transpose [decidable_eq m] : update_row Mᵀ j c = (update_column M j c)ᵀ :=
 begin
   ext i' j,
@@ -1246,6 +1279,22 @@ begin
   refl
 end
 
+lemma update_row_conj_transpose [decidable_eq m] [has_star α] :
+  update_row Mᴴ j (star c) = (update_column M j c)ᴴ :=
+begin
+  rw [conj_transpose, conj_transpose, transpose_map, transpose_map, update_row_transpose,
+    map_update_column],
+  refl,
+end
+
+lemma update_column_conj_transpose [decidable_eq n] [has_star α] :
+  update_column Mᴴ i (star b) = (update_row M i b)ᴴ :=
+begin
+  rw [conj_transpose, conj_transpose, transpose_map, transpose_map, update_column_transpose,
+    map_update_row],
+  refl,
+end
+
 @[simp] lemma update_row_eq_self [decidable_eq m]
   (A : matrix m n α) {i : m} :
   A.update_row i (A i) = A :=

src/data/matrix/block.lean

@@ -20,7 +20,7 @@ import data.matrix.basic
 variables {l m n o : Type*} [fintype l] [fintype m] [fintype n] [fintype o]
 variables {m' : o → Type*} [∀ i, fintype (m' i)]
 variables {n' : o → Type*} [∀ i, fintype (n' i)]
-variables {R : Type*} {S : Type*} {α : Type*}
+variables {R : Type*} {S : Type*} {α : Type*} {β : Type*}
 
 open_locale matrix
 
@@ -101,13 +101,27 @@ rfl
   (from_blocks A B C D).to_blocks₂₂ = D :=
 rfl
 
+lemma from_blocks_map
+  (A : matrix n l α) (B : matrix n m α) (C : matrix o l α) (D : matrix o m α) (f : α → β) :
+  (from_blocks A B C D).map f = from_blocks (A.map f) (B.map f) (C.map f) (D.map f) :=
+begin
+  ext i j, rcases i; rcases j; simp [from_blocks],
+end
+
 lemma from_blocks_transpose
   (A : matrix n l α) (B : matrix n m α) (C : matrix o l α) (D : matrix o m α) :
   (from_blocks A B C D)ᵀ = from_blocks Aᵀ Cᵀ Bᵀ Dᵀ :=
 begin
   ext i j, rcases i; rcases j; simp [from_blocks],
 end
 
+lemma from_blocks_conj_transpose [has_star α]
+  (A : matrix n l α) (B : matrix n m α) (C : matrix o l α) (D : matrix o m α) :
+  (from_blocks A B C D)ᴴ = from_blocks Aᴴ Cᴴ Bᴴ Dᴴ :=
+begin
+  simp only [conj_transpose, from_blocks_transpose, from_blocks_map]
+end
+
 /-- Let `p` pick out certain rows and `q` pick out certain columns of a matrix `M`. Then
   `to_block M p q` is the corresponding block matrix. -/
 def to_block (M : matrix m n α) (p : m → Prop) [decidable_pred p]
@@ -191,7 +205,7 @@ variables (M N : o → matrix m n α) [decidable_eq o]
 
 section has_zero
 
-variables [has_zero α]
+variables [has_zero α] [has_zero β]
 
 /-- `matrix.block_diagonal M` turns a homogenously-indexed collection of matrices
 `M : o → matrix m n α'` into a `m × o`-by-`n × o` block matrix which has the entries of `M` along
@@ -215,6 +229,14 @@ lemma block_diagonal_apply_ne (i j) {k k'} (h : k ≠ k') :
   block_diagonal M (i, k) (j, k') = 0 :=
 if_neg h
 
+lemma block_diagonal_map (f : α → β) (hf : f 0 = 0) :
+  (block_diagonal M).map f = block_diagonal (λ k, (M k).map f) :=
+begin
+  ext,
+  simp only [map_apply, block_diagonal_apply, eq_comm],
+  rw [apply_ite f, hf],
+end
+
 @[simp] lemma block_diagonal_transpose :
   (block_diagonal M)ᵀ = block_diagonal (λ k, (M k)ᵀ) :=
 begin
@@ -225,6 +247,14 @@ begin
   { refl }
 end
 
+@[simp] lemma block_diagonal_conj_transpose
+  {α : Type*} [semiring α] [star_ring α] (M : o → matrix m n α) :
+  (block_diagonal M)ᴴ = block_diagonal (λ k, (M k)ᴴ) :=
+begin
+  simp only [conj_transpose, block_diagonal_transpose],
+  rw block_diagonal_map _ star (star_zero α),
+end
+
 @[simp] lemma block_diagonal_zero :
   block_diagonal (0 : o → matrix m n α) = 0 :=
 by { ext, simp [block_diagonal_apply] }
@@ -284,7 +314,7 @@ variables (M N : Π i, matrix (m' i) (n' i) α) [decidable_eq o]
 
 section has_zero
 
-variables [has_zero α]
+variables [has_zero α] [has_zero β]
 
 /-- `matrix.block_diagonal' M` turns `M : Π i, matrix (m i) (n i) α` into a
 `Σ i, m i`-by-`Σ i, n i` block matrix which has the entries of `M` along the diagonal
@@ -317,6 +347,14 @@ lemma block_diagonal'_apply_ne {k k'} (i j) (h : k ≠ k') :
   block_diagonal' M ⟨k, i⟩ ⟨k', j⟩ = 0 :=
 dif_neg h
 
+lemma block_diagonal'_map (f : α → β) (hf : f 0 = 0) :
+  (block_diagonal' M).map f = block_diagonal' (λ k, (M k).map f) :=
+begin
+  ext,
+  simp only [map_apply, block_diagonal'_apply, eq_comm],
+  rw [apply_dite f, hf],
+end
+
 @[simp] lemma block_diagonal'_transpose :
   (block_diagonal' M)ᵀ = block_diagonal' (λ k, (M k)ᵀ) :=
 begin
@@ -330,6 +368,14 @@ begin
   { refl }
 end
 
+@[simp] lemma block_diagonal'_conj_transpose {α} [semiring α] [star_ring α]
+  (M : Π i, matrix (m' i) (n' i) α) :
+  (block_diagonal' M)ᴴ = block_diagonal' (λ k, (M k)ᴴ) :=
+begin
+  simp only [conj_transpose, block_diagonal'_transpose],
+  exact block_diagonal'_map _ star (star_zero α),
+end
+
 @[simp] lemma block_diagonal'_zero :
   block_diagonal' (0 : Π i, matrix (m' i) (n' i) α) = 0 :=
 by { ext, simp [block_diagonal'_apply] }