Abelian varieties

This file opens the Jacobian roadmap's Layer E by defining an abelian variety over a field K.

Following the roadmap, an abelian variety is bundled as a proper geometrically integral group scheme over K. From geometric integrality and the group-scheme smoothness theorem we derive the roadmap's smooth and geometrically connected interface, while Mathlib's rigidity theorem gives commutativity.

We bundle the data as a structure AbelianVariety K, so that later roadmap targets can write JacobianVariety X x₀ : AbelianVariety k and refer to (JacobianVariety X x₀).toScheme and its base changes, matching TauCetiRoadmap/JacobianChallenge/Suggested.lean. From the bundled hypotheses we derive:

• AbelianVariety.isCommMonObj: the group law is commutative, straight from Mathlib's rigidity theorem AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral;
• AbelianVariety.isIntegral: the underlying scheme is integral;
• AbelianVariety.smooth and AbelianVariety.geometricallyConnected: the roadmap's geometric hypotheses derived from geometric integrality;
• AbelianVariety.isLocallyNoetherian: the underlying scheme is locally Noetherian, since the structure morphism is locally of finite type; this is what makes the tangent space at the identity finite-dimensional downstream;
• AbelianVariety.dim: the topological Krull dimension of the underlying scheme;
• AbelianVariety.ofGeometricallyIntegral: a constructor from the geometrically integral package used by Mathlib's rigidity theorem;
• AbelianVariety.baseChange: the base change of an abelian variety along a field extension K → L is again an abelian variety, since properness and geometric integrality are stable under base change and the monoidal pullback functor carries the group-object structure.

The unit of the group law is a K-rational point, so the file also records the identity-point interface used by every later construction at the identity — the zero section AbelianVariety.zeroSection, the identity point AbelianVariety.zeroPoint, which is a closed point (AbelianVariety.isClosed_singleton_zeroPoint), and the resulting identification AbelianVariety.zeroResidueFieldRingEquiv : κ(0) ≃+* K of the residue field there with the ground field, with its K-algebra instance. These specialize the rational-point API of TauCeti.AlgebraicGeometry.RationalPoint.Basic at the unit section; the tangent space built on them lives in TauCeti.AlgebraicGeometry.AbelianVariety.TangentSpace.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer E, "Abelian variety = smooth, proper, geometrically connected group scheme over k; basic API ... Commutativity is automatic (rigidity, Group/Abelian.lean)", and the roadmap's base-change compatibility. No external mathematics is vendored; the proofs reuse Mathlib's Over/GrpObj monoidal API, the GeometricallyIntegral/IsProper morphism-property instances, and the commutativity theorem in Mathlib.AlgebraicGeometry.Group.Abelian.

structure TauCeti.AlgebraicGeometry.AbelianVariety (K : Type u) [Field K] : Type (u + 1)

An abelian variety over a field K: a proper geometrically integral group scheme over Spec K.

The group-object structure lives on toOver : Over (Spec (.of K)); the underlying scheme is toScheme = toOver.left. The fields are the standing hypotheses of the theory: grpObj is the group law, isProper says the structure morphism to Spec K is proper, and geometricallyIntegral records the geometric hypothesis from which smoothness, geometric connectedness, absolute integrality, and commutativity are derived.

• toOver : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)

  The underlying group scheme over Spec K.

• grpObj : CategoryTheory.GrpObj self.toOver

  The group-object structure on toOver.

• isProper : AlgebraicGeometry.IsProper self.toOver.hom

  The structure morphism to Spec K is proper.

• geometricallyIntegral : AlgebraicGeometry.GeometricallyIntegral self.toOver.hom

  The structure morphism to Spec K is geometrically integral.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.AbelianVariety.toScheme {K : Type u} [Field K] (A : AbelianVariety K) : AlgebraicGeometry.Scheme

The underlying scheme of an abelian variety.

Equations

• A.toScheme = A.toOver.left

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.AbelianVariety.dim {K : Type u} [Field K] (A : AbelianVariety K) : WithBot ℕ∞

The dimension of an abelian variety, defined as the topological Krull dimension of its underlying scheme.

Equations

• A.dim = topologicalKrullDim ↥A.toScheme

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.dim_def {K : Type u} [Field K] (A : AbelianVariety K) : A.dim = topologicalKrullDim ↥A.toScheme

