Abelian varieties #
Main results #
AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral: A proper geometrically integral group scheme over a field is commutative.
theorem
AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed
{K : Type u}
[Field K]
[IsAlgClosed K]
(G : CategoryTheory.Over (Spec (CommRingCat.of K)))
[IsProper G.hom]
[IsIntegral (CategoryTheory.MonoidalCategoryStruct.tensorObj G G).left]
[CategoryTheory.GrpObj G]
:
theorem
AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral
{K : Type u}
[Field K]
(G : CategoryTheory.Over (Spec (CommRingCat.of K)))
[IsProper G.hom]
[GeometricallyIntegral G.hom]
[CategoryTheory.GrpObj G]
:
A proper geometrically integral group scheme over a field is commutative.