The common kernel of algebraic characters

The common kernel of all characters of an affine group is a normal closed subgroup scheme. Its defining Hopf ideal is the kernel ideal of the canonical evaluation morphism from the character group algebra. A point lies in this subgroup precisely when every character has value one. The construction retains scheme-theoretic information over arbitrary base rings. When the characters span the coordinate algebra, as for a diagonalizable group, the common kernel is the trivial subgroup.

The formal construction uses MonoidAlgebra.liftGroupLikeBialgHom and TauCeti.CommHopfAlgCat.kernelHopfIdeal.

References

• A. Borel, Linear Algebraic Groups, §10.
• J. S. Milne, Algebraic Groups (2017), Chapters 12 and 16.

noncomputable def CommHopfAlgCat.characterKernelIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : TauCeti.HopfIdeal R ↑H

The defining Hopf ideal of the intersection of the kernels of all algebraic characters.

theorem CommHopfAlgCat.characterKernelIdeal_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : H.characterKernelIdeal = TauCeti.CommHopfAlgCat.kernelHopfIdeal (ofHom MonoidAlgebra.liftGroupLikeBialgHom)

The character kernel is the kernel of the evaluation morphism from the character group algebra.

theorem CommHopfAlgCat.isNormal_characterKernelIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : H.characterKernelIdeal.IsNormal

The common kernel of characters is a normal closed subgroup scheme.

@[simp]

theorem CommHopfAlgCat.sub_one_mem_characterKernelIdeal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (x : GroupLike R ↑H) : ↑x - 1 ∈ H.characterKernelIdeal

Every character restricts to one on the character kernel.

theorem CommHopfAlgCat.characterKernelIdeal_toIdeal_le_ker_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) {A : Type w} [Ring A] [Algebra R A] (f : ↑H →ₐ[R] A) : H.characterKernelIdeal.toIdeal ≤ RingHom.ker f.toRingHom ↔ ∀ (x : GroupLike R ↑H), f ↑x = 1

A coordinate map kills the character-kernel ideal exactly when all characters evaluate to one. In particular this characterizes membership of points in the common kernel.

theorem CommHopfAlgCat.characterKernelIdeal_le_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) : H.characterKernelIdeal ≤ I ↔ ∀ (x : GroupLike R ↑H), ↑x - 1 ∈ I

A closed subgroup lies in the common kernel of characters precisely when every character restricts to one on it.

theorem CommHopfAlgCat.characterKernelIdeal_eq_augmentation_of_groupLikeSetSpan_eq_top {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (h : TauCeti.Subcoalgebra.groupLikeSetSpan Set.univ = ⊤) : H.characterKernelIdeal = TauCeti.HopfIdeal.augmentation R ↑H

Characters of a diagonalizable group separate its points, scheme-theoretically and over any base ring: if the group-like elements span the coordinate algebra, the common kernel of characters is the trivial subgroup. This covers split tori and the geometric fibre of every group of multiplicative type, in particular of every torus.