instance TauCeti.AlgebraicGeometry.AbelianVariety.smooth {K : Type u} [Field K] (A : AbelianVariety K) : AlgebraicGeometry.Smooth A.toOver.hom

An abelian variety is smooth over the base field.

instance TauCeti.AlgebraicGeometry.AbelianVariety.isLocallyNoetherian {K : Type u} [Field K] (A : AbelianVariety K) : AlgebraicGeometry.IsLocallyNoetherian A.toScheme

The underlying scheme of an abelian variety is locally Noetherian.

instance TauCeti.AlgebraicGeometry.AbelianVariety.geometricallyConnected {K : Type u} [Field K] (A : AbelianVariety K) : AlgebraicGeometry.GeometricallyConnected A.toOver.hom

An abelian variety is geometrically connected over the base field.

instance TauCeti.AlgebraicGeometry.AbelianVariety.isCommMonObj {K : Type u} [Field K] (A : AbelianVariety K) : CategoryTheory.IsCommMonObj A.toOver

The group law of an abelian variety is commutative: a proper geometrically integral group scheme over a field is a commutative group object. This is the abstract rigidity theorem AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral, packaged for the bundled AbelianVariety.

instance TauCeti.AlgebraicGeometry.AbelianVariety.isIntegral {K : Type u} [Field K] (A : AbelianVariety K) : AlgebraicGeometry.IsIntegral A.toScheme

The underlying scheme of an abelian variety is integral: geometric integrality over the one-point base Spec K descends to absolute integrality. In particular the underlying space is nonempty, irreducible, and reduced.

The identity point

The unit of the group law is a section Spec K ⟶ A of the structure morphism, so it is a K-rational point of A and the residue field there is canonically the ground field. Following the additive convention for abelian varieties, these carry the zero stem.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.AbelianVariety.zeroSection {K : Type u} [Field K] (A : AbelianVariety K) : AlgebraicGeometry.Spec ↧K ⟶ A.toScheme

The zero section Spec K ⟶ A of an abelian variety, that is, the unit of its group law.

Equations

• A.zeroSection = CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one

theorem TauCeti.AlgebraicGeometry.AbelianVariety.zeroSection_comp_toOver_hom {K : Type u} [Field K] (A : AbelianVariety K) : CategoryTheory.CategoryStruct.comp A.zeroSection A.toOver.hom = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧K)

The zero section is a section of the structure morphism of A.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.zeroPoint {K : Type u} [Field K] (A : AbelianVariety K) : ↥A.toScheme

The identity point 0 of an abelian variety, obtained by evaluating the zero section at the unique point of Spec K. Its implementation is kept opaque; use zeroPoint_def to rewrite it explicitly.

Equations

• A.zeroPoint = A.zeroSection (IsLocalRing.closedPoint K)

theorem TauCeti.AlgebraicGeometry.AbelianVariety.zeroPoint_def {K : Type u} [Field K] (A : AbelianVariety K) : A.zeroPoint = A.zeroSection (IsLocalRing.closedPoint K)

The identity point is the value of the zero section. Not a simp lemma: the simp normal form of the structure morphism at the identity point is toOver_hom_zeroPoint, whose left-hand side this equation would rewrite.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.toOver_hom_zeroPoint {K : Type u} [Field K] (A : AbelianVariety K) : A.toOver.hom A.zeroPoint = IsLocalRing.closedPoint K

The structure morphism sends the identity point to the unique point of Spec K.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.isClosed_singleton_zeroPoint {K : Type u} [Field K] (A : AbelianVariety K) : IsClosed {A.zeroPoint}

The identity point is closed: the zero section is a closed immersion, and its image is the identity point.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.zeroResidueFieldRingEquiv {K : Type u} [Field K] (A : AbelianVariety K) : IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint) ≃+* K

The residue field of an abelian variety at its identity is canonically the ground field K, through the evaluation map of the zero section.

Equations

• A.zeroResidueFieldRingEquiv = TauCeti.AlgebraicGeometry.residueFieldRingEquivOfSection ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.zeroResidueFieldRingEquiv_apply {K : Type u} [Field K] (A : AbelianVariety K) (z : IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) : A.zeroResidueFieldRingEquiv z = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.descResidueField (AlgebraicGeometry.Scheme.stalkClosedPointTo A.zeroSection))) (⋯ ▸ z)

