Orthogonal subrepresentations

For a reduced affine group of finite type over an algebraically closed field, a bilinear form invariant under rational points makes the orthogonal complement of a subrepresentation a subrepresentation. Point separation retains the full comodule structure, rather than just stability under rational points. This permits orthogonal subquotients in symplectic representations, including in characteristic two.

References

• J. S. Milne, Algebraic Groups (2017), §16 (representations and Lie--Kolchin).

noncomputable def TauCeti.Subcomodule.orthogonal {k : Type u_1} {H : Type u_2} {M : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] (N : Subcomodule k H M) (B : LinearMap.BilinForm k M) (hB : Representation.IsInvariantForm (Comodule.basePointsRepresentation M) B) : Subcomodule k H M

The orthogonal complement of a subrepresentation for a rational-point-invariant form, with its induced comodule structure.

@[simp]

theorem TauCeti.Subcomodule.orthogonal_toSubmodule {k : Type u_1} {H : Type u_2} {M : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] (N : Subcomodule k H M) (B : LinearMap.BilinForm k M) (hB : Representation.IsInvariantForm (Comodule.basePointsRepresentation M) B) : (N.orthogonal B hB).toSubmodule = B.orthogonal N.toSubmodule

The orthogonal subcomodule has the usual orthogonal complement as underlying subspace.

@[simp]

theorem TauCeti.Subcomodule.mem_orthogonal {k : Type u_1} {H : Type u_2} {M : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] (N : Subcomodule k H M) (B : LinearMap.BilinForm k M) (hB : Representation.IsInvariantForm (Comodule.basePointsRepresentation M) B) (m : M) : m ∈ N.orthogonal B hB ↔ ∀ n ∈ N, (B n) m = 0

Membership in the orthogonal subrepresentation is vanishing of all pairings with it.

theorem TauCeti.Subcomodule.comap_orthogonal_subtype_toSubmodule_ne_top {k : Type u_1} {H : Type u_2} {M : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] {B : LinearMap.BilinForm k M} (hB : Representation.IsInvariantForm (Comodule.basePointsRepresentation M) B) (N : Subcomodule k H M) (hN : N.toSubmodule ≤ B.orthogonal N.toSubmodule) (heq : N.toSubmodule ≠ B.orthogonal N.toSubmodule) : (N.comap (N.orthogonal B hB).subtype).toSubmodule ≠ ⊤

If a subrepresentation N is isotropic but not equal to its orthogonal complement, then the pullback of N to the orthogonal subrepresentation Nᗮ is a proper subspace.