Inverse identities of the three-axes problem over a division ring

Exact versions, over an arbitrary division ring D (no commutativity), of the inversion identities of the three-axes problem that were only checked numerically.

Main results

• three_term_inv (Lemma 7.4, case n′ = 2; "A16"): (p⁻¹ + q⁻¹ + r)⁻¹ = q (p r q + p + q)⁻¹ p; one_term_inv: (d⁻¹ + r)⁻¹ = (1 + d r)⁻¹ d.
• schur_two: the 2 × 2 block inverse with a pivot a and Schur complement S, over any ring.
• harmonicMatrix: H a b c = !![a + b, a; a, a + c]. With s = a⁻¹ + b⁻¹ + c⁻¹ ≠ 0: harmonic_isUnit; woodbury_corner (§5.1): s⁻¹ = b − b (H⁻¹)₁₁ b; woodbury_sum (Lemma 7.6(1)): s⁻¹ = a − (a a) H⁻¹ (a a)ᵀ.
• intermediate_inv (Lemma 7.4, case n′ = 3, up to a permutation): for M = !![d₃, d₂; −d₁, d₁ r d₂ + d₁ + d₂], (d₁⁻¹ + d₂⁻¹ + d₃⁻¹ + r)⁻¹ = d₂ (M⁻¹)₂₂ d₁.
• fromBlocks_mul_schur: block inverse of fromBlocks A B C E from right inverses of E and of the Schur complement S = A − B E⁻¹ C, over any ring.
• compression_schur, compression_inv (Lemma 7.4): for M = [[Y, d₁ 𝟙ᵀ], [−𝟙 d₂, diag d]] with Y = d₁ r d₂ + d₁ + d₂ and f = d₁⁻¹ + d₂⁻¹ + Σ dᵢ⁻¹ + r, the Schur complement of diag d is d₁ f d₂ and f⁻¹ = d₂ (M⁻¹)₁₁ d₁.
• chain_mul_inv, chain_inv_corner (§3.4 and Lemma 3.5): the upper bidiagonal chain C with ℓ 0, …, ℓ q on the diagonal and −a 0, …, −a (q−1) above it has the explicit inverse chainInv, and (C⁻¹)_{0,q} = ℓ 0⁻¹ a 0 ℓ 1⁻¹ ⋯ a (q−1) ℓ q⁻¹ (chainProd), for every q.
• cycleMatrix_inv ((6.1)/(6.2)): for the cyclic d × d matrix F̂_d with p₁, …, p_d on the diagonal, c on the superdiagonal and in position (d, 1), (F̂_d⁻¹)₁₁ = [p₁ + (−1)^{d−1} c p₂⁻¹ c ⋯ p_d⁻¹ c]⁻¹, for every d ≥ 2; cycle_inv is the block form F̂_d = [[p₁, c e₁ᵀ], [c e_{d−1}, T_d]] with the explicit block inverse (2.2).

Matrix inverses are ⅟M for an arbitrary Invertible M instance; existence is proved separately (IsUnit), using that matrix rings over a division ring are Dedekind-finite.

Related

• three_term_eq with r = 0 is Mathlib's inv_add_inv' (invOf_add_invOf for Invertible).
• woodbury_corner and woodbury_sum are scalar readings of the Woodbury identity for the harmonic matrix diag(b, c) + a 𝟙 𝟙ᵀ. Mathlib has Woodbury for matrices over a Ring as Matrix.invOf_add_mul_mul (⅟ version; the ⁻¹ version Matrix.add_mul_mul_inv_eq_sub is stated over a CommRing).
• schur_two and fromBlocks_mul_schur are noncommutative versions, with one-sided inverses, of Mathlib's block inverse through a Schur complement, Matrix.fromBlocks₂₂Invertible and Matrix.invOf_fromBlocks₂₂_eq (also Matrix.fromBlocks₁₁Invertible), which are stated over a CommRing.

Scalar identities

