Kernels in intrinsic character coordinates

For diagonalizable coordinate Hopf algebras, the coordinate algebra of the kernel of a homomorphism is the group algebra of its character cokernel. Here the characters are the intrinsic group-like elements, so no presentation of either group as D(M) is chosen. The comparison commutes with the ambient quotient maps. It therefore retains the closed subgroup structure, including infinitesimal kernels in positive characteristic.

This extends the group-algebra calculation in TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Kernel using the natural evaluation isomorphisms of TauCeti.Algebra.AlgebraicGroup.CommHopfAlgCat.GroupLikeEvaluation.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.9(b).

noncomputable def TauCeti.DiagonalizableGroup.kernelGroupLikeCoordinateIso {k : Type u} [CommRing k] [IsDomain k] {H K : CommHopfAlgCat k} [Module.IsTorsionFree k ↑H] [Module.IsTorsionFree k ↑K] (hH : Submodule.span k (Set.range GroupLike.val) = ⊤) (hK : Submodule.span k (Set.range GroupLike.val) = ⊤) (f : H ⟶ K) : CommHopfAlgCat.quotient K (CommHopfAlgCat.kernelHopfIdeal f) ≅ ↧(MonoidAlgebra k (GroupLike k ↑K ⧸ (GroupLike.map (CommHopfAlgCat.Hom.hom f)).range))

The kernel coordinate algebra of a morphism of diagonalizable groups is the group algebra of the cokernel of its intrinsic character map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DiagonalizableGroup.mkQuotient_comp_kernelGroupLikeCoordinateIso_hom {k : Type u} [CommRing k] [IsDomain k] {H K : CommHopfAlgCat k} [Module.IsTorsionFree k ↑H] [Module.IsTorsionFree k ↑K] (hH : Submodule.span k (Set.range GroupLike.val) = ⊤) (hK : Submodule.span k (Set.range GroupLike.val) = ⊤) (f : H ⟶ K) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient K (CommHopfAlgCat.kernelHopfIdeal f)) (kernelGroupLikeCoordinateIso hH hK f).hom = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.evaluationIso hK).inv (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom k (QuotientGroup.mk' (GroupLike.map (CommHopfAlgCat.Hom.hom f)).range)))

The intrinsic kernel comparison commutes with the quotient coordinate maps. The ambient element is first expressed in its intrinsic character coordinates.

@[simp]

theorem TauCeti.DiagonalizableGroup.mkQuotient_comp_kernelGroupLikeCoordinateIso_hom_assoc {k : Type u} [CommRing k] [IsDomain k] {H K : CommHopfAlgCat k} [Module.IsTorsionFree k ↑H] [Module.IsTorsionFree k ↑K] (hH : Submodule.span k (Set.range GroupLike.val) = ⊤) (hK : Submodule.span k (Set.range GroupLike.val) = ⊤) (f : H ⟶ K) {Z : CommHopfAlgCat k} (h : ↧(MonoidAlgebra k (GroupLike k ↑K ⧸ (GroupLike.map (CommHopfAlgCat.Hom.hom f)).range)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient K (CommHopfAlgCat.kernelHopfIdeal f)) (CategoryTheory.CategoryStruct.comp (kernelGroupLikeCoordinateIso hH hK f).hom h) = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.evaluationIso hK).inv (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom k (QuotientGroup.mk' (GroupLike.map (CommHopfAlgCat.Hom.hom f)).range))) h)

The intrinsic kernel comparison commutes with the quotient coordinate maps. The ambient element is first expressed in its intrinsic character coordinates.