Matrix coefficients detect Chevalley-line cosets

Two algebra-valued points carry a unimodular vector to generators of the same line exactly when all their matrix coefficients differ by one common unit. For the exterior line realizing a closed subgroup as a stabilizer, this is precisely equality of left cosets. The criterion holds over arbitrary commutative value rings, including nonreduced rings; checking only field-valued points would lose the infinitesimal fiber relation.

The construction uses HopfIdeal.exists_finite_subcomodule_exteriorPower_line_stabilizer, Comodule.pointsAction, and scalar-extended dual evaluation. It supplies the algebraic fiber relation used to compare a projective orbit with a homogeneous quotient.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 4.27 and §§7.d–7.f.

theorem TauCeti.Comodule.span_pointsAction_eq_iff_exists_units_matrixCoefficient {R : Type u_1} {H : Type u_2} {M : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Free R M] [CommSemiring A] [Algebra R A] (m : M) (hm : Module.IsUnimodular R m) (g h : WithConv (H →ₐ[R] A)) : A ∙ ((pointsAction M) g) (1 ⊗ₜ[R] m) = A ∙ ((pointsAction M) h) (1 ⊗ₜ[R] m) ↔ ∃ (c : Aˣ), ∀ (φ : Module.Dual R M), h.ofConv (matrixCoefficient φ m) = ↑c * g.ofConv (matrixCoefficient φ m)

Equality of translated lines is equivalent to proportionality of all matrix coefficients by a common unit of the value algebra. No field or reducedness assumption is needed on it.

theorem TauCeti.HopfIdeal.coset_eq_iff_exists_units_matrixCoefficient {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {M : Type w} [AddCommGroup M] [Module R M] [Comodule R (↑H) M] [Module.Free R M] (I : HopfIdeal R ↑H) (m : M) (hm : Module.IsUnimodular R m) (A : CommAlgCat R) (hstab : ∀ (a : ↑(HopfAlgebra.points A)), a ∈ CommHopfAlgCat.quotientPointsSubgroup H I A ↔ Submodule.map (Comodule.endOfPoint M a.ofConv) (Submodule.baseChange (↑A) (R ∙ m)) = Submodule.baseChange (↑A) (R ∙ m)) (g h : ↑(HopfAlgebra.points A)) : ↑g = ↑h ↔ ∃ (c : (↑A)ˣ), ∀ (φ : Module.Dual R M), h.ofConv (Comodule.matrixCoefficient φ m) = ↑c * g.ofConv (Comodule.matrixCoefficient φ m)

If a closed subgroup is the stabilizer of a unimodular line, equality of left cosets is detected by unit proportionality of the line generator's matrix coefficients.

theorem TauCeti.HopfIdeal.exists_finite_subcomodule_exteriorPower_coset_matrixCoefficient {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (hI : I.toIdeal.FG) : ∃ (V : Subcomodule k ↑H ↑H) (n : ℕ), Module.Finite k ↥V.toSubmodule ∧ let this := Module.addCommMonoidToAddCommGroup k; ∃ (m : ↥(⋀[k]^n ↥V)), Module.IsUnimodular k m ∧ ∀ (A : CommAlgCat k) (g h : ↑(HopfAlgebra.points A)), ↑g = ↑h ↔ ∃ (c : (↑A)ˣ), ∀ (φ : Module.Dual k ↥(⋀[k]^n ↥V)), h.ofConv (Comodule.matrixCoefficient φ m) = ↑c * g.ofConv (Comodule.matrixCoefficient φ m)

Chevalley's coset criterion. A closed subgroup with finitely generated defining ideal admits a finite exterior-power representation and a unimodular vector whose matrix coefficients detect its left cosets over every commutative value algebra, including nonreduced algebras.