Reflection matrices for the standard symmetric form

The reflection of Rⁿ in the hyperplane orthogonal to a vector v has the matrix 1 - c • vecMulVec v v, where the scalar c satisfies c * (v ⬝ᵥ v) = 2. Carrying the scalar as data rather than as 2 * ⅟(v ⬝ᵥ v) makes the construction available over any commutative ring in which the norm of v happens to be invertible, makes it visibly natural in the coefficient ring, and makes the invariance of a reflection under rescaling its vector a one-line computation: putting μ²c on the unscaled-vector side gives the same matrix as putting c on the side whose vector is scaled by μ.

Products of two such matrices are exactly the generators of the special orthogonal group supplied by TauCeti.closure_reflection_mul_eq_matrixSpecialOrthogonalGroup, once toMatrix'_reflection identifies the coordinate matrix of the reflection of the standard quadratic form with reflectionMatrix. They are packaged here as TauCeti.reflectionPair.

The last and largest section of the file builds one-parameter families joining such a product to the identity. Over an algebraically closed field of characteristic different from two, exists_laurentPath_reflectionMatrix_mul produces for every product of two reflections a single special orthogonal matrix over the Laurent polynomials K[T;T⁻¹] together with two units a and b of K, such that specializing the parameter T to a gives the identity and specializing it to b gives the given product; a specialization is any K-algebra map K[T;T⁻¹] →ₐ[K] K, so the units are exactly the admissible parameter values. The family reflects first in v and then in a vector moving through the plane spanned by v and w, chosen so that the moving vector has invertible norm throughout, and the two parameters are those at which the moving vector becomes proportional to v, respectively to w. Consuming these families is what proves the special orthogonal group geometrically connected: an idempotent regular function on the group is constant once right translation by every rational point fixes it, a point joined to the identity by such a family fixes every idempotent, and the generation theorem reduces the rational points to be handled to the products of two reflections.

Main declarations

• TauCeti.reflectionMatrix: the matrix of a reflection, with its normalizing scalar as data.
• TauCeti.reflectionPair: the product of two reflections, as a special orthogonal matrix.
• TauCeti.toMatrix'_reflection: reflectionMatrix is the coordinate matrix of the reflection of the standard quadratic form.
• TauCeti.exists_laurentPath_reflectionMatrix_mul: over an algebraically closed field of characteristic different from two, every product of two reflections is joined to the identity by a one-parameter family of special orthogonal matrices over the Laurent polynomials.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.
• J. S. Milne, Algebraic Groups (2017), §2.3.

def TauCeti.reflectionMatrix {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] (v : n → R) (c : R) : Matrix n n R

The matrix of the reflection of Rⁿ in the hyperplane orthogonal to v, for a scalar c playing the role of 2 / (v ⬝ᵥ v). It is a reflection precisely when c * (v ⬝ᵥ v) = 2, which is not part of the definition.

Equations

• TauCeti.reflectionMatrix v c = 1 - c • Matrix.vecMulVec v v

@[simp]

theorem TauCeti.reflectionMatrix_apply {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] (v : n → R) (c : R) (i j : n) : reflectionMatrix v c i j = (if i = j then 1 else 0) - c * (v i * v j)

@[simp]

theorem TauCeti.transpose_reflectionMatrix {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] (v : n → R) (c : R) : (reflectionMatrix v c).transpose = reflectionMatrix v c

@[simp]

theorem TauCeti.map_reflectionMatrix {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] {S : Type w} [CommRing S] (f : R →+* S) (v : n → R) (c : R) : (reflectionMatrix v c).map ⇑f = reflectionMatrix (⇑f ∘ v) (f c)

Reflection matrices are natural in the coefficient ring.

theorem TauCeti.reflectionMatrix_smul {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] (v : n → R) (c μ : R) : reflectionMatrix (fun (i : n) => μ * v i) c = reflectionMatrix v (μ * μ * c)

Scaling the vector by μ with scalar c gives the same matrix as keeping the vector unchanged and using scalar μ²c.

theorem TauCeti.reflectionMatrix_eq_one_sub_vecMulVec {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] (v : n → R) (c : R) : reflectionMatrix v c = 1 - Matrix.vecMulVec (c • v) v

A reflection matrix is a rank-one perturbation of the identity, so the calculus of TauCeti.LinearAlgebra.Matrix.OneSubVecMulVec applies to it.

@[simp]

theorem TauCeti.reflectionMatrix_mul_self {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] [Fintype n] {v : n → R} {c : R} (hc : c * v ⬝ᵥ v = 2) : reflectionMatrix v c * reflectionMatrix v c = 1

