Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral

∀ {K : Type u} [inst : Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of K)))
  [AlgebraicGeometry.IsProper G.hom] [AlgebraicGeometry.GeometricallyIntegral G.hom] [inst_3 : CategoryTheory.GrpObj G],
  CategoryTheory.IsCommMonObj G

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

Defined in

Mathlib.AlgebraicGeometry.Group.Abelian

Cited by

0 results in Mathlib

Foundations

Depth 242 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldAlgebraicGeometry.IsProperAlgebraicGeometry.GeometricallyIntegralCategoryTheory.GrpObj