theorem ThreeAxes.InverseIdentities.three_term_eq {D : Type u_1} [DivisionRing D] (p q r : D) (hp : p ≠ 0) (hq : q ≠ 0) : p⁻¹ + q⁻¹ + r = p⁻¹ * (p * r * q + p + q) * q⁻¹

theorem ThreeAxes.InverseIdentities.three_term_inv {D : Type u_1} [DivisionRing D] (p q r : D) (hp : p ≠ 0) (hq : q ≠ 0) : (p⁻¹ + q⁻¹ + r)⁻¹ = q * (p * r * q + p + q)⁻¹ * p

A16. (p⁻¹ + q⁻¹ + r)⁻¹ = q (p r q + p + q)⁻¹ p in a division ring.

theorem ThreeAxes.InverseIdentities.three_term_ne_zero_iff {D : Type u_1} [DivisionRing D] (p q r : D) (hp : p ≠ 0) (hq : q ≠ 0) : p⁻¹ + q⁻¹ + r ≠ 0 ↔ p * r * q + p + q ≠ 0

theorem ThreeAxes.InverseIdentities.one_term_inv {D : Type u_1} [DivisionRing D] (d r : D) (hd : d ≠ 0) : (d⁻¹ + r)⁻¹ = (1 + d * r)⁻¹ * d

One pure summand: (d⁻¹ + r)⁻¹ = (1 + d r)⁻¹ d.

2 × 2 Schur complement

theorem ThreeAxes.InverseIdentities.schur_two {R : Type u_2} [Ring R] (a b c S ai Si : R) (ha : a * ai = 1) (hS : S * Si = 1) : !![a, b; c, S + c * ai * b] * !![ai + ai * b * Si * c * ai, -(ai * b * Si); -(Si * c * ai), Si] = 1

The 2 × 2 block inverse with pivot a and Schur complement S, over any ring.

The harmonic matrix and the Woodbury identity

def ThreeAxes.InverseIdentities.harmonicMatrix {D : Type u_1} [DivisionRing D] (a b c : D) : Matrix (Fin 2) (Fin 2) D

H a b c = !![a + b, a; a, a + c] = diag(b, c) + a 𝟙 𝟙ᵀ.

Equations

• ThreeAxes.InverseIdentities.harmonicMatrix a b c = !![a + b, a; a, a + c]

noncomputable def ThreeAxes.InverseIdentities.harmonicInv {D : Type u_1} [DivisionRing D] (a b c : D) : Matrix (Fin 2) (Fin 2) D

An explicit inverse of harmonicMatrix a b c, through H = !![1, 1; 0, 1] * K with K = !![b, −c; a, a + c], whose Schur complement is a s c, s = a⁻¹ + b⁻¹ + c⁻¹.

Equations

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

theorem ThreeAxes.InverseIdentities.harmonic_mul_inv {D : Type u_1} [DivisionRing D] (a b c : D) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hs : a⁻¹ + b⁻¹ + c⁻¹ ≠ 0) : harmonicMatrix a b c * harmonicInv a b c = 1

theorem ThreeAxes.InverseIdentities.harmonic_isUnit {D : Type u_1} [DivisionRing D] (a b c : D) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hs : a⁻¹ + b⁻¹ + c⁻¹ ≠ 0) : IsUnit (harmonicMatrix a b c)

theorem ThreeAxes.InverseIdentities.woodbury_corner {D : Type u_1} [DivisionRing D] (a b c : D) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hs : a⁻¹ + b⁻¹ + c⁻¹ ≠ 0) [Invertible (harmonicMatrix a b c)] : b - b * ⅟(harmonicMatrix a b c) 0 0 * b = (a⁻¹ + b⁻¹ + c⁻¹)⁻¹

§5.1. s⁻¹ = b − b (H⁻¹)₁₁ b with H = diag(b, c) + a 𝟙 𝟙ᵀ and s = a⁻¹ + b⁻¹ + c⁻¹ (in the paper a = u², b = v², c = w²).

