feat(data/matrix/basic): lemmas about transpose and conj_transpose on sums and products (#9880)

This also generalizes some previous results from `star_ring` to `star_add_monoid` now that the latter exists.

To help prove the non-commutative statements, this adds `monoid_hom.unop_map_list_prod` and similar.
This could probably used for proving `star_list_prod` in future.



Co-authored-by: Johan Commelin <johan@commelin.net>

Author: eric-wieser

src/algebra/big_operators/basic.lean

@@ -124,6 +124,11 @@ lemma ring_hom.map_list_sum [non_assoc_semiring β] [non_assoc_semiring γ]
   f l.sum = (l.map f).sum :=
 f.to_add_monoid_hom.map_list_sum l
 
+/-- A morphism into the opposite ring acts on the product by acting on the reversed elements -/
+lemma ring_hom.unop_map_list_prod [semiring β] [semiring γ] (f : β →+* γᵒᵖ) (l : list β) :
+  opposite.unop (f l.prod) = (l.map (opposite.unop ∘ f)).reverse.prod :=
+f.to_monoid_hom.unop_map_list_prod l
+
 lemma ring_hom.map_multiset_prod [comm_semiring β] [comm_semiring γ] (f : β →+* γ)
   (s : multiset β) :
   f s.prod = (s.map f).prod :=

src/data/equiv/ring.lean

@@ -370,6 +370,11 @@ lemma map_list_prod [semiring R] [semiring S] (f : R ≃+* S) (l : list R) :
 lemma map_list_sum [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) (l : list R) :
   f l.sum = (l.map f).sum := f.to_ring_hom.map_list_sum l
 
+/-- An isomorphism into the opposite ring acts on the product by acting on the reversed elements -/
+lemma unop_map_list_prod [semiring R] [semiring S] (f : R ≃+* Sᵒᵖ) (l : list R) :
+  opposite.unop (f l.prod) = (l.map (opposite.unop ∘ f)).reverse.prod :=
+f.to_ring_hom.unop_map_list_prod l
+
 lemma map_multiset_prod [comm_semiring R] [comm_semiring S] (f : R ≃+* S) (s : multiset R) :
   f s.prod = (s.map f).prod := f.to_ring_hom.map_multiset_prod s
 

src/data/list/basic.lean

@@ -2402,6 +2402,10 @@ theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod :=
 calc (l₁ ++ l₂).prod = foldl (*) (foldl (*) 1 l₁ * 1) l₂ : by simp [list.prod]
   ... = l₁.prod * l₂.prod : foldl_assoc
 
+@[to_additive]
+theorem prod_concat : (l.concat a).prod = l.prod * a :=
+by rw [concat_eq_append, prod_append, prod_cons, prod_nil, mul_one]
+
 @[simp, to_additive]
 theorem prod_join {l : list (list α)} : l.join.prod = (l.map list.prod).prod :=
 by induction l; [refl, simp only [*, list.join, map, prod_append, prod_cons]]
@@ -2485,6 +2489,18 @@ lemma prod_update_nth : ∀ (L : list α) (n : ℕ) (a : α),
 | (x::xs) (i+1) a := by simp [update_nth, prod_update_nth xs i a, mul_assoc]
 | []      _     _ := by simp [update_nth, (nat.zero_le _).not_lt]
 
+open opposite
+
+lemma _root_.opposite.op_list_prod : ∀ (l : list α), op (l.prod) = (l.map op).reverse.prod
+| [] := rfl
+| (x :: xs) := by rw [list.prod_cons, list.map_cons, list.reverse_cons', list.prod_concat, op_mul,
+                      _root_.opposite.op_list_prod]
+
+lemma _root_.opposite.unop_list_prod : ∀ (l : list αᵒᵖ), (l.prod).unop = (l.map unop).reverse.prod
+| [] := rfl
+| (x :: xs) := by rw [list.prod_cons, list.map_cons, list.reverse_cons', list.prod_concat, unop_mul,
+                      _root_.opposite.unop_list_prod]
+
 end monoid
 
 section group
@@ -4671,6 +4687,15 @@ theorem monoid_hom.map_list_prod {α β : Type*} [monoid α] [monoid β] (f : α
   f l.prod = (l.map f).prod :=
 (l.prod_hom f).symm
 
+open opposite
+
+/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements -/
+lemma monoid_hom.unop_map_list_prod {α β : Type*} [monoid α] [monoid β] (f : α →* βᵒᵖ) (l : list α):
+  unop (f l.prod) = (l.map (unop ∘ f)).reverse.prod :=
+begin
+  rw [f.map_list_prod l, opposite.unop_list_prod, list.map_map],
+end
+
 namespace list
 
 @[to_additive]

src/data/matrix/basic.lean

@@ -1137,6 +1137,42 @@ by ext i j; refl
 lemma transpose_map {f : α → β} {M : matrix m n α} : Mᵀ.map f = (M.map f)ᵀ :=
 by { ext, refl }
 
+/-- `matrix.transpose` as an `add_equiv` -/
+@[simps apply]
+def transpose_add_equiv [has_add α] : matrix m n α ≃+ matrix n m α :=
+{ to_fun := transpose,
+  inv_fun := transpose,
+  left_inv := transpose_transpose,
+  right_inv := transpose_transpose,
+  map_add' := transpose_add }
+
+@[simp] lemma transpose_add_equiv_symm [has_add α] :
+  (transpose_add_equiv : matrix m n α ≃+ matrix n m α).symm = transpose_add_equiv := rfl
+
+lemma transpose_list_sum [add_monoid α] (l : list (matrix m n α)) :
+  l.sumᵀ = (l.map transpose).sum :=
+(transpose_add_equiv : matrix m n α ≃+ matrix n m α).to_add_monoid_hom.map_list_sum l
+
+lemma transpose_multiset_sum [add_comm_monoid α] (s : multiset (matrix m n α)) :
+  s.sumᵀ = (s.map transpose).sum :=
+(transpose_add_equiv : matrix m n α ≃+ matrix n m α).to_add_monoid_hom.map_multiset_sum s
+
+lemma transpose_sum [add_comm_monoid α] {ι : Type*} (s : finset ι) (M : ι → matrix m n α) :
+  (∑ i in s, M i)ᵀ = ∑ i in s, (M i)ᵀ :=
+(transpose_add_equiv : matrix m n α ≃+ matrix n m α).to_add_monoid_hom.map_sum _ s
+
+/-- `matrix.transpose` as a `ring_equiv` to the opposite ring -/
+@[simps]
+def transpose_ring_equiv [comm_semiring α] [fintype m] : matrix m m α ≃+* (matrix m m α)ᵒᵖ :=
+{ to_fun := λ M, opposite.op (Mᵀ),
+  inv_fun := λ M, M.unopᵀ,
+  map_mul' := λ M N, (congr_arg opposite.op (transpose_mul M N)).trans (opposite.op_mul _ _),
+  ..transpose_add_equiv.trans opposite.op_add_equiv }
+
+lemma transpose_list_prod [comm_semiring α] [fintype m] [decidable_eq m] (l : list (matrix m m α)) :
+  l.prodᵀ = (l.map transpose).reverse.prod :=
+(transpose_ring_equiv : matrix m m α ≃+* (matrix m m α)ᵒᵖ).unop_map_list_prod l
+
 end transpose
 
 section conj_transpose
@@ -1162,11 +1198,10 @@ by ext i j; simp
   (1 : matrix n n α)ᴴ = 1 :=
 by simp [conj_transpose]
 
-@[simp] lemma conj_transpose_add
-[semiring α] [star_ring α] (M : matrix m n α) (N : matrix m n α) :
+@[simp] lemma conj_transpose_add [add_monoid α] [star_add_monoid α] (M N : matrix m n α) :
   (M + N)ᴴ = Mᴴ + Nᴴ  := by ext i j; simp
 
-@[simp] lemma conj_transpose_sub [ring α] [star_ring α] (M : matrix m n α) (N : matrix m n α) :
+@[simp] lemma conj_transpose_sub [add_group α] [star_add_monoid α] (M N : matrix m n α) :
   (M - N)ᴴ = Mᴴ - Nᴴ  := by ext i j; simp
 
 @[simp] lemma conj_transpose_smul [comm_monoid α] [star_monoid α] (c : α) (M : matrix m n α) :
@@ -1179,6 +1214,46 @@ by ext i j; simp [mul_comm]
 @[simp] lemma conj_transpose_neg [ring α] [star_ring α] (M : matrix m n α) :
   (- M)ᴴ = - Mᴴ  := by ext i j; simp
 
+/-- `matrix.conj_transpose` as an `add_equiv` -/
+@[simps apply]
+def conj_transpose_add_equiv [add_monoid α] [star_add_monoid α] : matrix m n α ≃+ matrix n m α :=
+{ to_fun := conj_transpose,
+  inv_fun := conj_transpose,
+  left_inv := conj_transpose_conj_transpose,
+  right_inv := conj_transpose_conj_transpose,
+  map_add' := conj_transpose_add }
+
+@[simp] lemma conj_transpose_add_equiv_symm [add_monoid α] [star_add_monoid α] :
+  (conj_transpose_add_equiv : matrix m n α ≃+ matrix n m α).symm = conj_transpose_add_equiv := rfl
+
+lemma conj_transpose_list_sum [add_monoid α] [star_add_monoid α] (l : list (matrix m n α)) :
+  l.sumᴴ = (l.map conj_transpose).sum :=
+(conj_transpose_add_equiv : matrix m n α ≃+ matrix n m α).to_add_monoid_hom.map_list_sum l
+
+lemma conj_transpose_multiset_sum [add_comm_monoid α] [star_add_monoid α]
+  (s : multiset (matrix m n α)) :
+  s.sumᴴ = (s.map conj_transpose).sum :=
+(conj_transpose_add_equiv : matrix m n α ≃+ matrix n m α).to_add_monoid_hom.map_multiset_sum s
+
+lemma conj_transpose_sum [add_comm_monoid α] [star_add_monoid α] {ι : Type*} (s : finset ι)
+  (M : ι → matrix m n α) :
+  (∑ i in s, M i)ᴴ = ∑ i in s, (M i)ᴴ :=
+(conj_transpose_add_equiv : matrix m n α ≃+ matrix n m α).to_add_monoid_hom.map_sum _ s
+
+/-- `matrix.conj_transpose` as a `ring_equiv` to the opposite ring -/
+@[simps]
+def conj_transpose_ring_equiv [comm_semiring α] [star_ring α] [fintype m] :
+  matrix m m α ≃+* (matrix m m α)ᵒᵖ :=
+{ to_fun := λ M, opposite.op (Mᴴ),
+  inv_fun := λ M, M.unopᴴ,
+  map_mul' := λ M N, (congr_arg opposite.op (conj_transpose_mul M N)).trans (opposite.op_mul _ _),
+  ..conj_transpose_add_equiv.trans opposite.op_add_equiv }
+
+lemma conj_transpose_list_prod [comm_semiring α] [star_ring α] [fintype m] [decidable_eq m]
+  (l : list (matrix m m α)) :
+  l.prodᴴ = (l.map conj_transpose).reverse.prod :=
+(conj_transpose_ring_equiv : matrix m m α ≃+* (matrix m m α)ᵒᵖ).unop_map_list_prod l
+
 end conj_transpose
 
 section star
@@ -1195,6 +1270,10 @@ lemma star_eq_conj_transpose [has_star α] (M : matrix m m α) : star M = Mᴴ :
 instance [has_involutive_star α] : has_involutive_star (matrix n n α) :=
 { star_involutive := conj_transpose_conj_transpose }
 
+/-- When `α` is a `*`-additive monoid, `matrix.has_star` is also a `*`-additive monoid. -/
+instance [add_monoid α] [star_add_monoid α] : star_add_monoid (matrix n n α) :=
+{ star_add := conj_transpose_add }
+
 /-- When `α` is a `*`-(semi)ring, `matrix.has_star` is also a `*`-(semi)ring. -/
 instance [fintype n] [decidable_eq n] [semiring α] [star_ring α] : star_ring (matrix n n α) :=
 { star_add := conj_transpose_add,