Unitary transvections

Let σ be a ring endomorphism of a commutative semiring R and Q a square matrix over R, and write B(x, y) = σ(x)ᵀ Q y for the σ-sesquilinear form with Gram matrix Q, semilinear in its first argument. A matrix g preserves B exactly when σ(g)ᵀ Q g = Q. For a vector v and a scalar a, the unitary transvection

τ_{v,a} : x ↦ x + a B(v, x) v,        τ_{v,a} = 1 + a v (σ(v)ᵀ Q)

is Matrix.unitaryTransvection Q σ v a. When v is isotropic, B(v, v) = 0, the map a ↦ τ_{v,a} turns addition into multiplication, and over a commutative ring τ_{v,a} has determinant one. When moreover σ is an involution, the Gram matrix satisfies σ(Q)ᵀ = ε Q, so that B is ε-Hermitian, and a + ε σ(a) = 0, the transvection preserves B. A matrix g preserving B conjugates τ_{v,a} to τ_{g v,a}. That such a g preserves the values of B, and that B is then ε-Hermitian, are Matrix.comp_mulVec_dotProduct_mulVec_mulVec and Matrix.apply_comp_dotProduct_mulVec in TauCeti/LinearAlgebra/Matrix/SesquilinearForm.lean.

For σ the involution x ↦ x ^ q of the field with q² elements and B Hermitian, these are the transvections of the finite special unitary group SU_n(q). The transvections along a fixed isotropic vector form an abelian subgroup, and the conjugation law permutes these subgroups like the isotropic vectors, which is the shape of an Iwasawa structure for the action of the unitary group on the isotropic points of projective space. The special isometry group of B and these transvection groups, indexed by the isotropic points, are in TauCeti/LinearAlgebra/Matrix/SpecialLinearGroup/Isometry/Transvection.lean.

Main definitions

• Matrix.unitaryTransvection: the matrix 1 + a v (σ(v)ᵀ Q).

Main results

• Matrix.unitaryTransvection_mulVec: the action x ↦ x + a B(v, x) v; as a linear map τ_{v,a} is Mathlib's LinearMap.transvection (Matrix.toLin'_unitaryTransvection).
• Matrix.unitaryTransvection_mul_unitaryTransvection: τ_{v,a} τ_{v,b} = τ_{v,a+b} for isotropic v.
• Matrix.det_unitaryTransvection: an isotropic transvection has determinant one.
• Matrix.unitaryTransvection_smul: rescaling the vector, τ_{c v,a} = τ_{v, a c σ(c)}.
• Matrix.mul_unitaryTransvection: the conjugation law g τ_{v,a} = τ_{g v,a} g for g preserving B.
• Matrix.transpose_map_unitaryTransvection_mul_mul: the isometry defect σ(τ_{v,a})ᵀ Q τ_{v,a} - Q = (a + ε σ(a)) (Q v) (σ(v)ᵀ Q) of an isotropic transvection for the ε-Hermitian form B, so that τ_{v,a} preserves B when a + ε σ(a) = 0 (Matrix.transpose_map_unitaryTransvection_mul_mul_self).
• Matrix.exists_eq_unitaryTransvection_smul_iff: over a field, the transvections along a nonzero multiple of v are those along v.

References

• D. E. Taylor, The Geometry of the Classical Groups (1992), the chapter on unitary groups.
• L. C. Grove, Classical Groups and Geometric Algebra, Graduate Studies in Mathematics 39 (2002), the chapters on unitary groups.

def Matrix.unitaryTransvection {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] (Q : Matrix n n R) (σ : R →+* R) (v : n → R) (a : R) : Matrix n n R

The unitary transvection τ_{v,a} = 1 + a v (σ(v)ᵀ Q) along the vector v, for the σ-sesquilinear form B(x, y) = σ(x)ᵀ Q y. It acts by x ↦ x + a B(v, x) v (Matrix.unitaryTransvection_mulVec).

theorem Matrix.unitaryTransvection_def {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] (Q : Matrix n n R) (σ : R →+* R) (v : n → R) (a : R) : Q.unitaryTransvection σ v a = 1 + a • vecMulVec v (vecMul (⇑σ ∘ v) Q)

@[simp]

theorem Matrix.unitaryTransvection_zero {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} : Q.unitaryTransvection σ v 0 = 1

theorem Matrix.unitaryTransvection_mulVec {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} (a : R) (x : n → R) : (Q.unitaryTransvection σ v a).mulVec x = x + (a * ⇑σ ∘ v ⬝ᵥ Q.mulVec x) • v

