[Merged by Bors] - feat(AlgebraicGeometry): abelian varieties are abelian

[erdOne]

We show that proper geometrically-integral group schemes over fields are commutative.

Co-authored-by: Christian Merten

---

• depends on: [Merged by Bors] - feat(AlgebraicGeometry): geometrically integral schemes #35353
• depends on: [Merged by Bors] - feat(AlgebraicGeometry): corollaries of Zariski's main theorem #35232

[github-actions]

PR summary 330d0ae2dc

Import changes exceeding 2%

%	File
+3.61%	Mathlib.AlgebraicGeometry.Noetherian

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicGeometry.Noetherian	2297	2380	+83 (+3.61%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite	22
Mathlib.AlgebraicGeometry.Geometrically.Reduced	57
Mathlib.AlgebraicGeometry.Artinian	64
3 files Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.SpreadingOut	83
Mathlib.AlgebraicGeometry.Group.Abelian (new file)	2759

---

Declarations diff

+ Functor.map_inv'
+ JacobsonSpace.closure_inter_closedPoints_eq_closure
+ LocallyOfFinitePresentation.iff_locallyOfFiniteType
+ Set.Finite.isDiscrete_of_subset_closedPoints
+ ext_of_apply_closedPoint_eq
+ ext_of_apply_eq
+ ext_of_fromSpecResidueField_eq
+ fst_left
+ instance (G : Over (Spec (.of K))) [GrpObj G] : IsClosedImmersion η[G].left
+ instance (priority := low) [Nonempty X] [Subsingleton Y] (f : X ⟶ Y) :
+ instance (priority := low) {X Y : Scheme} (f : X ⟶ Y)
+ instance {X Y : Scheme} (f : X ⟶ Y) [Surjective f] [Flat f] [LocallyOfFinitePresentation f] :
+ instance {X Y : Scheme} (f : X ⟶ Y) [Surjective f] [Flat f] [QuasiCompact f] :
+ isCommMonObj_of_isProper_of_geometricallyIntegral
+ isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed
+ snd_left
+ subsingleton_image_closure_of_finite_of_isPreirreducible
++ instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S)

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(AlgebraicGeometry): geometrically integral schemes #35353
• [Merged by Bors] - feat(AlgebraicGeometry): corollaries of Zariski's main theorem #35232
  By Dependent Issues (🤖). Happy coding!

[CBirkbeck]

This is a looks really great, thanks for doing it! (I dont really have any serious comments on the PR other than tiny things I noticed)

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-CI job