zeroResidueFieldRingEquiv is the evaluation map of the identity point. The argument is transported explicitly from zeroPoint to the value of the zero section.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.algebraZeroResidueField {K : Type u} [Field K] (A : AbelianVariety K) : Algebra K (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint))

The residue field at the identity is a K-algebra through zeroResidueFieldRingEquiv.

Equations

• A.algebraZeroResidueField = A.zeroResidueFieldRingEquiv.symm.toRingHom.toAlgebra

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.algebraMap_zeroResidueField {K : Type u} [Field K] (A : AbelianVariety K) (k : K) : (algebraMap K (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint))) k = A.zeroResidueFieldRingEquiv.symm k

The structure map of the K-algebra κ(0) is the inverse of zeroResidueFieldRingEquiv.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.ofGeometricallyIntegral {K : Type u} [Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) [CategoryTheory.GrpObj G] [AlgebraicGeometry.IsProper G.hom] [AlgebraicGeometry.GeometricallyIntegral G.hom] : AbelianVariety K

A constructor for abelian varieties from Mathlib's geometrically integral package.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.ofGeometricallyIntegral G = { toOver := G, grpObj := inferInstance, isProper := ⋯, geometricallyIntegral := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.ofGeometricallyIntegral_toOver {K : Type u} [Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) [CategoryTheory.GrpObj G] [AlgebraicGeometry.IsProper G.hom] [AlgebraicGeometry.GeometricallyIntegral G.hom] : (ofGeometricallyIntegral G).toOver = G

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.ofGeometricallyIntegral_one {K : Type u} [Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) [CategoryTheory.GrpObj G] [AlgebraicGeometry.IsProper G.hom] [AlgebraicGeometry.GeometricallyIntegral G.hom] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.eqToHom ⋯) = CategoryTheory.MonObj.one

The unit of ofGeometricallyIntegral G is the unit of G.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.ofGeometricallyIntegral_mul {K : Type u} [Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) [CategoryTheory.GrpObj G] [AlgebraicGeometry.IsProper G.hom] [AlgebraicGeometry.GeometricallyIntegral G.hom] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) CategoryTheory.MonObj.mul

The multiplication of ofGeometricallyIntegral G is the multiplication of G.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.ofGeometricallyIntegral_inv {K : Type u} [Field K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) [CategoryTheory.GrpObj G] [AlgebraicGeometry.IsProper G.hom] [AlgebraicGeometry.GeometricallyIntegral G.hom] : CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) CategoryTheory.GrpObj.inv

The inverse of ofGeometricallyIntegral G is the inverse of G.

Base change along a field extension

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.baseChange {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : AbelianVariety L

The base change of an abelian variety along a field extension K → L, obtained by pulling back the group scheme along Spec L → Spec K.

Properness and geometric integrality are stable under base change, and the monoidal pullback functor carries the group-object structure (Functor.grpObjObj), so the result is again an abelian variety. This realizes the roadmap's base-change compatibility of the Jacobian at the level of abelian varieties.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChange_toOver {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : (A.baseChange L).toOver = (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).obj A.toOver

theorem TauCeti.AlgebraicGeometry.AbelianVariety.commGrpMk_baseChange_toOver {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : { X := (A.baseChange L).toOver, grp := (A.baseChange L).grpObj, comm := ⋯ } = (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).mapCommGrp.obj { X := A.toOver, grp := A.grpObj, comm := ⋯ }

Bundling the underlying Over object of a base change with CommGrp.mk gives the commutative group object obtained by applying pullback.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChange_one {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L))))) ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).map CategoryTheory.MonObj.one)

The unit of a base-changed abelian variety is the pullback of the original unit, with the monoidal comparison for Over.pullback.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChange_mul {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))) A.toOver A.toOver) ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).map CategoryTheory.MonObj.mul))

The multiplication of a base-changed abelian variety is the pullback of the original multiplication, with the monoidal comparison for Over.pullback.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChange_inv {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).map CategoryTheory.GrpObj.inv)

The inverse of a base-changed abelian variety is the pullback of the original inverse.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChange_toScheme {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : (A.baseChange L).toScheme = CategoryTheory.Limits.pullback A.toOver.hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))

The underlying scheme of a base change is the fibre product of the abelian variety with Spec L over Spec K.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChange_dim {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : (A.baseChange L).dim = topologicalKrullDim ↥(CategoryTheory.Limits.pullback A.toOver.hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L))))