Commit 2026-02-17 07:11 3773dce3

View on Github →

feat(AlgebraicGeometry): abelian varieties are abelian (#35354) We show that proper geometrically-integral group schemes over fields are commutative.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AlgClosed/Basic.lean

added theorem AlgebraicGeometry.ext_of_apply_closedPoint_eq

added theorem AlgebraicGeometry.ext_of_apply_eq

Created Mathlib/AlgebraicGeometry/Group/Abelian.lean

added theorem AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral

added theorem AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed

Modified Mathlib/AlgebraicGeometry/Morphisms/FlatDescent.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

added theorem AlgebraicGeometry.ext_of_fromSpecResidueField_eq

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

Modified Mathlib/AlgebraicGeometry/Noetherian.lean

added theorem AlgebraicGeometry.LocallyOfFinitePresentation.iff_locallyOfFiniteType

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

added theorem CategoryTheory.Functor.map_inv'

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean

added theorem CategoryTheory.Over.fst_left

added theorem CategoryTheory.Over.snd_left

Modified Mathlib/Topology/JacobsonSpace.lean

added theorem JacobsonSpace.closure_inter_closedPoints_eq_closure

added theorem Set.Finite.isDiscrete_of_subset_closedPoints

added theorem subsingleton_image_closure_of_finite_of_isPreirreducible