Documentation

TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.Isometry.Basic

The special isometry group of a sesquilinear Gram matrix #

Let σ be an endomorphism of a commutative ring K and Q a square matrix over K. Together they define the σ-sesquilinear form

h(x, y) = (σ ∘ x) ⬝ᵥ (Q *ᵥ y) = ∑ i j, σ (x i) * Q i j * y j

on n → K, and a matrix g preserves it, h(g x, g y) = h(x, y), exactly when (g ^ σ)ᵀ * Q * g = Q, where g ^ σ applies σ to every entry. The matrices of determinant one with this property form the subgroup Matrix.specialIsometryGroup Q σ of the special linear group. For σ an involution and Q Hermitian or skew-Hermitian ((Q ^ σ)ᵀ = ε • Q with ε = ±1) this is a special unitary group SU(Q); for σ = id the defining equation is that of the bilinear isometry monoid Matrix.isometryMatrices Q, and the group is the special orthogonal group of a symmetric Q or the symplectic group of an alternating one. The finite special unitary groups SU_{r+1}(q) arise in this form as the Steinberg fixed points of the twisted groups ²A_r(q).

Over a field the group acts on the projective space ℙ K (n → K) through the special linear group. A point is isotropic when a representative v satisfies h(v, v) = 0; this does not depend on the representative, and the isometries permute the isotropic points. They form the sub-MulAction Matrix.isotropicPoints Q σ, the natural permutation domain of a unitary group.

Main definitions #

Main results #

References #

source
def Matrix.specialIsometryGroup {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] (Q : Matrix n n K) (σ : K →+* K) :
Subgroup (SpecialLinearGroup n K)

The special isometry group of a sesquilinear Gram matrix: the matrices g of determinant one with (g ^ σ)ᵀ * Q * g = Q, that is, the special linear transformations preserving the σ-sesquilinear form h(x, y) = (σ ∘ x) ⬝ᵥ (Q *ᵥ y). For an involution σ and a Hermitian or skew-Hermitian Q it is the special unitary group of Q.

Instances For
    source
    @[simp]
    theorem Matrix.mem_specialIsometryGroup_iff {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] {Q : Matrix n n K} {σ : K →+* K} {g : SpecialLinearGroup n K} :
    g ∈ Q.specialIsometryGroup σ ↔ ((↑g).map ⇑σ).transpose * Q * ↑g = Q

    An element of the special linear group is an isometry exactly when (g ^ σ)ᵀ * Q * g = Q.

    source
    def Matrix.isotropicPoints {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] (Q : Matrix n n K) (σ : K →+* K) :
    SubMulAction (↥(Q.specialIsometryGroup σ)) (Projectivization K (n → K))

    The isotropic points of projective space: the points [v] with h(v, v) = 0, as a sub-MulAction of the special isometry group. Whether [v] is isotropic does not depend on the representative v (Matrix.mk_mem_isotropicPoints_iff).

    Instances For
      source
      theorem Matrix.mem_isotropicPoints_iff {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} {p : Projectivization K (n → K)} :
      p ∈ Q.isotropicPoints σ ↔ ⇑σ ∘ p.rep ⬝ᵥ Q.mulVec p.rep = 0

      A point lies in isotropicPoints exactly when its chosen representative is isotropic.

      source
      @[simp]
      theorem Matrix.mk_mem_isotropicPoints_iff {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} {v : n → K} (hv : v ≠ 0) :
      Projectivization.mk K v hv ∈ Q.isotropicPoints σ ↔ ⇑σ ∘ v ⬝ᵥ Q.mulVec v = 0

      Isotropy of a point is isotropy of any representative: [v] is isotropic exactly when h(v, v) = 0.

      source
      theorem Matrix.comp_rep_dotProduct_mulVec_rep {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} (p : ↥(Q.isotropicPoints σ)) :
      ⇑σ ∘ (↑p).rep ⬝ᵥ Q.mulVec (↑p).rep = 0

      The representative of an isotropic point is an isotropic vector.