Quadratic and matrix orthogonal groups

When multiplication by two is injective in the base ring, a linear automorphism preserves the standard quadratic form exactly when its matrix is orthogonal. Adding determinant one identifies the two special orthogonal groups. These criteria transfer quadratic-space results to the matrix models of the classical groups.

The criteria apply to any finite index type, including the empty type, and to rings such as ℤ where two is regular but not invertible.

Main results

• TauCeti.toMatrix_mem_orthogonalGroup_iff: the coordinate criterion for the orthogonal group.
• TauCeti.toMatrix_mem_specialOrthogonalGroup_iff: the coordinate criterion for the special orthogonal group.

theorem TauCeti.toQuadraticForm'_one_apply {R : Type u} [CommRing R] {n : Type v} [Fintype n] [DecidableEq n] (x : n → R) : (Matrix.toQuadraticForm' 1) x = x ⬝ᵥ x

The quadratic form of the identity matrix sends a vector to its dot product with itself.

This is not a simp lemma: TauCeti.PDE.toQuadraticForm'_one already normalises the same left-hand side to ‖ξ‖ ^ 2 on EuclideanSpace ℝ n, and the two cannot both be simp-normal.

@[simp]

theorem TauCeti.polar_toQuadraticForm'_one {R : Type u} [CommRing R] {n : Type v} [Fintype n] [DecidableEq n] (x y : n → R) : QuadraticMap.polar (⇑(Matrix.toQuadraticForm' 1)) x y = 2 * x ⬝ᵥ y

The polar form of the standard quadratic form is twice the dot product.

@[simp]

theorem TauCeti.toMatrix_mem_orthogonalGroup_iff (R : Type u) [CommRing R] (n : Type v) [Fintype n] [DecidableEq n] (h2 : IsSMulRegular R 2) (e : (n → R) ≃ₗ[R] n → R) : LinearMap.toMatrix' ↑e ∈ Matrix.orthogonalGroup n R ↔ e ∈ QuadraticMap.orthogonalGroup (Matrix.toQuadraticForm' 1)

The coordinate matrix of a linear automorphism is orthogonal exactly when the automorphism preserves the standard quadratic form.

@[simp]

theorem TauCeti.toMatrix_mem_specialOrthogonalGroup_iff (R : Type u) [CommRing R] (n : Type v) [Fintype n] [DecidableEq n] (h2 : IsSMulRegular R 2) (e : (n → R) ≃ₗ[R] n → R) : LinearMap.toMatrix' ↑e ∈ Matrix.specialOrthogonalGroup n R ↔ e ∈ QuadraticMap.specialOrthogonalGroup (Matrix.toQuadraticForm' 1)

The coordinate matrix is special orthogonal exactly when the linear automorphism is special orthogonal for the standard quadratic form.