Abelian varieties

Main results

• AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral: A proper geometrically integral group scheme over a field is commutative.

instance AlgebraicGeometry.instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf {K : Type u} [Field K] (G : CategoryTheory.Over (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })) [CategoryTheory.GrpObj G] : IsClosedImmersion CategoryTheory.MonObj.one.left

theorem AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed {K : Type u} [Field K] [IsAlgClosed K] (G : CategoryTheory.Over (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })) [IsProper G.hom] [IsIntegral (CategoryTheory.MonoidalCategoryStruct.tensorObj G G).left] [CategoryTheory.GrpObj G] : CategoryTheory.IsCommMonObj G

theorem AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral {K : Type u} [Field K] (G : CategoryTheory.Over (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })) [IsProper G.hom] [GeometricallyIntegral G.hom] [CategoryTheory.GrpObj G] : CategoryTheory.IsCommMonObj G

A proper geometrically integral group scheme over a field is commutative.