[Merged by Bors] - feat(ring_theory/matrix_equiv_tensor): matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R)

src/algebra/ring.lean

@@ -229,6 +229,9 @@ variables [rα : semiring α] [rβ : semiring β]
 section
 include rα rβ
 
+@[simp]
+lemma to_fun_eq_coe (f : α →+* β) : f.to_fun = f := rfl
+
 @[simp] lemma coe_mk (f : α → β) (h₁ h₂ h₃ h₄) : ⇑(⟨f, h₁, h₂, h₃, h₄⟩ : α →+* β) = f := rfl
 
 variables (f : α →+* β) {x y : α} {rα rβ}

src/data/matrix/basic.lean

@@ -334,22 +334,52 @@ instance {β : Type w} [semiring α] [add_comm_monoid β] [semimodule α β] :
 
 @[simp] lemma smul_val [semiring α] (a : α) (A : matrix m n α) (i : m) (j : n) : (a • A) i j = a * A i j := rfl
 
-section comm_semiring
-variables [comm_semiring α]
+section semiring
+variables [semiring α]
 
 lemma smul_eq_diagonal_mul [decidable_eq m] (M : matrix m n α) (a : α) :
   a • M = diagonal (λ _, a) ⬝ M :=
 by { ext, simp }
 
+@[simp] lemma smul_mul (M : matrix m n α) (a : α) (N : matrix n l α) : (a • M) ⬝ N = a • M ⬝ N :=
+by { ext, apply smul_dot_product }
+
+@[simp] lemma mul_mul_left (M : matrix m n α) (N : matrix n o α) (a : α) :
+  (λ i j, a * M i j) ⬝ N = a • (M ⬝ N) :=
+begin
+  simp only [←smul_val],
+  simp,
+end
+
+/--
+The ring homomorphism `α →+* matrix n n α`
+sending `a` to the diagonal matrix with `a` on the diagonal.
+-/
+def scalar (n : Type u) [fintype n] [decidable_eq n] : α →+* matrix n n α :=
+{ to_fun := λ a, a • 1,
+  map_zero' := by simp,
+  map_add' := by { intros, ext, simp [add_mul], },
+  map_one' := by simp,
+  map_mul' := by { intros, ext, simp [mul_assoc], }, }
+
+end semiring
+
+section comm_semiring
+variables [comm_semiring α]
+
 lemma smul_eq_mul_diagonal [decidable_eq n] (M : matrix m n α) (a : α) :
   a • M = M ⬝ diagonal (λ _, a) :=
 by { ext, simp [mul_comm] }
 
 @[simp] lemma mul_smul (M : matrix m n α) (a : α) (N : matrix n l α) : M ⬝ (a • N) = a • M ⬝ N :=
 by { ext, apply dot_product_smul }
 
-@[simp] lemma smul_mul (M : matrix m n α) (a : α) (N : matrix n l α) : (a • M) ⬝ N = a • M ⬝ N :=
-by { ext, apply smul_dot_product }
+@[simp] lemma mul_mul_right (M : matrix m n α) (N : matrix n o α) (a : α) :
+  M ⬝ (λ i j, a * N i j) = a • (M ⬝ N) :=
+begin
+  simp only [←smul_val],
+  simp,
+end
 
 end comm_semiring
 
@@ -547,3 +577,13 @@ lemma row_mul_vec [semiring α] (M : matrix m n α) (v : n → α) :
 end row_col
 
 end matrix
+
+namespace ring_hom
+variables {α β : Type*} [semiring α] [semiring β]
+variables {m n o : Type u} [fintype m] [fintype n] [fintype o]
+
+lemma map_matrix_mul (M : matrix m n α) (N : matrix n o α) (i : m) (j : o) (f : α →+* β) :
+  f (matrix.mul M N i j) = matrix.mul (λ i j, f (M i j)) (λ i j, f (N i j)) i j :=
+by simp [matrix.mul_val, ring_hom.map_sum]
+
+end ring_hom

src/linear_algebra/tensor_product.lean

@@ -249,6 +249,29 @@ lemma tmul_zero (m : M) : (m ⊗ₜ[R] 0 : M ⊗ N) = 0 := (mk R M N _).map_zero
 lemma neg_tmul (m : M) (n : N) : (-m) ⊗ₜ n = -(m ⊗ₜ[R] n) := (mk R M N).map_neg₂ _ _
 lemma tmul_neg (m : M) (n : N) : m ⊗ₜ (-n) = -(m ⊗ₜ[R] n) := (mk R M N _).map_neg _
 
+
+section
+open_locale big_operators
+
+lemma sum_tmul {α : Type*} (s : finset α) (m : α → M) (n : N) :
+  ((∑ a in s, m a) ⊗ₜ[R] n) = ∑ a in s, m a ⊗ₜ[R] n :=
+begin
+  classical,
+  induction s using finset.induction with a s has ih h,
+  { simp, },
+  { simp [finset.sum_insert has, add_tmul, ih], },
+end
+
+lemma tmul_sum (m : M) {α : Type*} (s : finset α) (n : α → N) :
+  (m ⊗ₜ[R] (∑ a in s, n a)) = ∑ a in s, m ⊗ₜ[R] n a :=
+begin
+  classical,
+  induction s using finset.induction with a s has ih h,
+  { simp, },
+  { simp [finset.sum_insert has, tmul_add, ih], },
+end
+end
+
 end module
 
 local attribute [instance] quotient_add_group.left_rel normal_add_subgroup.to_is_add_subgroup

src/logic/basic.lean

@@ -968,3 +968,25 @@ instance {α β} [h : nonempty α] [h2 : nonempty β] : nonempty (α × β) :=
 h.elim $ λ g, h2.elim $ λ g2, ⟨⟨g, g2⟩⟩
 
 end nonempty
+
+section ite
+
+lemma apply_dite {α β : Type*} (f : α → β) (P : Prop) [decidable P] (x : P → α) (y : ¬P → α) :
+  f (dite P x y) = dite P (λ h, f (x h)) (λ h, f (y h)) :=
+by { by_cases h : P; simp [h], }
+
+lemma apply_ite {α β : Type*} (f : α → β) (P : Prop) [decidable P] (x y : α) :
+  f (ite P x y) = ite P (f x) (f y) :=
+apply_dite f P (λ _, x) (λ _, y)
+
+lemma dite_apply {α : Type*} {β : α → Type*} (P : Prop) [decidable P]
+  (f : P → Π a, β a) (g : ¬ P → Π a, β a) (x : α) :
+  (dite P f g) x = dite P (λ h, f h x) (λ h, g h x) :=
+by { by_cases h : P; simp [h], }
+
+lemma ite_apply {α : Type*} {β : α → Type*} (P : Prop) [decidable P]
+  (f g : Π a, β a) (x : α) :
+  (ite P f g) x = ite P (f x) (g x) :=
+dite_apply P (λ _, f) (λ _, g) x
+
+end ite

src/ring_theory/algebra.lean

@@ -106,6 +106,10 @@ attribute [instance, priority 0] algebra.to_has_scalar
 lemma smul_def (r : R) (x : A) : r • x = algebra_map R A r * x :=
 algebra.smul_def' r x
 
+lemma algebra_map_eq_smul_one (r : R) : algebra_map R A r = r • 1 :=
+calc algebra_map R A r = algebra_map R A r * 1 : (mul_one _).symm
+                   ... = r • 1                 : (algebra.smul_def r 1).symm
+
 theorem commutes (r : R) (x : A) : algebra_map R A r * x = x * algebra_map R A r :=
 algebra.commutes' r x
 
@@ -171,13 +175,9 @@ instance module.endomorphism_algebra (R : Type u) (M : Type v)
 
 instance matrix_algebra (n : Type u) (R : Type v)
   [fintype n] [decidable_eq n] [comm_semiring R] : algebra R (matrix n n R) :=
-{ to_fun    := λ r, r • 1,
-  map_one'  := one_smul _ _,
-  map_mul'  := λ r₁ r₂, by { ext, simp [mul_assoc] },
-  map_zero' :=  zero_smul _ _,
-  map_add'  := λ _ _, add_smul _ _ _,
-  commutes' := by { intros, simp },
-  smul_def' := by { intros, simp } }
+{ commutes' := by { intros, simp [matrix.scalar], },
+  smul_def' := by { intros, simp [matrix.scalar], },
+  ..(matrix.scalar n) }
 
 set_option old_structure_cmd true
 /-- Defining the homomorphism in the category R-Alg. -/
@@ -447,6 +447,9 @@ def symm (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁ :=
 
 @[simp] lemma inv_fun_apply {e : A₁ ≃ₐ[R] A₂} {a : A₂} : e.inv_fun a = e.symm a := rfl
 
+@[simp] lemma symm_symm {e : A₁ ≃ₐ[R] A₂} : e.symm.symm = e :=
+by { ext, refl, }
+
 /-- Algebra equivalences are transitive. -/
 @[trans]
 def trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃ₐ[R] A₃ :=

src/ring_theory/matrix_algebra.lean

@@ -0,0 +1,199 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import ring_theory.tensor_product
+import data.matrix.basic
+
+/-!
+We provide the `R`-algebra structure on `matrix n n A` when `A` is an `R`-algebra,
+and show `matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R)`.
+-/
+
+universes u v w
+
+open_locale tensor_product
+open_locale big_operators
+
+open tensor_product
+open algebra.tensor_product
+
+variables {R : Type u} [comm_ring R]
+variables {A : Type v} [comm_ring A] [algebra R A]
+variables {n : Type w} [fintype n]
+
+section
+variables [decidable_eq n]
+
+instance : algebra R (matrix n n A) :=
+{ commutes' := λ r x, begin ext, simp [matrix.scalar], end,
+  smul_def' := λ r x, begin ext, simp [matrix.scalar, algebra.smul_def'' r], end,
+  ..((matrix.scalar n).comp (algebra_map R A)) }
+
+lemma algebra_map_matrix_val {r : R} {i j : n} :
+  algebra_map R (matrix n n A) r i j = if i = j then algebra_map R A r else 0 :=
+begin
+  dsimp [algebra_map, algebra.to_ring_hom, matrix.scalar],
+  split_ifs with h; simp [h, matrix.one_val_ne],
+end
+end
+
+variables (R A n)
+namespace matrix_equiv_tensor
+
+/--
+(Implementation detail).
+The bare function underlying `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`, on pure tensors.
+-/
+def to_fun (a : A) (m : matrix n n R) : matrix n n A :=
+λ i j, a * algebra_map R A (m i j)
+
+/--
+(Implementation detail).
+The function underlying `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`,
+as an `R`-linear map in the second tensor factor.
+-/
+def to_fun_right_linear (a : A) : matrix n n R →ₗ[R] matrix n n A :=
+{ to_fun := to_fun R A n a,
+  map_add' := λ x y, by { dsimp only [to_fun], ext, simp [mul_add], },
+  map_smul' := λ r x,
+  begin
+    dsimp only [to_fun],
+    ext,
+    simp only [matrix.smul_val, pi.smul_apply, ring_hom.map_mul,
+      algebra.id.smul_eq_mul, ring_hom.map_mul],
+    rw [algebra.smul_def r, mul_left_comm],
+  end, }
+
+/--
+(Implementation detail).
+The function underlying `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`,
+as an `R`-bilinear map.
+-/
+def to_fun_bilinear : A →ₗ[R] matrix n n R →ₗ[R] matrix n n A :=
+{ to_fun := to_fun_right_linear R A n,
+  map_add' := λ x y, by { ext, simp [to_fun_right_linear, to_fun, add_mul], },
+  map_smul' := λ r x, by { ext, simp [to_fun_right_linear, to_fun] }, }
+
+/--
+(Implementation detail).
+The function underlying `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`,
+as an `R`-linear map.
+-/
+def to_fun_linear : A ⊗[R] matrix n n R →ₗ[R] matrix n n A :=
+tensor_product.lift (to_fun_bilinear R A n)
+
+variables [decidable_eq n]
+
+/--
+The function `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`, as an algebra homomorphism.
+-/
+def to_fun_alg_hom : (A ⊗[R] matrix n n R) →ₐ[R] matrix n n A :=
+alg_hom_of_linear_map_tensor_product (to_fun_linear R A n)
+begin
+  intros, ext,
+  simp only [to_fun_linear, to_fun_bilinear, to_fun_right_linear, to_fun, lift.tmul,
+    linear_map.coe_mk, matrix.mul_mul_left, matrix.smul_val, matrix.mul_eq_mul,
+    matrix.mul_mul_right, ring_hom.map_matrix_mul],
+  rw [←_root_.mul_assoc, mul_comm a₁ a₂],
+end
+begin
+  intros, ext,
+  simp only [to_fun_linear, to_fun_bilinear, to_fun_right_linear, to_fun, matrix.one_val,
+    algebra_map_matrix_val, lift.tmul, linear_map.coe_mk],
+  split_ifs; simp,
+end
+
+@[simp] lemma to_fun_alg_hom_apply (a : A) (m : matrix n n R) :
+  to_fun_alg_hom R A n (a ⊗ₜ m) = λ i j, a * algebra_map R A (m i j) :=
+begin
+  simp [to_fun_alg_hom, alg_hom_of_linear_map_tensor_product, to_fun_linear],
+  refl,
+end
+
+/--
+(Implementation detail.)
+
+The bare function `matrix n n A → A ⊗[R] matrix n n R`.
+(We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)
+-/
+def inv_fun (M : matrix n n A) : A ⊗[R] matrix n n R :=
+∑ (p : n × n), M p.1 p.2 ⊗ₜ (λ i' j', if (i', j') = p then 1 else 0)
+
+@[simp] lemma inv_fun_zero : inv_fun R A n 0 = 0 :=
+by simp [inv_fun]
+
+@[simp] lemma inv_fun_add (M N : matrix n n A) :
+  inv_fun R A n (M + N) = inv_fun R A n M + inv_fun R A n N :=
+by simp [inv_fun, add_tmul, finset.sum_add_distrib]
+
+@[simp] lemma inv_fun_smul (a : A) (M : matrix n n A) :
+  inv_fun R A n (λ i j, a * M i j) = (a ⊗ₜ 1) * inv_fun R A n M :=
+by simp [inv_fun,finset.mul_sum]
+
+@[simp] lemma inv_fun_algebra_map (M : matrix n n R) :
+  inv_fun R A n (λ i j, algebra_map R A (M i j)) = 1 ⊗ₜ M :=
+begin
+  dsimp [inv_fun],
+  simp only [algebra.algebra_map_eq_smul_one, smul_tmul, ←tmul_sum, (•), mul_boole],
+  congr, ext,
+  calc
+    (∑ (x : n × n), λ (i i_1 : n), ite ((i, i_1) = x) (M x.fst x.snd) 0) i j
+      = (∑ (x : n × n), λ (i_1 : n), ite ((i, i_1) = x) (M x.fst x.snd) 0) j : _
+     ... = (∑ (x : n × n), ite ((i, j) = x) (M x.fst x.snd) 0) : _
+     ... = M i j : _,
+  { apply congr_fun, dsimp, simp, },
+  { simp, },
+  { simp, },
+end
+
+lemma right_inv (M : matrix n n A) : (to_fun_alg_hom R A n) (inv_fun R A n M) = M :=
+begin
+  ext,
+  simp [inv_fun, alg_hom.map_sum, apply_ite (algebra_map R A)],
+end
+
+lemma left_inv (M : A ⊗[R] matrix n n R) : inv_fun R A n (to_fun_alg_hom R A n M) = M :=
+begin
+  apply tensor_product.induction_on _ _ M,
+  { simp, },
+  { intros a m, simp, },
+  { intros x y hx hy, simp [alg_hom.map_sum, hx, hy], },
+end
+
+/--
+(Implementation detail)
+
+The equivalence, ignoring the algebra structure, `(A ⊗[R] matrix n n R) ≃ matrix n n A`.
+-/
+def equiv : (A ⊗[R] matrix n n R) ≃ matrix n n A :=
+{ to_fun := to_fun_alg_hom R A n,
+  inv_fun := inv_fun R A n,
+  left_inv := left_inv R A n,
+  right_inv := right_inv R A n, }
+
+end matrix_equiv_tensor
+
+variables [decidable_eq n]
+
+/--
+The `R`-algebra isomorphism `matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R)`.
+-/
+def matrix_equiv_tensor : matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) :=
+alg_equiv.symm { ..(matrix_equiv_tensor.to_fun_alg_hom R A n), ..(matrix_equiv_tensor.equiv R A n) }
+
+open matrix_equiv_tensor
+
+@[simp] lemma matrix_equiv_tensor_apply (M : matrix n n A) :
+  matrix_equiv_tensor R A n M =
+    ∑ (p : n × n), M p.1 p.2 ⊗ₜ (λ i' j', if (i', j') = p then 1 else 0) :=
+rfl
+
+@[simp] lemma matrix_equiv_tensor_apply_symm (a : A) (M : matrix n n R) :
+  (matrix_equiv_tensor R A n).symm (a ⊗ₜ M) =
+    λ i j, a * algebra_map R A (M i j) :=
+begin
+  simp [matrix_equiv_tensor, to_fun_alg_hom, alg_hom_of_linear_map_tensor_product, to_fun_linear],
+  refl,
+end

src/ring_theory/tensor_product.lean

@@ -180,7 +180,7 @@ instance : algebra R (A ⊗[R] B) :=
     apply tensor_product.induction_on A B x,
     { simp, },
     { intros a b, simp [tensor_algebra_map, algebra.commutes], },
-    { intros, simp [mul_add, add_mul, *], },
+    { intros y y' h h', simp at h h', simp [mul_add, add_mul, h, h'], },
   end,
   smul_def' := λ r x,
   begin