diff --git a/src/algebra/invertible.lean b/src/algebra/invertible.lean index 5515d8d1180eb..19ebbb9f01ec6 100644 --- a/src/algebra/invertible.lean +++ b/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] } diff --git a/src/data/mv_polynomial/invertible.lean b/src/data/mv_polynomial/invertible.lean index 89f5ca9f55b4c..cae1d3c1874bf 100644 --- a/src/data/mv_polynomial/invertible.lean +++ b/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. diff --git a/src/linear_algebra/matrix/nonsingular_inverse.lean b/src/linear_algebra/matrix/nonsingular_inverse.lean index 08c9c5c4c8120..c84571d57cdd1 100644 --- a/src/linear_algebra/matrix/nonsingular_inverse.lean +++ b/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, diff --git a/src/ring_theory/algebra_tower.lean b/src/ring_theory/algebra_tower.lean index 2253f528d4f21..8d019859161ba 100644 --- a/src/ring_theory/algebra_tower.lean +++ b/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. -/