theorem ThreeAxes.InverseIdentities.woodbury_sum {D : Type u_1} [DivisionRing D] (a b c : D) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hs : a⁻¹ + b⁻¹ + c⁻¹ ≠ 0) [Invertible (harmonicMatrix a b c)] : a - (a * ⅟(harmonicMatrix a b c) 0 0 * a + a * ⅟(harmonicMatrix a b c) 0 1 * a + a * ⅟(harmonicMatrix a b c) 1 0 * a + a * ⅟(harmonicMatrix a b c) 1 1 * a) = (a⁻¹ + b⁻¹ + c⁻¹)⁻¹

Lemma 7.6(1). s⁻¹ = a − (a a) H⁻¹ (a a)ᵀ with H = !![a + b, a; a, a + c] and s = a⁻¹ + b⁻¹ + c⁻¹ (in the paper a = d₁, b = d₂, c = d₃).

Intermediate inverse (Lemma 7.4, case n′ = 3)

def ThreeAxes.InverseIdentities.intermediateMatrix {D : Type u_1} [DivisionRing D] (d₁ d₂ d₃ r : D) : Matrix (Fin 2) (Fin 2) D

The matrix !![d₃, d₂; −d₁, d₁ r d₂ + d₁ + d₂] of the intermediate inverse.

Equations

• ThreeAxes.InverseIdentities.intermediateMatrix d₁ d₂ d₃ r = !![d₃, d₂; -d₁, d₁ * r * d₂ + d₁ + d₂]

theorem ThreeAxes.InverseIdentities.intermediate_schur {D : Type u_1} [DivisionRing D] (d₁ d₂ d₃ r : D) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : d₁ * r * d₂ + d₁ + d₂ = d₁ * (d₁⁻¹ + d₂⁻¹ + d₃⁻¹ + r) * d₂ + -d₁ * d₃⁻¹ * d₂

theorem ThreeAxes.InverseIdentities.intermediate_mul_inv {D : Type u_1} [DivisionRing D] (d₁ d₂ d₃ r : D) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) (h₃ : d₃ ≠ 0) (hf : d₁⁻¹ + d₂⁻¹ + d₃⁻¹ + r ≠ 0) : (intermediateMatrix d₁ d₂ d₃ r * have S := d₁ * (d₁⁻¹ + d₂⁻¹ + d₃⁻¹ + r) * d₂; !![d₃⁻¹ + d₃⁻¹ * d₂ * S⁻¹ * -d₁ * d₃⁻¹, -(d₃⁻¹ * d₂ * S⁻¹); -(S⁻¹ * -d₁ * d₃⁻¹), S⁻¹]) = 1

theorem ThreeAxes.InverseIdentities.intermediate_isUnit {D : Type u_1} [DivisionRing D] (d₁ d₂ d₃ r : D) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) (h₃ : d₃ ≠ 0) (hf : d₁⁻¹ + d₂⁻¹ + d₃⁻¹ + r ≠ 0) : IsUnit (intermediateMatrix d₁ d₂ d₃ r)

theorem ThreeAxes.InverseIdentities.intermediate_inv {D : Type u_1} [DivisionRing D] (d₁ d₂ d₃ r : D) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) (h₃ : d₃ ≠ 0) (hf : d₁⁻¹ + d₂⁻¹ + d₃⁻¹ + r ≠ 0) [Invertible (intermediateMatrix d₁ d₂ d₃ r)] : d₂ * ⅟(intermediateMatrix d₁ d₂ d₃ r) 1 1 * d₁ = (d₁⁻¹ + d₂⁻¹ + d₃⁻¹ + r)⁻¹

Intermediate inverse (Lemma 7.4, case n′ = 3). (s₃ + r)⁻¹ = d₂ (M⁻¹)₂₂ d₁ with s₃ = d₁⁻¹ + d₂⁻¹ + d₃⁻¹ and M = !![d₃, d₂; −d₁, d₁ r d₂ + d₁ + d₂].

