feat(linear_algebra/matrix/nonsingular_inverse): inverse of a diagona…

…l matrix is diagonal (#13827)

The main results are `is_unit (diagonal v) ↔ is_unit v` and `(diagonal v)⁻¹ = diagonal (ring.inverse v)`.

This also generalizes `invertible.map` to `monoid_hom_class`.

src/algebra/invertible.lean

@@ -260,12 +260,10 @@ def invertible_inv {a : α} [invertible a] : invertible (a⁻¹) :=
 
 end group_with_zero
 
-/--
-Monoid homs preserve invertibility.
--/
-def invertible.map {R : Type*} {S : Type*} [monoid R] [monoid S] (f : R →* S)
-  (r : R) [invertible r] :
+/-- Monoid homs preserve invertibility. -/
+def invertible.map {R : Type*} {S : Type*} {F : Type*} [mul_one_class R] [mul_one_class S]
+  [monoid_hom_class F R S] (f : F) (r : R) [invertible r] :
   invertible (f r) :=
 { inv_of := f (⅟r),
-  inv_of_mul_self := by rw [← f.map_mul, inv_of_mul_self, f.map_one],
-  mul_inv_of_self := by rw [← f.map_mul, mul_inv_of_self, f.map_one] }
+  inv_of_mul_self := by rw [←map_mul, inv_of_mul_self, map_one],
+  mul_inv_of_self := by rw [←map_mul, mul_inv_of_self, map_one] }

src/data/mv_polynomial/invertible.lean

@@ -19,7 +19,7 @@ open mv_polynomial
 noncomputable instance mv_polynomial.invertible_C
   (σ : Type*) {R : Type*} [comm_semiring R] (r : R) [invertible r] :
   invertible (C r : mv_polynomial σ R) :=
-invertible.map (C.to_monoid_hom : R →* mv_polynomial σ R) _
+invertible.map (C : R →+* mv_polynomial σ R) _
 
 /-- A natural number that is invertible when coerced to a commutative semiring `R`
 is also invertible when coerced to any polynomial ring with rational coefficients.

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -155,13 +155,7 @@ def unit_of_det_invertible [invertible A.det] : (matrix n n α)ˣ :=
 
 /-- When lowered to a prop, `matrix.invertible_equiv_det_invertible` forms an `iff`. -/
 lemma is_unit_iff_is_unit_det : is_unit A ↔ is_unit A.det :=
-begin
-  split; rintros ⟨x, hx⟩; refine @is_unit_of_invertible _ _ _ (id _),
-  { haveI : invertible A := hx.rec x.invertible,
-    apply det_invertible_of_invertible, },
-  { haveI : invertible A.det := hx.rec x.invertible,
-    apply invertible_of_det_invertible, },
-end
+by simp only [← nonempty_invertible_iff_is_unit, (invertible_equiv_det_invertible A).nonempty_congr]
 
 /-! #### Variants of the statements above with `is_unit`-/
 
@@ -380,6 +374,59 @@ begin
   rw [smul_mul, mul_adjugate, units.smul_def, smul_smul, h.coe_inv_mul, one_smul]
 end
 
+/-- `diagonal v` is invertible if `v` is -/
+def diagonal_invertible {α} [non_assoc_semiring α] (v : n → α) [invertible v] :
+  invertible (diagonal v) :=
+invertible.map (diagonal_ring_hom n α) v
+
+lemma inv_of_diagonal_eq {α} [semiring α] (v : n → α) [invertible v] [invertible (diagonal v)] :
+  ⅟(diagonal v) = diagonal (⅟v) :=
+by { letI := diagonal_invertible v, convert (rfl : ⅟(diagonal v) = _) }
+
+/-- `v` is invertible if `diagonal v` is -/
+def invertible_of_diagonal_invertible (v : n → α) [invertible (diagonal v)] : invertible v :=
+{ inv_of := diag (⅟(diagonal v)),
+  inv_of_mul_self := funext $ λ i, begin
+    letI : invertible (diagonal v).det := det_invertible_of_invertible _,
+    rw [inv_of_eq, diag_smul, adjugate_diagonal, diag_diagonal],
+    dsimp,
+    rw [mul_assoc, prod_erase_mul _ _ (finset.mem_univ _), ←det_diagonal],
+    exact mul_inv_of_self _,
+  end,
+  mul_inv_of_self := funext $ λ i, begin
+    letI : invertible (diagonal v).det := det_invertible_of_invertible _,
+    rw [inv_of_eq, diag_smul, adjugate_diagonal, diag_diagonal],
+    dsimp,
+    rw [mul_left_comm, mul_prod_erase _ _ (finset.mem_univ _), ←det_diagonal],
+    exact mul_inv_of_self _,
+  end }
+
+/-- Together `matrix.diagonal_invertible` and `matrix.invertible_of_diagonal_invertible` form an
+equivalence, although both sides of the equiv are subsingleton anyway. -/
+@[simps]
+def diagonal_invertible_equiv_invertible (v : n → α) : invertible (diagonal v) ≃ invertible v :=
+{ to_fun := @invertible_of_diagonal_invertible _ _ _ _ _ _,
+  inv_fun := @diagonal_invertible _ _ _ _ _ _,
+  left_inv := λ _, subsingleton.elim _ _,
+  right_inv := λ _, subsingleton.elim _ _ }
+
+/-- When lowered to a prop, `matrix.diagonal_invertible_equiv_invertible` forms an `iff`. -/
+@[simp] lemma is_unit_diagonal {v : n → α} : is_unit (diagonal v) ↔ is_unit v :=
+by simp only [← nonempty_invertible_iff_is_unit,
+  (diagonal_invertible_equiv_invertible v).nonempty_congr]
+
+lemma inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (ring.inverse v) :=
+begin
+  rw nonsing_inv_eq_ring_inverse,
+  by_cases h : is_unit v,
+  { have := is_unit_diagonal.mpr h,
+    casesI this.nonempty_invertible,
+    casesI h.nonempty_invertible,
+    rw [ring.inverse_invertible, ring.inverse_invertible, inv_of_diagonal_eq], },
+  { have := is_unit_diagonal.not.mpr h,
+    rw [ring.inverse_non_unit _ h, pi.zero_def, diagonal_zero, ring.inverse_non_unit _ this] }
+end
+
 @[simp] lemma inv_inv_inv (A : matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ :=
 begin
   by_cases h : is_unit A.det,

src/ring_theory/algebra_tower.lean

@@ -44,8 +44,8 @@ variables (R S A B)
 If an element `r : R` is invertible in `S`, then it is invertible in `A`. -/
 def invertible.algebra_tower (r : R) [invertible (algebra_map R S r)] :
   invertible (algebra_map R A r) :=
-invertible.copy (invertible.map (algebra_map S A : S →* A) (algebra_map R S r)) (algebra_map R A r)
-  (by rw [ring_hom.coe_monoid_hom, is_scalar_tower.algebra_map_apply R S A])
+invertible.copy (invertible.map (algebra_map S A) (algebra_map R S r)) (algebra_map R A r)
+  (is_scalar_tower.algebra_map_apply R S A r)
 
 /-- A natural number that is invertible when coerced to `R` is also invertible
 when coerced to any `R`-algebra. -/