The unitary transvection τ_{v,a} sends x to x + a B(v, x) v.

theorem Matrix.toLin'_unitaryTransvection {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} (a : R) : toLin' (Q.unitaryTransvection σ v a) = (a • (toBilin' Q) (⇑σ ∘ v)).transvection v

As a linear map, the unitary transvection τ_{v,a} is Mathlib's transvection x ↦ x + f x • v for the linear form f = a B(v, ·).

theorem Matrix.unitaryTransvection_mul_unitaryTransvection {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} (hv : ⇑σ ∘ v ⬝ᵥ Q.mulVec v = 0) (a b : R) : Q.unitaryTransvection σ v a * Q.unitaryTransvection σ v b = Q.unitaryTransvection σ v (a + b)

The parameter of a transvection along an isotropic vector is additive. If B(v, v) = 0, then τ_{v,a} τ_{v,b} = τ_{v,a+b}, so a ↦ τ_{v,a} turns addition into multiplication. Over a commutative ring, where τ_{v,-a} inverts τ_{v,a}, these transvections form a one-parameter group.

theorem Matrix.unitaryTransvection_smul {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} (c a : R) : Q.unitaryTransvection σ (c • v) a = Q.unitaryTransvection σ v (a * c * σ c)

Rescaling the vector of a unitary transvection rescales its parameter by the norm of the scalar: τ_{c v,a} = τ_{v, a c σ(c)}.

theorem Matrix.mul_unitaryTransvection {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} {g : Matrix n n R} (hg : (g.map ⇑σ).transpose * Q * g = Q) (a : R) : g * Q.unitaryTransvection σ v a = Q.unitaryTransvection σ (g.mulVec v) a * g

The conjugation law. A matrix g preserving the form, σ(g)ᵀ Q g = Q, carries the transvection τ_{v,a} to τ_{g v,a}: g τ_{v,a} = τ_{g v,a} g.

theorem Matrix.transpose_map_unitaryTransvection_mul_mul {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} (hσ : Function.Involutive ⇑σ) {ε : R} (hQ : (Q.map ⇑σ).transpose = ε • Q) (hv : ⇑σ ∘ v ⬝ᵥ Q.mulVec v = 0) (a : R) : ((Q.unitaryTransvection σ v a).map ⇑σ).transpose * Q * Q.unitaryTransvection σ v a = Q + (a + ε * σ a) • vecMulVec (Q.mulVec v) (vecMul (⇑σ ∘ v) Q)

The isometry defect of a unitary transvection. Let σ be an involution, let the Gram matrix satisfy σ(Q)ᵀ = ε Q, so that σ(B(x, y)) = ε B(y, x), and let v be isotropic. Then σ(τ_{v,a})ᵀ Q τ_{v,a} = Q + (a + ε σ(a)) (Q v) (σ(v)ᵀ Q).

theorem Matrix.transpose_map_unitaryTransvection_mul_mul_self {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} (hσ : Function.Involutive ⇑σ) {ε : R} (hQ : (Q.map ⇑σ).transpose = ε • Q) (hv : ⇑σ ∘ v ⬝ᵥ Q.mulVec v = 0) {a : R} (ha : a + ε * σ a = 0) : ((Q.unitaryTransvection σ v a).map ⇑σ).transpose * Q * Q.unitaryTransvection σ v a = Q

Unitary transvections are isometries. Let σ be an involution, let the Gram matrix satisfy σ(Q)ᵀ = ε Q, so that σ(B(x, y)) = ε B(y, x), and let v be isotropic. If a + ε σ(a) = 0, then τ_{v,a} preserves the form: σ(τ_{v,a})ᵀ Q τ_{v,a} = Q.

theorem Matrix.det_unitaryTransvection {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] {Q : Matrix n n R} {σ : R →+* R} {v : n → R} (hv : ⇑σ ∘ v ⬝ᵥ Q.mulVec v = 0) (a : R) : (Q.unitaryTransvection σ v a).det = 1

An isotropic transvection has determinant one.

theorem Matrix.exists_eq_unitaryTransvection_smul_iff {n : Type u_2} [Fintype n] [DecidableEq n] {K : Type u_3} [Field K] {Q : Matrix n n K} {σ : K →+* K} {c : K} (hc : c ≠ 0) (v : n → K) (M : Matrix n n K) : (∃ (a : K), M = Q.unitaryTransvection σ (c • v) a) ↔ ∃ (a : K), M = Q.unitaryTransvection σ v a

Along a nonzero multiple c v of v, the unitary transvections are those along v.