Block Schur complement over a noncommutative ring

theorem ThreeAxes.InverseIdentities.fromBlocks_mul_schur {R : Type u_2} [Ring R] {m : Type u_3} {n : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (S Si : Matrix m m R) (B : Matrix m n R) (C : Matrix n m R) (E Ei : Matrix n n R) (hE : E * Ei = 1) (hS : S * Si = 1) : Matrix.fromBlocks (S + B * Ei * C) B C E * Matrix.fromBlocks Si (-(Si * B * Ei)) (-(Ei * C * Si)) (Ei + Ei * C * Si * B * Ei) = 1

Block inverse of fromBlocks (S + B E⁻¹ C) B C E from right inverses Ei of E and Si of the Schur complement S, over any ring.

Lemma 7.4: compression

def ThreeAxes.InverseIdentities.compressionMatrix {D : Type u_1} [DivisionRing D] {ι : Type u_2} [DecidableEq ι] (d₁ d₂ r : D) (d : ι → D) : Matrix (Fin 1 ⊕ ι) (Fin 1 ⊕ ι) D

M = [[Y, d₁ 𝟙ᵀ], [−𝟙 d₂, diag d]] with Y = d₁ r d₂ + d₁ + d₂ (Lemma 7.4).

Equations

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

theorem ThreeAxes.InverseIdentities.compression_schur {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d₁ d₂ r : D) (d : ι → D) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : ((Matrix.of fun (x x_1 : Fin 1) => d₁ * r * d₂ + d₁ + d₂) - ((Matrix.of fun (x : Fin 1) (x_1 : ι) => d₁) * Matrix.diagonal fun (i : ι) => (d i)⁻¹) * Matrix.of fun (x : ι) (x_1 : Fin 1) => -d₂) = Matrix.of fun (x x_1 : Fin 1) => d₁ * (d₁⁻¹ + d₂⁻¹ + ∑ i : ι, (d i)⁻¹ + r) * d₂

The Schur complement of diag d in compressionMatrix is d₁ f d₂, f = d₁⁻¹ + d₂⁻¹ + Σ dᵢ⁻¹ + r.

theorem ThreeAxes.InverseIdentities.compression_mul_inv {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d₁ d₂ r : D) (d : ι → D) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) (hd : ∀ (i : ι), d i ≠ 0) (hf : d₁⁻¹ + d₂⁻¹ + ∑ i : ι, (d i)⁻¹ + r ≠ 0) : (compressionMatrix d₁ d₂ r d * have Si := Matrix.of fun (x x_1 : Fin 1) => (d₁ * (d₁⁻¹ + d₂⁻¹ + ∑ i : ι, (d i)⁻¹ + r) * d₂)⁻¹; have B := Matrix.of fun (x : Fin 1) (x_1 : ι) => d₁; have C := Matrix.of fun (x : ι) (x_1 : Fin 1) => -d₂; have Ei := Matrix.diagonal fun (i : ι) => (d i)⁻¹; Matrix.fromBlocks Si (-(Si * B * Ei)) (-(Ei * C * Si)) (Ei + Ei * C * Si * B * Ei)) = 1

theorem ThreeAxes.InverseIdentities.compression_isUnit {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d₁ d₂ r : D) (d : ι → D) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) (hd : ∀ (i : ι), d i ≠ 0) (hf : d₁⁻¹ + d₂⁻¹ + ∑ i : ι, (d i)⁻¹ + r ≠ 0) : IsUnit (compressionMatrix d₁ d₂ r d)

