Closed immersions of diagonalizable group schemes

A surjective homomorphism of finitely generated commutative character groups induces a surjective map of their group algebras. Relative spectrum reverses this map, so the resulting morphism of diagonalizable group schemes is a closed immersion.

Main declarations

• TauCeti.DiagonalizableGroup.isClosedImmersion_groupSchemeMap_of_surjective: the contravariant diagonalizable-group image of a surjective character-group homomorphism is a closed immersion.

theorem TauCeti.DiagonalizableGroup.isClosedImmersion_groupSchemeMap_of_surjective (R : Type u) [CommRing R] {G H : FGCommGrpCat} (φ : G ⟶ H) (hφ : Function.Surjective ⇑(FGCommGrpCat.toMonoidHom φ)) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (groupSchemeMap R φ).hom.hom)

A surjective homomorphism of character groups induces a closed immersion of the associated diagonalizable group schemes.