Linear algebra for the free-locus obstruction #

Elementary linear-algebra and ring-identity ingredients of the free-locus obstruction to inversion height.

Main results #

woodbury_special, inv_add_inv_two, inv_add_inv_one: ring identities in a division ring (a special case of Woodbury, and two "inverse of r plus inverses" identities).
corank_left_le, corank_right_le: the corank of each diagonal block of fromBlocks A B 0 D is at most the corank of the whole matrix.
corank_unit_sub_le: an invertible matrix minus a matrix of rank ≤ k has corank ≤ k.

theorem FreeLocus.inv_add_inv_one {R : Type u_1} [DivisionRing R] (r a : R) (ha : a ≠ 0) :

(1c) (r + a⁻¹)⁻¹ = a (r a + 1)⁻¹, only a ≠ 0 needed. Mirror image of ThreeAxes.InverseIdentities.one_term_inv, read in the opposite ring.

theorem FreeLocus.inv_add_inv_two {R : Type u_1} [DivisionRing R] (r a b : R) (ha : a ≠ 0) (hb : b ≠ 0) :

(r + a⁻¹ + b⁻¹)⁻¹ = a * (b * r * a + a + b)⁻¹ * b

(1b) (r + a⁻¹ + b⁻¹)⁻¹ = a (b r a + a + b)⁻¹ b, only a, b ≠ 0 needed. This is ThreeAxes.InverseIdentities.three_term_inv with p = b, q = a.

theorem FreeLocus.woodbury_special {R : Type u_1} [DivisionRing R] (x y : R) (hy : y ≠ 0) (hS : y + x * x ≠ 0) :

(1 + x * y⁻¹ * x)⁻¹ = 1 - x * (y + x * x)⁻¹ * x

(1a) Woodbury special case: (1 + x y⁻¹ x)⁻¹ = 1 - x (y + x x)⁻¹ x, for y ≠ 0 and y + x x ≠ 0 (no hypothesis on 1 + x y⁻¹ x is needed).

theorem FreeLocus.corank_left_le {K : Type u_1} [Field K] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] (A : Matrix n n K) (B : Matrix n m K) (D : Matrix m m K) :

(2, left block) corank of A ≤ corank of fromBlocks A B 0 D.

theorem FreeLocus.corank_right_le {K : Type u_1} [Field K] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] (A : Matrix n n K) (B : Matrix n m K) (D : Matrix m m K) :

(2, right block) corank of D ≤ corank of fromBlocks A B 0 D.

theorem FreeLocus.corank_unit_sub_le {K : Type u_1} [Field K] {n : Type u_2} [Fintype n] [DecidableEq n] (U E : Matrix n n K) (hU : IsUnit U) (k : ℕ) (hE : E.rank ≤ k) :

(3) invertible minus rank ≤ k has corank ≤ k.