theorem ThreeAxes.InverseIdentities.compression_inv {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d₁ d₂ r : D) (d : ι → D) (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) (hd : ∀ (i : ι), d i ≠ 0) (hf : d₁⁻¹ + d₂⁻¹ + ∑ i : ι, (d i)⁻¹ + r ≠ 0) [Invertible (compressionMatrix d₁ d₂ r d)] : d₂ * ⅟(compressionMatrix d₁ d₂ r d) (Sum.inl 0) (Sum.inl 0) * d₁ = (d₁⁻¹ + d₂⁻¹ + ∑ i : ι, (d i)⁻¹ + r)⁻¹

Lemma 7.4. f⁻¹ = d₂ (M⁻¹)₁₁ d₁ for f = d₁⁻¹ + d₂⁻¹ + Σ dᵢ⁻¹ + r.

Bidiagonal chains (§3.4, Lemma 3.5)

noncomputable def ThreeAxes.InverseIdentities.chainProd {D : Type u_1} [DivisionRing D] (ℓ a : ℕ → D) : ℕ → ℕ → D

chainProd ℓ a i n = ℓ i⁻¹ a i ℓ (i+1)⁻¹ a (i+1) ⋯ a (i+n−1) ℓ (i+n)⁻¹.

Equations

• ThreeAxes.InverseIdentities.chainProd ℓ a x✝ 0 = (ℓ x✝)⁻¹
• ThreeAxes.InverseIdentities.chainProd ℓ a x✝ n.succ = (ℓ x✝)⁻¹ * a x✝ * ThreeAxes.InverseIdentities.chainProd ℓ a (x✝ + 1) n

def ThreeAxes.InverseIdentities.chain {D : Type u_1} [DivisionRing D] (q : ℕ) (ℓ a : ℕ → D) : Matrix (Fin q) (Fin q) D

The upper bidiagonal chain: ℓ i on the diagonal and −a i at (i, i + 1).

Equations

• ThreeAxes.InverseIdentities.chain q ℓ a = Matrix.of fun (i j : Fin q) => if ↑j = ↑i then ℓ ↑i else if ↑j = ↑i + 1 then -a ↑i else 0

noncomputable def ThreeAxes.InverseIdentities.chainInv {D : Type u_1} [DivisionRing D] (q : ℕ) (ℓ a : ℕ → D) : Matrix (Fin q) (Fin q) D

The explicit inverse of chain q ℓ a: entry (i, j) is chainProd ℓ a i (j − i) for i ≤ j.

Equations

• ThreeAxes.InverseIdentities.chainInv q ℓ a = Matrix.of fun (i j : Fin q) => if ↑i ≤ ↑j then ThreeAxes.InverseIdentities.chainProd ℓ a (↑i) (↑j - ↑i) else 0

theorem ThreeAxes.InverseIdentities.chain_row {D : Type u_1} [DivisionRing D] (ℓ a : ℕ → D) (hℓ : ∀ (i : ℕ), ℓ i ≠ 0) (q I J : ℕ) (hI : I < q) (hJ : J < q) : (∑ k ∈ Finset.range q, (if k = I then ℓ I else if k = I + 1 then -a I else 0) * if k ≤ J then chainProd ℓ a k (J - k) else 0) = if I = J then 1 else 0

theorem ThreeAxes.InverseIdentities.chain_mul_inv {D : Type u_1} [DivisionRing D] (q : ℕ) (ℓ a : ℕ → D) (hℓ : ∀ (i : ℕ), ℓ i ≠ 0) : chain q ℓ a * chainInv q ℓ a = 1

theorem ThreeAxes.InverseIdentities.chain_isUnit {D : Type u_1} [DivisionRing D] (q : ℕ) (ℓ a : ℕ → D) (hℓ : ∀ (i : ℕ), ℓ i ≠ 0) : IsUnit (chain q ℓ a)

theorem ThreeAxes.InverseIdentities.chain_inv_corner {D : Type u_1} [DivisionRing D] (q : ℕ) (ℓ a : ℕ → D) (hℓ : ∀ (i : ℕ), ℓ i ≠ 0) [Invertible (chain (q + 1) ℓ a)] : ⅟(chain (q + 1) ℓ a) 0 (Fin.last q) = chainProd ℓ a 0 q

