def Garrett.BilinFormRadical {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Submodule k V

The radical of a bilinear form is the orthogonal complement of the whole space: the set of vectors orthogonal to everything.

def Garrett.BilinFormIsNondegenerate {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Prop

A bilinear form is nondegenerate (in Garrett's sense) when its radical is the zero subspace.

def Garrett.IsometryGroup {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Subgroup (V ≃ₗ[k] V)

The isometry group of a bilinear form B: linear automorphisms g of V satisfying B (g v₁) (g v₂) = B v₁ v₂ for all v₁, v₂.

def Garrett.SimilitudeGroup {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Subgroup (V ≃ₗ[k] V)

The similitude group of a bilinear form B: linear automorphisms scaling B by some unit ν, i.e. B (g v₁) (g v₂) = ν * B v₁ v₂.

def Garrett.OrthogonalGroup {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (_hB : B.IsSymm) : Subgroup (V ≃ₗ[k] V)

The orthogonal group of a symmetric bilinear form: the isometry group of B.

def Garrett.SymplecticGroup {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (_hB : B.IsAlt) : Subgroup (V ≃ₗ[k] V)

The symplectic group of an alternating bilinear form: the isometry group of B.

def Garrett.OrthogonalSimilitudeGroup {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (_hB : B.IsSymm) : Subgroup (V ≃ₗ[k] V)

The orthogonal similitude group: similitudes of a symmetric bilinear form.

def Garrett.SymplecticSimilitudeGroup {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (_hB : B.IsAlt) : Subgroup (V ≃ₗ[k] V)

The symplectic similitude group: similitudes of an alternating bilinear form.