A reflection matrix is an involution.

theorem TauCeti.reflectionMatrix_mem_orthogonalGroup {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] [Fintype n] {v : n → R} {c : R} (hc : c * v ⬝ᵥ v = 2) : reflectionMatrix v c ∈ Matrix.orthogonalGroup n R

A reflection matrix is orthogonal.

@[simp]

theorem TauCeti.det_reflectionMatrix {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] [Fintype n] {v : n → R} {c : R} (hc : c * v ⬝ᵥ v = 2) : (reflectionMatrix v c).det = -1

A reflection matrix has determinant -1.

Comparison with the reflection of the standard quadratic form

theorem TauCeti.toMatrix'_reflection {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] [Fintype n] (v : n → R) [Invertible ((Matrix.toQuadraticForm' 1) v)] : LinearMap.toMatrix' ↑(QuadraticMap.reflection (Matrix.toQuadraticForm' 1) v) = reflectionMatrix v (2 * ⅟((Matrix.toQuadraticForm' 1) v))

The reflection of the standard quadratic form in a vector of invertible norm has reflectionMatrix as its coordinate matrix.

Products of two reflections

theorem TauCeti.reflectionMatrix_mul_mem_specialOrthogonalGroup {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] [Fintype n] {v w : n → R} {c d : R} (hc : c * v ⬝ᵥ v = 2) (hd : d * w ⬝ᵥ w = 2) : reflectionMatrix v c * reflectionMatrix w d ∈ Matrix.specialOrthogonalGroup n R

The product of two reflection matrices is special orthogonal.

def TauCeti.reflectionPair {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] [Fintype n] (v w : n → R) (c d : R) (hc : c * v ⬝ᵥ v = 2) (hd : d * w ⬝ᵥ w = 2) : ↥(Matrix.specialOrthogonalGroup n R)

The product of the reflections in two vectors with supplied normalizing scalars, as an element of the matrix special orthogonal group of the standard symmetric form. The scalars satisfy the displayed equations with the respective norms.

Equations

• TauCeti.reflectionPair v w c d hc hd = ⟨TauCeti.reflectionMatrix v c * TauCeti.reflectionMatrix w d, ⋯⟩

@[simp]

theorem TauCeti.coe_reflectionPair {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] [Fintype n] {v w : n → R} {c d : R} (hc : c * v ⬝ᵥ v = 2) (hd : d * w ⬝ᵥ w = 2) : ↑(reflectionPair v w c d hc hd) = reflectionMatrix v c * reflectionMatrix w d

@[simp]

theorem TauCeti.map_reflectionPair {n : Type v} [DecidableEq n] {R : Type u} [CommRing R] {S : Type w} [CommRing S] [Fintype n] (f : R →+* S) {v w : n → R} {c d : R} (hc : c * v ⬝ᵥ v = 2) (hd : d * w ⬝ᵥ w = 2) : (Matrix.SpecialOrthogonalGroup.map f) (reflectionPair v w c d hc hd) = reflectionPair (⇑f ∘ v) (⇑f ∘ w) (f c) (f d) ⋯ ⋯

Products of two reflections are natural in the coefficient ring.

One-parameter families through a product of two reflections

theorem TauCeti.exists_laurentPath_reflectionMatrix_mul {n : Type v} [DecidableEq n] {K : Type u} [Field K] [Fintype n] [NeZero 2] [IsAlgClosed K] {v w : n → K} {c d : K} (hc : c * v ⬝ᵥ v = 2) (hd : d * w ⬝ᵥ w = 2) : ∃ (M : ↥(Matrix.specialOrthogonalGroup n (LaurentPolynomial K))) (a : Kˣ) (b : Kˣ), ∀ (φ : LaurentPolynomial K →ₐ[K] K), (φ (LaurentPolynomial.T 1) = ↑a → (↑M).map ⇑↑φ = 1) ∧ (φ (LaurentPolynomial.T 1) = ↑b → (↑M).map ⇑↑φ = reflectionMatrix v c * reflectionMatrix w d)

Every product of two reflections is joined to the identity by a one-parameter family of special orthogonal matrices over the Laurent polynomials.

Both reflection vectors are anisotropic, so they span either a degenerate or a nondegenerate plane. In the degenerate case the two vectors are joined, up to scaling, by an affine line of vectors of constant norm. In the nondegenerate case the plane has, over an algebraically closed field, a basis of two isotropic vectors e and f, and e + t • f runs through every anisotropic line of the plane as t runs through the units. Reflecting first in v and then in the moving vector gives the family, and its two endpoints are the parameters at which the moving vector is proportional to v, respectively to w.