Chain inverse (§3.4, Lemma 3.5). For the (q+1) × (q+1) upper bidiagonal chain with ℓ 0, …, ℓ q on the diagonal and −a 0, …, −a (q−1) above it, (C⁻¹)_{0,q} = ℓ 0⁻¹ a 0 ℓ 1⁻¹ ⋯ a (q−1) ℓ q⁻¹.

theorem ThreeAxes.InverseIdentities.chainProd_neg {D : Type u_1} [DivisionRing D] (ℓ : ℕ → D) (c : D) (i n : ℕ) : chainProd ℓ (fun (x : ℕ) => -c) i n = (-1) ^ n * chainProd ℓ (fun (x : ℕ) => c) i n

The cyclic witness, (6.1)/(6.2)

def ThreeAxes.InverseIdentities.cycleBlocks {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) : Matrix (Fin 1 ⊕ Fin (n + 1)) (Fin 1 ⊕ Fin (n + 1)) D

F̂_d for d = n + 2 in the block form of the proof of (6.1): F̂_d = [[p₁, c e₁ᵀ], [c e_{d−1}, T_d]], with T_d upper bidiagonal, p₂, …, p_d on the diagonal and c above it (chain with a = −c). Here p k is p_{k+1}. Up to the reindexing Fin 1 ⊕ Fin (d − 1) ≃ Fin d, this is the matrix with p₁, …, p_d on the diagonal, c on the superdiagonal and c in position (d, 1).

Equations

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

def ThreeAxes.InverseIdentities.cycleMatrix {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) : Matrix (Fin (n + 2)) (Fin (n + 2)) D

F̂_d for d = n + 2 as a d × d matrix (0-indexed): p i on the diagonal, c on the superdiagonal and c in position (d − 1, 0).

Equations

• ThreeAxes.InverseIdentities.cycleMatrix n p c = Matrix.of fun (i j : Fin (n + 2)) => if ↑j = ↑i then p ↑i else if ↑j = ↑i + 1 then c else if ↑i = n + 1 ∧ ↑j = 0 then c else 0

def ThreeAxes.InverseIdentities.cycleEquiv (n : ℕ) : Fin 1 ⊕ Fin (n + 1) ≃ Fin (n + 2)

The reindexing Fin 1 ⊕ Fin (n + 1) ≃ Fin (n + 2).

Equations

• ThreeAxes.InverseIdentities.cycleEquiv n = finSumFinEquiv.trans (finCongr ⋯)

theorem ThreeAxes.InverseIdentities.cycleBlocks_eq_submatrix {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) : cycleBlocks n p c = (cycleMatrix n p c).submatrix ⇑(cycleEquiv n) ⇑(cycleEquiv n)

theorem ThreeAxes.InverseIdentities.cycle_schur {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) : ((Matrix.of fun (x x_1 : Fin 1) => p 0) - ((Matrix.of fun (x : Fin 1) (j : Fin (n + 1)) => if j = 0 then c else 0) * chainInv (n + 1) (fun (k : ℕ) => p (k + 1)) fun (x : ℕ) => -c) * Matrix.of fun (i : Fin (n + 1)) (x : Fin 1) => if i = Fin.last n then c else 0) = Matrix.of fun (x x_1 : Fin 1) => p 0 - c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => -c) 0 n * c

The Schur complement of T_d in F̂_d: σ = p₁ − c (T_d⁻¹)_{1,d−1} c.

noncomputable def ThreeAxes.InverseIdentities.cycleBlocksInv {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) : Matrix (Fin 1 ⊕ Fin (n + 1)) (Fin 1 ⊕ Fin (n + 1)) D

The block inverse (2.2) of cycleBlocks.

Equations

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

