noncomputable def CoordinateExamples.symplecticFormMatrix (n : ℕ) (k : Type u_1) [Ring k] : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) k

The standard symplectic form matrix on kⁿ ⊕ kⁿ: the block matrix [[0, -1], [1, 0]].

def CoordinateExamples.splitOrthogonalFormMatrix (n : ℕ) (k : Type u_1) [Zero k] [One k] : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) k

The standard split-orthogonal (hyperbolic) form matrix on kⁿ ⊕ kⁿ: the block matrix [[0, 1], [1, 0]].

noncomputable def CoordinateExamples.orthogonalFormMatrix (p q : ℕ) (k : Type u_1) [Ring k] : Matrix (Fin p ⊕ Fin q) (Fin p ⊕ Fin q) k

The standard signature (p, q) orthogonal form matrix: the block-diagonal matrix with 1's in the first p slots and -1's in the last q slots.

def CoordinateExamples.IsFormPreserving {m : ℕ} {k : Type u_1} [CommRing k] (F g : Matrix (Fin m) (Fin m) k) : Prop

A matrix g is form-preserving for the bilinear form matrix F when gᵀ F g = F.

@[reducible, inline]

abbrev CoordinateExamples.IsSymplectic {n : ℕ} {k : Type u_1} [CommRing k] (J g : Matrix (Fin n) (Fin n) k) : Prop

Symplectic condition: g preserves the (alternating) form J.

@[reducible, inline]

abbrev CoordinateExamples.IsSplitOrthogonal {n : ℕ} {k : Type u_1} [CommRing k] (S g : Matrix (Fin n) (Fin n) k) : Prop

Split-orthogonal condition: g preserves the (symmetric hyperbolic) form S.

@[reducible, inline]

abbrev CoordinateExamples.IsOrthogonalPQ {m : ℕ} {k : Type u_1} [CommRing k] (Q g : Matrix (Fin m) (Fin m) k) : Prop

(p, q)-orthogonal condition: g preserves the signature (p, q) form Q.

def CoordinateExamples.IsInvertibleIsometry {m : ℕ} {k : Type u_1} [CommRing k] (F g : Matrix (Fin m) (Fin m) k) : Prop

A matrix g is an invertible isometry of the bilinear form F when it is invertible (its determinant is a unit) and form-preserving (gᵀ F g = F).

def CoordinateExamples.MatrixIsometryGroup {ι : Type u_1} [DecidableEq ι] [Fintype ι] {k : Type u_2} [CommRing k] (J : Matrix ι ι k) : Subgroup (GL ι k)

The matrix isometry group of a bilinear form matrix J: the subgroup of GL ι k consisting of matrices g satisfying gᵀ J g = J.

noncomputable def CoordinateExamples.Sp (n : ℕ) (k : Type u_1) [CommRing k] : Subgroup (GL (Fin n ⊕ Fin n) k)

The symplectic group Sp(2n, k): the matrix isometry group of the standard symplectic form on kⁿ ⊕ kⁿ.

def CoordinateExamples.OrthoSplit (n : ℕ) (k : Type u_1) [CommRing k] : Subgroup (GL (Fin n ⊕ Fin n) k)

The split-orthogonal group O(n, n; k): the matrix isometry group of the standard hyperbolic symmetric form on kⁿ ⊕ kⁿ.

noncomputable def CoordinateExamples.OrthogonalPQ (p q : ℕ) (k : Type u_1) [CommRing k] : Subgroup (GL (Fin p ⊕ Fin q) k)

The orthogonal group O(p, q; k) of signature (p, q): the matrix isometry group of the standard (p, q)-form on kᵖ ⊕ kᵠ.

structure CoordinateExamples.StandardParabolicData (n : ℕ) : Type

Combinatorial data for a standard parabolic subgroup of GL(n): a list of positive block sizes whose sum is at most n, used to record the dimensions of a partial flag of subspaces.

• sizes : List ℕ
• sizes_pos (s : ℕ) : s ∈ self.sizes → 0 < s
• sizes_sum : self.sizes.sum ≤ n

theorem CoordinateExamples.isFormPreserving_one {m : ℕ} {k : Type u_1} [CommRing k] (F : Matrix (Fin m) (Fin m) k) : IsFormPreserving F 1

The identity matrix is form-preserving for any bilinear form matrix F.