Kernels of homomorphisms of multiplicative-type groups

For a homomorphism of groups of multiplicative type over a field, the geometric kernel has coordinate algebra the group algebra of the geometric character cokernel. In particular, the kernel over the original field is finite exactly when this cokernel is finite, and the Module.finrank of its coordinate algebra equals the Nat.card of the cokernel. For a finite kernel, this is its dimension equal to the cokernel's cardinality; in the infinite case both quantities are zero. These statements apply to arbitrary homomorphisms, without an isogeny or smoothness hypothesis.

The Hopf-algebra comparison retains the scheme structure of the kernel. Thus a finite kernel's rank counts infinitesimal structure as well as geometric points; for example, it gives rank p for the kernel μ_p of the pth power map in characteristic p.

The intrinsic diagonalizable-kernel calculation and the quotient base-change comparison supply the geometric identification; faithful-flat descent transfers finiteness to the original field.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.9(b) and §12.d.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

noncomputable def TauCeti.multiplicativeTypeCommHopfAlgProperty.geometricKernelCoordinateIso {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) (hK : multiplicativeTypeCommHopfAlgProperty k K) (f : H.obj ⟶ K.obj) : CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient K.obj (CommHopfAlgCat.kernelHopfIdeal f)) ≅ ↧(MonoidAlgebra (AlgebraicClosure k) (CommHopfAlgCat.geometricCharacterGroup K.obj ⧸ (CommHopfAlgCat.geometricCharacterMap f).range))

The geometric kernel of a homomorphism of multiplicative-type groups has coordinate Hopf algebra the group algebra of its geometric character cokernel.

Equations

• hH.geometricKernelCoordinateIso hK f = TauCeti.multiplicativeTypeCommHopfAlgProperty.geometricKernelCoordinateIsoAux✝ hH hK f (TauCeti.CommHopfAlgCat.geometricCharacterMap f) ⋯

@[simp]

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.baseChangeMap_mkQuotient_comp_geometricKernelCoordinateIso_hom {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) (hK : multiplicativeTypeCommHopfAlgProperty k K) (f : H.obj ⟶ K.obj) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient K.obj (CommHopfAlgCat.kernelHopfIdeal f))) (hH.geometricKernelCoordinateIso hK f).hom = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.evaluationIso ⋯).inv (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom (AlgebraicClosure k) (QuotientGroup.mk' (CommHopfAlgCat.geometricCharacterMap f).range)))

The geometric kernel comparison commutes with the scalar-extended quotient map. The right side expresses the ambient algebra in intrinsic character coordinates and then applies the character quotient.

@[simp]

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.baseChangeMap_mkQuotient_comp_geometricKernelCoordinateIso_hom_assoc {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) (hK : multiplicativeTypeCommHopfAlgProperty k K) (f : H.obj ⟶ K.obj) {Z : CommHopfAlgCat (AlgebraicClosure k)} (h : ↧(MonoidAlgebra (AlgebraicClosure k) (CommHopfAlgCat.geometricCharacterGroup K.obj ⧸ (CommHopfAlgCat.geometricCharacterMap f).range)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient K.obj (CommHopfAlgCat.kernelHopfIdeal f))) (CategoryTheory.CategoryStruct.comp (hH.geometricKernelCoordinateIso hK f).hom h) = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.evaluationIso ⋯).inv (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom (AlgebraicClosure k) (QuotientGroup.mk' (CommHopfAlgCat.geometricCharacterMap f).range))) h)

The geometric kernel comparison commutes with the scalar-extended quotient map. The right side expresses the ambient algebra in intrinsic character coordinates and then applies the character quotient.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.moduleFinite_kernelCoordinate_iff_finite_quotient {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) (hK : multiplicativeTypeCommHopfAlgProperty k K) (f : H.obj ⟶ K.obj) : Module.Finite k ↑(CommHopfAlgCat.quotient K.obj (CommHopfAlgCat.kernelHopfIdeal f)) ↔ Finite (CommHopfAlgCat.geometricCharacterGroup K.obj ⧸ (CommHopfAlgCat.geometricCharacterMap f).range)

A homomorphism of multiplicative-type groups has finite scheme-theoretic kernel exactly when its geometric character map has finite cokernel.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.finrank_kernelCoordinate {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) (hK : multiplicativeTypeCommHopfAlgProperty k K) (f : H.obj ⟶ K.obj) : Module.finrank k ↑(CommHopfAlgCat.quotient K.obj (CommHopfAlgCat.kernelHopfIdeal f)) = Nat.card (CommHopfAlgCat.geometricCharacterGroup K.obj ⧸ (CommHopfAlgCat.geometricCharacterMap f).range)

The Module.finrank of a multiplicative-type kernel's coordinate algebra over the ground field equals the Nat.card of the geometric character cokernel. For a finite kernel, this is its dimension, or scheme-theoretic rank, even when the kernel is nonreduced; in the infinite case both quantities are zero.