Inverse of an arrow matrix over a division ring

For d : ι → D with every d τ ≠ 0 and α ω : ι → D, the arrow (bordered diagonal) matrix B = [[diag d, ω], [α, 0]] is invertible when x = Σ_τ α_τ d_τ⁻¹ ω_τ ≠ 0, and the border corner of its inverse is −x⁻¹. So x⁻¹ is minus a corner of the inverse of a linear matrix. Over a division ring Matrix.inv is not available (it needs a commutative ring), so the inverse is given explicitly and checked on both sides.

Main results

• arrow, arrowInv: the matrix and its explicit inverse (Schur complement of diag d, −x).
• arrow_mul_arrowInv, arrowInv_mul_arrow: B * B' = 1 and B' * B = 1.
• arrow_isUnit; arrowInv_corner: B' (inr, inr) = −x⁻¹.

Related

InverseIdentities.fromBlocks_mul_schur has the pivot in the lower-right block and gives a one-sided inverse; here the pivot is the upper-left diagonal block and both products are checked. Over a commutative ring this is a case of Mathlib's Matrix.invOf_fromBlocks₁₁_eq.

def ThreeAxes.ArrowMatrix.arrowSum {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] (d α ω : ι → D) : D

x = Σ_τ α_τ d_τ⁻¹ ω_τ.

Equations

• ThreeAxes.ArrowMatrix.arrowSum d α ω = ∑ τ : ι, α τ * (d τ)⁻¹ * ω τ

def ThreeAxes.ArrowMatrix.arrow {D : Type u_1} [DivisionRing D] {ι : Type u_2} [DecidableEq ι] (d α ω : ι → D) : Matrix (ι ⊕ Unit) (ι ⊕ Unit) D

The arrow matrix [[diag d, ω], [α, 0]], border indexed by Unit.

Equations

• ThreeAxes.ArrowMatrix.arrow d α ω = Matrix.fromBlocks (Matrix.diagonal d) (Matrix.replicateCol Unit ω) (Matrix.replicateRow Unit α) 0

def ThreeAxes.ArrowMatrix.arrowInv {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → D) : Matrix (ι ⊕ Unit) (ι ⊕ Unit) D

The inverse of arrow d α ω.

Equations

• One or more equations did not get rendered due to their size.

theorem ThreeAxes.ArrowMatrix.arrow_mul_arrowInv {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → D) (hd : ∀ (τ : ι), d τ ≠ 0) (hx : arrowSum d α ω ≠ 0) : arrow d α ω * arrowInv d α ω = 1

theorem ThreeAxes.ArrowMatrix.arrowInv_mul_arrow {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → D) (hd : ∀ (τ : ι), d τ ≠ 0) (hx : arrowSum d α ω ≠ 0) : arrowInv d α ω * arrow d α ω = 1

theorem ThreeAxes.ArrowMatrix.arrow_isUnit {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → D) (hd : ∀ (τ : ι), d τ ≠ 0) (hx : arrowSum d α ω ≠ 0) : IsUnit (arrow d α ω)

theorem ThreeAxes.ArrowMatrix.arrowInv_corner {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → D) : arrowInv d α ω (Sum.inr ()) (Sum.inr ()) = -(arrowSum d α ω)⁻¹

The border corner of the inverse is −x⁻¹.