abelian schemes

Stream: mathlib4

[Johan Commelin]

David Holmes said:

Starting from the top: "Abelian variety (in alg geom)". I wrote the def of abelian scheme in lean, v easy. Then I tried to prove they are commutative, not so simple. Probably doable if one assumes (Cohomology and Base-Change) and (proper pushforward of coherent is coherent), though I still have some sorries where gremlins may lurk. But actually writing down the def seems to me in this case not the hard part, unlike proving anything non-trivial.

What is your definition of abelian variety?
Mine are commutative by definition. But I guess you can do the theorem of the cube stuff, etc...

[Matthew Ballard]

Let's see some definitions!

[Kevin Buzzard]

"Smooth proper geometrically connected group variety" is a definition over fields for which commutativity is true but hard

[Matthew Ballard]

Kevin Buzzard said:

"Smooth proper geometrically connected group variety" is a definition over fields for which commutativity is true but hard

unexpected token; expected command

[Kevin Buzzard]

I think we might be just about ready for this though?

[Matthew Ballard]

I read above it was very easy

[Christian Merten]

Along the lines of Kevin's definition:

import Mathlib
universe u
open AlgebraicGeometry CategoryTheory Limits

namespace AlgebraicGeometry

class GeometricallyConnected {X : Scheme.{u}} {k : Type u} [Field k]
    (f : X ⟶ Spec (.of k)) : Prop where
  connectedSpace_pullback : ConnectedSpace
    ↑(pullback f (Spec.map (CommRingCat.ofHom <| algebraMap k (AlgebraicClosure k))))

class Scheme.Hom.GeometricallyConnected {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop where
  geometricallyConnected_fiber (y : Y) :
    AlgebraicGeometry.GeometricallyConnected (f.fiberToSpecResidueField y)

class Abelian {X S : Scheme.{u}} (f : X ⟶ S) extends GrpObj (Over.mk f),
  Smooth f, IsProper f, f.GeometricallyConnected

end AlgebraicGeometry

[Christian Merten]

Although, this should also be correct?

import Mathlib
universe u
open AlgebraicGeometry CategoryTheory Limits

namespace AlgebraicGeometry

class Abelian {X S : Scheme.{u}} (f : X ⟶ S) extends GrpObj (Over.mk f),
    Smooth f, IsProper f where
  connectedSpace_fiber (s : S) : ConnectedSpace (f.fiber s)

end AlgebraicGeometry

[Andrew Yang]

#35354 shows that proper geometrically-integral group schemes over fields are commutative.
(This follows from Zariski's main theorem, and it is done in a very productive week with Joël and Junyan in Utrecht organized by Christian)

We also know that proper reduced group schemes over algebraically closed fields are smooth (docs#AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed) and we can generalize to geometrically reduced + arbitrary base field once fpqc descent for smoothness from Christian's pi1 repo is upstreamed.