Trace and determinant extractors

Finite identities used in the three-axes problem.

Main results

• blk_det_formula: det [[A+B, A],[A, A+C]] = det(A(B+C)) + det(B(A+C)) + det(C(A+B)) − det(AB) − det(AC) − det(BC) for 2×2 matrices over a commutative ring.
• trace_extractor: with K = XY − YX, E2(T) := {K,[XT+TX,Y]} − {[X²,Y],[T,Y]} satisfies E2(T) = (2·tr T) • K² (2×2).
• det_extractor: E2(T)·T − 2•(K²·T²) = (2·det T) • K².
• H0_square_zero: if X², Y², Z² vanish then the block matrix H0 vanishes.
• sharpness: in a division ring, u (u⁻²+v⁻²) v = u⁻¹ v + u v⁻¹.
• fox_commutator: for units x, y, x y x⁻¹ y⁻¹ − 1 = (1+x)(y x⁻¹ y⁻¹ + x⁻¹ y⁻¹) − (1+y)(x⁻¹ y⁻¹ + y⁻¹); comaximal_intersection: if u e + w f = 1 then u (1 − e u) = w (f u).
• re_inv_one_add: for z ∈ ℂ with ‖z‖ = 1, z ≠ −1, Re (1+z)⁻¹ = 1/2.
• PM_partial_fractions: (1−2du)/((1−(d+1)u)(1−du)) = (1−d)/(1−(d+1)u) + d/(1−du) (Kassel–Reutenauer, §5.2).

The block matrix blk, the 4 × 4 determinant det4 and M2 are in Formalizations.RingTheory.FreeField.ThreeAxes.Basic.

theorem ThreeAxes.Extractors.blk_det_formula {R : Type u_1} [CommRing R] (A B C : M2 R) : (blk A B C).det = (A * (B + C)).det + (B * (A + C)).det + (C * (A + B)).det - (A * B).det - (A * C).det - (B * C).det

(B) block-determinant formula for H0.

def ThreeAxes.Extractors.cm {R : Type u_1} [CommRing R] (P Q : M2 R) : M2 R

Equations

• ThreeAxes.Extractors.cm P Q = P * Q - Q * P

def ThreeAxes.Extractors.acm {R : Type u_1} [CommRing R] (P Q : M2 R) : M2 R

Equations

• ThreeAxes.Extractors.acm P Q = P * Q + Q * P

def ThreeAxes.Extractors.E2 {R : Type u_1} [CommRing R] (X Y T : M2 R) : M2 R

(E) doubled trace extractor.

Equations

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

theorem ThreeAxes.Extractors.trace_extractor {R : Type u_1} [CommRing R] (X Y T : M2 R) : E2 X Y T = (2 * Matrix.trace T) • (cm X Y * cm X Y)

theorem ThreeAxes.Extractors.det_extractor {R : Type u_1} [CommRing R] (X Y T : M2 R) : E2 X Y T * T - 2 • (cm X Y * cm X Y * (T * T)) = (2 * Matrix.det T) • (cm X Y * cm X Y)

(D) doubled determinant extractor.

theorem ThreeAxes.Extractors.H0_square_zero {R : Type u_1} [CommRing R] (X Y Z : M2 R) (hx : X * X = 0) (hy : Y * Y = 0) (hz : Z * Z = 0) : blk (X * X) (Y * Y) (Z * Z) = 0

(Z) H0 vanishes at square-zero triples.

theorem ThreeAxes.Extractors.PM_partial_fractions {K : Type u_2} [Field K] (d u : K) (h1 : 1 - (d + 1) * u ≠ 0) (h2 : 1 - d * u ≠ 0) : (1 - 2 * d * u) / ((1 - (d + 1) * u) * (1 - d * u)) = (1 - d) / (1 - (d + 1) * u) + d / (1 - d * u)

(P) partial fractions behind the closed form of P_M.

theorem ThreeAxes.Extractors.sharpness {D : Type u_1} [DivisionRing D] (u v : D) (hu : u ≠ 0) (hv : v ≠ 0) : u * (u⁻¹ * u⁻¹ + v⁻¹ * v⁻¹) * v = u⁻¹ * v + u * v⁻¹

(S) two-axis clearing in a division ring.

theorem ThreeAxes.Extractors.fox_commutator {R : Type u_1} [Ring R] (x y : Rˣ) : ↑x * ↑y * ↑x⁻¹ * ↑y⁻¹ - 1 = (1 + ↑x) * (↑y * ↑x⁻¹ * ↑y⁻¹ + ↑x⁻¹ * ↑y⁻¹) - (1 + ↑y) * (↑x⁻¹ * ↑y⁻¹ + ↑y⁻¹)

(F) χ-twisted right Fox decomposition of a commutator (no z-term).

theorem ThreeAxes.Extractors.comaximal_intersection {R : Type u_1} [Ring R] (u w e f : R) (h : u * e + w * f = 1) : u * (1 - e * u) = w * (f * u)

(F) the element of the counterexample lies in uR ∩ wR.

theorem ThreeAxes.Extractors.commutator_eq_bracket {R : Type u_1} [Ring R] (x y : Rˣ) : ↑x * ↑y * ↑x⁻¹ * ↑y⁻¹ - 1 = ((1 + ↑x) * (1 + ↑y) - (1 + ↑y) * (1 + ↑x)) * ↑x⁻¹ * ↑y⁻¹

(F′) minimal form: the commutator binomial is a Lie bracket times units: x y x⁻¹ y⁻¹ − 1 = ((1+x)(1+y) − (1+y)(1+x)) x⁻¹ y⁻¹.

theorem ThreeAxes.Extractors.bracket_comaximal {D : Type u_1} [DivisionRing D] (a b : D) (h : a * b - b * a ≠ 0) : a * (b * (a * b - b * a)⁻¹) - b * (a * (a * b - b * a)⁻¹) = 1

(F″) minimal clearing mechanism: inverting ℓ = ab − ba makes a and b right comaximal.

theorem ThreeAxes.Extractors.re_inv_one_add (z : ℂ) (hz : ‖z‖ = 1) (h : z ≠ -1) : (1 + z)⁻¹.re = 1 / 2

(A) accretivity of simple reciprocals on the unit circle.