The matrices 1 - u ⊗ v

This file develops the matrix calculus for the rank-one perturbations 1 - vecMulVec u v of the identity: their products, the commutation and braid relations, the quadratic relation, the inverse, the determinant, and the resulting element of the general linear group. Everything is stated for plain pairs of vectors, and every hypothesis is a value of one of the pairings v ⬝ᵥ u of the vectors involved.

Main definitions

• TauCeti.oneSubVecMulVecGL: 1 - vecMulVec u v as an element of the general linear group, when its self-pairing v ⬝ᵥ u is t + 1 for a unit t.

Main results

• TauCeti.one_sub_vecMulVec_mul_comm and TauCeti.one_sub_vecMulVec_braid: the commutation and braid relations, from the values of the pairings.
• TauCeti.one_sub_vecMulVec_mul_self: the quadratic relation.
• TauCeti.det_one_sub_vecMulVec and TauCeti.inv_one_sub_vecMulVec: the determinant and the inverse.

theorem TauCeti.one_sub_vecMulVec_mul_one_sub_vecMulVec {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (u₁ v₁ u₂ v₂ : α → R) : (1 - Matrix.vecMulVec u₁ v₁) * (1 - Matrix.vecMulVec u₂ v₂) = 1 - Matrix.vecMulVec u₁ v₁ - Matrix.vecMulVec u₂ v₂ + (v₁ ⬝ᵥ u₂) • Matrix.vecMulVec u₁ v₂

The product of two rank-one perturbations of the identity.

theorem TauCeti.one_sub_vecMulVec_mul_comm {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] {u₁ v₁ u₂ v₂ : α → R} (h₁₂ : v₁ ⬝ᵥ u₂ = 0) (h₂₁ : v₂ ⬝ᵥ u₁ = 0) : (1 - Matrix.vecMulVec u₁ v₁) * (1 - Matrix.vecMulVec u₂ v₂) = (1 - Matrix.vecMulVec u₂ v₂) * (1 - Matrix.vecMulVec u₁ v₁)

Two rank-one perturbations of the identity commute when their cross-pairings vanish.

theorem TauCeti.one_sub_vecMulVec_braid {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] {u₁ v₁ u₂ v₂ : α → R} (h₁ : v₁ ⬝ᵥ u₁ = 1 + v₁ ⬝ᵥ u₂ * v₂ ⬝ᵥ u₁) (h₂ : v₂ ⬝ᵥ u₂ = 1 + v₁ ⬝ᵥ u₂ * v₂ ⬝ᵥ u₁) : (1 - Matrix.vecMulVec u₁ v₁) * (1 - Matrix.vecMulVec u₂ v₂) * (1 - Matrix.vecMulVec u₁ v₁) = (1 - Matrix.vecMulVec u₂ v₂) * (1 - Matrix.vecMulVec u₁ v₁) * (1 - Matrix.vecMulVec u₂ v₂)

Two rank-one perturbations of the identity obey the braid relation when both self-pairings equal one plus the product of the cross-pairings.

theorem TauCeti.one_sub_vecMulVec_mul_self {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (t : R) {u v : α → R} (h : v ⬝ᵥ u = t + 1) : (1 - Matrix.vecMulVec u v) * (1 - Matrix.vecMulVec u v) = (1 - t) • (1 - Matrix.vecMulVec u v) + t • 1

The quadratic relation for a rank-one perturbation of the identity whose self-pairing is t + 1.

theorem TauCeti.one_sub_vecMulVec_mul_inv {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (t : Rˣ) {u v : α → R} (h : v ⬝ᵥ u = ↑t + 1) : (1 - Matrix.vecMulVec u v) * (1 - ↑t⁻¹ • Matrix.vecMulVec u v) = 1

A right inverse for a rank-one perturbation of the identity whose self-pairing is t + 1.

theorem TauCeti.one_sub_vecMulVec_inv_mul {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (t : Rˣ) {u v : α → R} (h : v ⬝ᵥ u = ↑t + 1) : (1 - ↑t⁻¹ • Matrix.vecMulVec u v) * (1 - Matrix.vecMulVec u v) = 1

A left inverse for a rank-one perturbation of the identity whose self-pairing is t + 1.

@[simp]

theorem TauCeti.det_one_sub_vecMulVec {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (u v : α → R) : (1 - Matrix.vecMulVec u v).det = 1 - v ⬝ᵥ u

The determinant of a rank-one perturbation of the identity in terms of its self-pairing.

def TauCeti.oneSubVecMulVecGL {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (t : Rˣ) (u v : α → R) (h : v ⬝ᵥ u = ↑t + 1) : GL α R

A rank-one perturbation of the identity as an element of the general linear group, when its self-pairing is t + 1.

Equations

• TauCeti.oneSubVecMulVecGL t u v h = { val := 1 - Matrix.vecMulVec u v, inv := 1 - ↑t⁻¹ • Matrix.vecMulVec u v, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem TauCeti.coe_oneSubVecMulVecGL {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (t : Rˣ) (u v : α → R) (h : v ⬝ᵥ u = ↑t + 1) : ↑(oneSubVecMulVecGL t u v h) = 1 - Matrix.vecMulVec u v

The matrix underlying TauCeti.oneSubVecMulVecGL.

theorem TauCeti.inv_one_sub_vecMulVec {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (t : Rˣ) {u v : α → R} (h : v ⬝ᵥ u = ↑t + 1) : (1 - Matrix.vecMulVec u v)⁻¹ = 1 - ↑t⁻¹ • Matrix.vecMulVec u v

The inverse of a rank-one perturbation of the identity whose self-pairing is t + 1.

This is not a simp lemma: the unit t occurs only in the right-hand side and in the hypothesis, so simp cannot infer it from the left-hand side. Consumers that fix t — such as TauCeti.KnotTheory.inv_reducedBurauColMatrix — carry the simp attribute instead.