The standard representation of the orthogonal group

This file restricts the standard representation of the general linear group to the orthogonal group. It records the matrix action, its faithfulness, preservation of the standard symmetric bilinear pairing, and the corresponding character formulas.

Main definitions

• TauCeti.stdOrthogonalRep is the standard representation of Matrix.orthogonalGroup.
• TauCeti.stdOrthogonalFDRep is its finite-dimensional bundled form.
• TauCeti.stdOrthogonalDualRep is its contragredient.
• TauCeti.stdOrthogonalRepEquivDual is the equivariant self-duality induced by the dot product.

References

• Classical groups roadmap

def TauCeti.orthogonalGroupToGL (k : Type u) (n : ℕ) [CommRing k] : ↥(Matrix.orthogonalGroup (Fin n) k) →* GL (Fin n) k

The canonical inclusion of the orthogonal group into the general linear group.

Equations

• TauCeti.orthogonalGroupToGL k n = Matrix.GeneralLinearGroup.toLin.symm.toMonoidHom.comp Matrix.UnitaryGroup.embeddingGL

@[simp]

theorem TauCeti.orthogonalGroupToGL_coe (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : ↑((orthogonalGroupToGL k n) g) = ↑g

The orthogonal-to-general-linear inclusion has the original matrix as its underlying matrix.

theorem TauCeti.orthogonalGroupToGL_injective (k : Type u) (n : ℕ) [CommRing k] : Function.Injective ⇑(orthogonalGroupToGL k n)

The canonical inclusion of the orthogonal group into the general linear group is injective.

def TauCeti.stdOrthogonalRep (k : Type u) (n : ℕ) [CommRing k] : Representation k (↥(Matrix.orthogonalGroup (Fin n) k)) (Fin n → k)

The standard representation of the orthogonal group on column vectors.

Equations

• TauCeti.stdOrthogonalRep k n = MonoidHom.comp (TauCeti.stdRep k n) (TauCeti.orthogonalGroupToGL k n)

@[simp]

theorem TauCeti.stdOrthogonalRep_apply (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : (stdOrthogonalRep k n) g = (↑g).mulVecLin

The standard orthogonal action is multiplication by the underlying matrix.

theorem TauCeti.stdOrthogonalRep_apply_apply (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) (v : Fin n → k) : ((stdOrthogonalRep k n) g) v = (↑g).mulVec v

Evaluation of the standard orthogonal action is matrix-vector multiplication.

theorem TauCeti.stdOrthogonalRep_dotProduct_stdOrthogonalRep (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) (v w : Fin n → k) : ((stdOrthogonalRep k n) g) v ⬝ᵥ ((stdOrthogonalRep k n) g) w = v ⬝ᵥ w

The standard orthogonal action preserves the coordinate dot product.

noncomputable def TauCeti.stdOrthogonalRepToDual (k : Type u) (n : ℕ) [CommRing k] : (Fin n → k) ≃ₗ[k] Module.Dual k (Fin n → k)

The coordinate dot product identifies the standard module with its dual.

Equations

• TauCeti.stdOrthogonalRepToDual k n = (Pi.basisFun k (Fin n)).toDualEquiv

theorem TauCeti.stdOrthogonalRepToDual_apply (k : Type u) (n : ℕ) [CommRing k] (v w : Fin n → k) : ((stdOrthogonalRepToDual k n) v) w = v ⬝ᵥ w

stdOrthogonalRepToDual evaluates as the coordinate dot product.

theorem TauCeti.stdOrthogonalRep_injective (k : Type u) (n : ℕ) [CommRing k] : Function.Injective ⇑(stdOrthogonalRep k n)

The standard representation of the orthogonal group is faithful.

@[reducible, inline]

noncomputable abbrev TauCeti.stdOrthogonalFDRep (k : Type u) (n : ℕ) [CommRing k] : FDRep k ↥(Matrix.orthogonalGroup (Fin n) k)

The standard representation of the orthogonal group, bundled as an object of FDRep.

Equations

• TauCeti.stdOrthogonalFDRep k n = FDRep.of (TauCeti.stdOrthogonalRep k n)

noncomputable def TauCeti.stdOrthogonalDualRep (k : Type u) (n : ℕ) [CommRing k] : Representation k (↥(Matrix.orthogonalGroup (Fin n) k)) (Module.Dual k (Fin n → k))

The dual, or contragredient, of the standard representation of the orthogonal group.

Equations

• TauCeti.stdOrthogonalDualRep k n = (TauCeti.stdOrthogonalRep k n).dual

@[simp]

theorem TauCeti.stdOrthogonalDualRep_apply (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : (stdOrthogonalDualRep k n) g = Module.Dual.transpose (↑g⁻¹).mulVecLin

The dual standard orthogonal action is the transpose of the inverse matrix action.

theorem TauCeti.stdOrthogonalRepToDual_equivariant (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : ↑(stdOrthogonalRepToDual k n) ∘ₗ (stdOrthogonalRep k n) g = (stdOrthogonalDualRep k n) g ∘ₗ ↑(stdOrthogonalRepToDual k n)

The coordinate-dot-product identification intertwines the standard and dual actions.

noncomputable def TauCeti.stdOrthogonalRepEquivDual (k : Type u) (n : ℕ) [CommRing k] : (stdOrthogonalRep k n).Equiv (stdOrthogonalDualRep k n)

The standard representation of the orthogonal group is equivariantly self-dual.

Equations

• TauCeti.stdOrthogonalRepEquivDual k n = Representation.Equiv.mk (TauCeti.stdOrthogonalRepToDual k n) ⋯

@[simp]

theorem TauCeti.stdOrthogonalRepEquivDual_apply (k : Type u) (n : ℕ) [CommRing k] (v w : Fin n → k) : ((stdOrthogonalRepEquivDual k n) v) w = v ⬝ᵥ w

The orthogonal self-duality equivalence evaluates as the coordinate dot product.

@[reducible, inline]

noncomputable abbrev TauCeti.stdOrthogonalDualFDRep (k : Type u) (n : ℕ) [CommRing k] : FDRep k ↥(Matrix.orthogonalGroup (Fin n) k)

The dual standard representation of the orthogonal group, bundled as an object of FDRep.

Equations

• TauCeti.stdOrthogonalDualFDRep k n = FDRep.of (TauCeti.stdOrthogonalDualRep k n)

@[simp]

theorem TauCeti.char_stdOrthogonalRep (k : Type u) (n : ℕ) [Field k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : (stdOrthogonalRep k n).character g = (↑g).trace

The character of the standard representation of the orthogonal group is the matrix trace.

@[simp]

theorem TauCeti.char_stdOrthogonalFDRep (k : Type u) (n : ℕ) [Field k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : (stdOrthogonalFDRep k n).character g = (↑g).trace

The bundled standard orthogonal character is the matrix trace.

@[simp]

theorem TauCeti.char_stdOrthogonalDualRep (k : Type u) (n : ℕ) [Field k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : (stdOrthogonalDualRep k n).character g = (↑g⁻¹).trace

The dual standard orthogonal character is the inverse matrix trace.

@[simp]

theorem TauCeti.char_stdOrthogonalDualFDRep (k : Type u) (n : ℕ) [Field k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : (stdOrthogonalDualFDRep k n).character g = (↑g⁻¹).trace

The bundled dual standard character of the orthogonal group is the inverse matrix trace.