Matrix inverse identities and entrywise bounds

Applying a ring homomorphism f : R →+* S entrywise commutes with taking the inverse of a square matrix, provided f is a local homomorphism (Matrix.map_nonsing_inv). The inverse A⁻¹ = Ring.inverse (det A) • adjugate A is built from the determinant and the adjugate, which commute with every ring homomorphism (RingHom.map_det, RingHom.map_adjugate), and a local homomorphism commutes with Ring.inverse (map_ringInverse).

Locality is needed: ℤ →+* ℚ is not local, and the 1 × 1 matrix 2 over ℤ has inverse 0, while its image in ℚ has inverse 1 / 2. Every ring homomorphism from a field to a nontrivial ring is local, so the statement applies, for instance, to the casts ℚ → ℝ and ℝ → ℂ: an inverse computed over ℚ is the inverse over ℝ.

Matrix.inv_submatrix_mul_row_eq_single normalizes the rows of a matrix whose columns off a pivot set vanish to coordinate vectors, by the inverse of its pivot submatrix.

LinearMap.toMatrix_ringInverse identifies the matrix of an endomorphism's ring inverse.

For invertible matrices A, B over a linearly ordered field, inverse entries bounded by L and entrywise difference bounded by d give |A⁻¹ i j - B⁻¹ i j| ≤ (card ι)² L² d (Matrix.abs_inv_sub_inv_apply_le). This estimate supplies the inverse-entry Hölder modulus. It is adapted from the KLS formalization.

@[simp]

theorem Matrix.map_nonsing_inv {n : Type u_1} {R : Type u_2} {S : Type u_3} {F : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] [CommRing S] [FunLike F R S] [RingHomClass F R S] (f : F) [IsLocalHom f] (A : Matrix n n R) : A⁻¹.map ⇑f = (A.map ⇑f)⁻¹

A local ring homomorphism applied entrywise commutes with the inverse of a square matrix.

theorem Matrix.inv_submatrix_mul_row_eq_single {K : Type u_5} {ι : Type u_6} [CommRing K] [Fintype ι] [DecidableEq ι] {p : ℕ} {x : Matrix (Fin p) ι K} {e : Fin p ↪ ι} {Q : Matrix ι ι K} (he : IsUnit (x.submatrix id ⇑e).det) (hred : ∀ (i : Fin p) (j : ι), (x * Q) i j = if j ∈ Set.range ⇑e then x i j else 0) : ((x.submatrix id ⇑e)⁻¹ * (x * Q)).row = fun (i : Fin p) => Pi.single (e i) 1

If the column change Q kills x off the pivot columns e, then normalizing by the inverse of the pivot matrix turns the rows of x * Q into coordinate vectors.

theorem LinearMap.toMatrix_ringInverse {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (A : M →ₗ[R] M) : (toMatrix b b) (Ring.inverse A) = ((toMatrix b b) A)⁻¹

The matrix of the ring inverse of an endomorphism is the inverse of its matrix.

theorem Matrix.abs_inv_sub_inv_apply_le {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [Field R] [LinearOrder R] [IsStrictOrderedRing R] {A B : Matrix ι ι R} {L d : R} (hA : IsUnit A) (hB : IsUnit B) (ha : ∀ (i j : ι), |A⁻¹ i j| ≤ L) (hb : ∀ (i j : ι), |B⁻¹ i j| ≤ L) (hab : ∀ (i j : ι), |A i j - B i j| ≤ d) (i j : ι) : |A⁻¹ i j - B⁻¹ i j| ≤ ↑(Fintype.card ι) ^ 2 * L ^ 2 * d

Entrywise modulus of the inverse. For invertible A, B over a linearly ordered field whose inverse entries are bounded by L and whose entrywise difference is bounded by d, |A⁻¹ᵢⱼ − B⁻¹ᵢⱼ| ≤ n² L² d with n = card ι.