Matrix coefficients of a unimodular vector #
In a finite projective comodule over a commutative Hopf algebra, the matrix coefficients of a unimodular vector generate the unit ideal. Thus these coefficients can serve as homogeneous coordinates of a morphism to projective space: they have no common zero, including over nonreduced value algebras.
The result uses the invariant pairing of a comodule with its dual, formalized by
Comodule.baseChangeEvaluation_dual_endOfPoint_invariant.
References #
- J. S. Milne, Algebraic Groups (2017), §§7.d–7.f, projective orbits.
@[simp]
theorem
TauCeti.Comodule.span_matrixCoefficient_eq_top_iff_isUnimodular
{R : Type u}
{H : Type v}
{M : Type w}
[CommSemiring R]
[CommSemiring H]
[HopfAlgebra R H]
[AddCommMonoid M]
[Module R M]
[Comodule R H M]
[Module.Finite R M]
[Module.Projective R M]
(m : M)
:
Ideal.span (Set.range fun (φ : Module.Dual R M) => matrixCoefficient φ m) = ⊤ ↔ Module.IsUnimodular R m
The matrix coefficients of a vector in a finite projective Hopf comodule generate the unit ideal exactly when the vector is unimodular.