Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed

∀ {K : Type u} [inst : Field K] [IsAlgClosed K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of K)))
  [AlgebraicGeometry.IsProper G.hom]
  [AlgebraicGeometry.IsIntegral (CategoryTheory.MonoidalCategoryStruct.tensorObj G G).left]
  [inst_4 : CategoryTheory.GrpObj G], CategoryTheory.IsCommMonObj G

Defined in

Mathlib.AlgebraicGeometry.Group.Abelian

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldIsAlgClosedAlgebraicGeometry.IsProperAlgebraicGeometry.IsIntegralCategoryTheory.GrpObj