theorem ThreeAxes.InverseIdentities.cycle_mul_inv {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) (hp : ∀ (k : ℕ), p (k + 1) ≠ 0) (hσ : p 0 - c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => -c) 0 n * c ≠ 0) : cycleBlocks n p c * cycleBlocksInv n p c = 1

theorem ThreeAxes.InverseIdentities.cycle_isUnit {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) (hp : ∀ (k : ℕ), p (k + 1) ≠ 0) (hσ : p 0 - c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => -c) 0 n * c ≠ 0) : IsUnit (cycleBlocks n p c)

theorem ThreeAxes.InverseIdentities.cycle_schur_sign {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) : p 0 - c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => -c) 0 n * c = p 0 + (-1) ^ (n + 1) * (c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => c) 0 n * c)

The sign in (2.1): p₁ − c (T_d⁻¹)_{1,d−1} c = p₁ + (−1)^{d−1} c p₂⁻¹ c ⋯ p_d⁻¹ c.

theorem ThreeAxes.InverseIdentities.cycle_inv {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) (hp : ∀ (k : ℕ), p (k + 1) ≠ 0) (hσ : p 0 - c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => -c) 0 n * c ≠ 0) [Invertible (cycleBlocks n p c)] : ⅟(cycleBlocks n p c) (Sum.inl 0) (Sum.inl 0) = (p 0 + (-1) ^ (n + 1) * (c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => c) 0 n * c))⁻¹

(6.1)/(6.2), block form. ρ_d = (F̂_d⁻¹)₁₁ = σ⁻¹ = [p₁ + (−1)^{d−1} c p₂⁻¹ c p₃⁻¹ c ⋯ p_d⁻¹ c]⁻¹ (d = n + 2; chainProd _ (fun _ => c) 0 n = p₂⁻¹ c p₃⁻¹ ⋯ c p_d⁻¹).

theorem ThreeAxes.InverseIdentities.cycleMatrix_eq_submatrix {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) : cycleMatrix n p c = (cycleBlocks n p c).submatrix ⇑(cycleEquiv n).symm ⇑(cycleEquiv n).symm

theorem ThreeAxes.InverseIdentities.cycleEquiv_symm_zero (n : ℕ) : (cycleEquiv n).symm 0 = Sum.inl 0

theorem ThreeAxes.InverseIdentities.cycleMatrix_mul_inv {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) (hp : ∀ (k : ℕ), p (k + 1) ≠ 0) (hσ : p 0 - c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => -c) 0 n * c ≠ 0) : cycleMatrix n p c * (cycleBlocksInv n p c).submatrix ⇑(cycleEquiv n).symm ⇑(cycleEquiv n).symm = 1

theorem ThreeAxes.InverseIdentities.cycleMatrix_isUnit {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) (hp : ∀ (k : ℕ), p (k + 1) ≠ 0) (hσ : p 0 - c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => -c) 0 n * c ≠ 0) : IsUnit (cycleMatrix n p c)

theorem ThreeAxes.InverseIdentities.cycleMatrix_inv {D : Type u_1} [DivisionRing D] (n : ℕ) (p : ℕ → D) (c : D) (hp : ∀ (k : ℕ), p (k + 1) ≠ 0) (hσ : p 0 - c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => -c) 0 n * c ≠ 0) [Invertible (cycleMatrix n p c)] : ⅟(cycleMatrix n p c) 0 0 = (p 0 + (-1) ^ (n + 1) * (c * chainProd (fun (k : ℕ) => p (k + 1)) (fun (x : ℕ) => c) 0 n * c))⁻¹

(6.1). For the cyclic d × d matrix F̂_d (d = n + 2) with p₁, …, p_d on the diagonal, c on the superdiagonal and c in position (d, 1), over a division ring: ρ_d = (F̂_d⁻¹)₁₁ = [p₁ + (−1)^{d−1} c p₂⁻¹ c p₃⁻¹ c ⋯ p_d⁻¹ c]⁻¹, provided the p_j (j ≥ 2) and the Schur complement are nonzero.