Abelian varieties

Main results

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

instance AlgebraicGeometry.instIsClosedImmersionLeftSchemeOneOverSpecOf {K : Type u} [Field K] (G : CategoryTheory.Over (Spec ↧K)) [CategoryTheory.GrpObj G] : IsClosedImmersion (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

theorem AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed {K : Type u} [Field K] [IsAlgClosed K] (G : CategoryTheory.Over (Spec ↧K)) [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 ↧K)) [IsProper G.hom] [GeometricallyIntegral G.hom] [CategoryTheory.GrpObj G] : CategoryTheory.IsCommMonObj G

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