The trivial abelian variety

The base Spec K itself, with its unique group-scheme structure, is an abelian variety over K. This file constructs it as AbelianVariety.trivial K and identifies it as the zero object of the category of abelian varieties over K.

• AbelianVariety.trivial: the trivial abelian variety, carried by the monoidal unit 𝟙_ (Over (Spec K)), whose underlying scheme is Spec K;
• AbelianVariety.dim_trivial: its dimension is 0;
• AbelianVariety.isTerminalTrivial, AbelianVariety.isInitialTrivial, AbelianVariety.isZeroTrivial: it is a zero object, so there is exactly one homomorphism in either direction between it and any abelian variety;
• AbelianVariety.toTrivial_comp_fromTrivial: the composite A ⟶ trivial K ⟶ B is the identity element of the group A ⟶ B of MorphismGroup.lean, so the zero object of the category and the neutral element of the pointwise group law agree;
• AbelianVariety.baseChangeTrivialIso: base change along K → L carries the trivial abelian variety over K to the trivial abelian variety over L.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer E, "Abelian variety = smooth, proper, geometrically connected group scheme over k; basic API, dim", and the roadmap's base-change compatibility. Mathematically this is the degenerate case of the Jacobian: a curve of genus 0 has trivial Jacobian, and there the acceptance criterion dim (Jac X) = genus X reads dim (trivial K) = 0. No external mathematics is vendored; the proofs reuse Mathlib's group-object structure on the monoidal unit together with its uniqueness API for the trivial group object (CommGrp.uniqueHomFromTrivial, Grp.uniqueHomToTrivial), the terminal object of Over S, preservation of terminal objects by the right adjoint Over.pullback, and PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim together with ringKrullDim_eq_zero_of_field. The geometric-integrality input is TauCeti.AlgebraicGeometry.geometricallyIntegral_of_isIso. The abelian variety itself is assembled by the existing constructor AbelianVariety.ofGeometricallyIntegral; its characteristic lemmas identify the underlying group scheme and operations without exposing the constructor's implementation.

An earlier Tau Ceti formalization of this target, PR #1030, was retired by queue housekeeping at the review round cap without an all-green review. This file follows its overall design: the same carrier 𝟙_ (Over (Spec K)) passed to ofGeometricallyIntegral, the same trivial_toOver / trivial_toScheme / isTerminalTrivialToOver interface, and its geometricallyIntegral_of_isIso (revised here from a low-priority instance to a plain lemma, and placed in TauCeti.AlgebraicGeometry.Geometrically.Integral). It is extended here beyond terminality to the full zero-object statement, the compatibility with the pointwise group law on hom-sets, and the behaviour under base change.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.trivial (K : Type u) [Field K] : AbelianVariety K

The trivial abelian variety over K: the base Spec K regarded as a group scheme over itself.

It is carried by the monoidal unit 𝟙_ (Over (Spec K)), which is a group object because it is terminal, and whose structure morphism is proper and geometrically integral by isProperTensorUnit and geometricallyIntegralTensorUnit. Those are exactly the hypotheses of AbelianVariety.ofGeometricallyIntegral, which assembles them.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.trivial_toOver (K : Type u) [Field K] : (trivial K).toOver = CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K))

The group scheme underlying the trivial abelian variety is the monoidal unit of Over (Spec K).

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.trivial_toScheme (K : Type u) [Field K] : (trivial K).toScheme = AlgebraicGeometry.Spec ↧K

The scheme underlying the trivial abelian variety is Spec K.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.isTerminalTrivialToOver (K : Type u) [Field K] : CategoryTheory.Limits.IsTerminal (trivial K).toOver

The scheme over Spec K underlying the trivial abelian variety is terminal: it is the monoidal unit of Over (Spec K).

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.isTerminalTrivialToOver K = CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.ofIso (CategoryTheory.eqToIso ⋯)

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.trivial_one (K : Type u) [Field K] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.eqToHom ⋯) = CategoryTheory.MonObj.one

The unit section of the trivial abelian variety is the identity: it is an endomorphism of a terminal object.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.trivial_mul (K : Type u) [Field K] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) CategoryTheory.MonObj.mul

The multiplication of the trivial abelian variety is the terminal projection.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.trivial_inv (K : Type u) [Field K] : CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) CategoryTheory.GrpObj.inv

The inversion of the trivial abelian variety is the identity.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.dim_trivial (K : Type u) [Field K] : (trivial K).dim = 0

The trivial abelian variety has dimension 0.

The zero object

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.uniqueHomToTrivial {K : Type u} [Field K] (A : AbelianVariety K) : Unique (A ⟶ trivial K)

There is exactly one homomorphism from an abelian variety to the trivial one. Since (trivial K).toOver is the monoidal unit, this is Mathlib's Grp.uniqueHomToTrivial, transported through the hom equivalences of the induced categories AbelianVariety K, CommGrp and Grp.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.uniqueHomFromTrivial {K : Type u} [Field K] (A : AbelianVariety K) : Unique (trivial K ⟶ A)

There is exactly one homomorphism from the trivial abelian variety to an abelian variety. Since (trivial K).toOver is the monoidal unit, this is Mathlib's CommGrp.uniqueHomFromTrivial, transported through the hom equivalence of the induced category AbelianVariety K.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.toTrivial {K : Type u} [Field K] (A : AbelianVariety K) : A ⟶ trivial K

The homomorphism from an abelian variety to the trivial one, namely the identity element of the group A ⟶ trivial K. Its underlying morphism over Spec K is the structure morphism of A.

Equations

• A.toTrivial = 1

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.toOverHom_toTrivial {K : Type u} [Field K] (A : AbelianVariety K) : CategoryTheory.CategoryStruct.comp (Hom.toOverHom A.toTrivial) (CategoryTheory.eqToHom ⋯) = CategoryTheory.SemiCartesianMonoidalCategory.toUnit A.toOver

The morphism over Spec K underlying toTrivial A is the structure morphism of A, after transporting its codomain along trivial_toOver.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.toSchemeHom_toTrivial {K : Type u} [Field K] (A : AbelianVariety K) : CategoryTheory.CategoryStruct.comp (Hom.toSchemeHom A.toTrivial) (CategoryTheory.eqToHom ⋯) = A.toOver.hom

The scheme morphism underlying toTrivial A is the structure morphism of A, after transporting its codomain to Spec K.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.fromTrivial {K : Type u} [Field K] (A : AbelianVariety K) : trivial K ⟶ A

The homomorphism from the trivial abelian variety to an abelian variety, namely the identity element of the group trivial K ⟶ A. Its underlying morphism over Spec K is the unit section of A.

Equations

• A.fromTrivial = 1

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.toOverHom_fromTrivial {K : Type u} [Field K] (A : AbelianVariety K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (Hom.toOverHom A.fromTrivial) = CategoryTheory.MonObj.one

The identity element of trivial K ⟶ A is the unit section of A: it is toUnit (trivial K).toOver ≫ η[A.toOver], and the first factor is an endomorphism of a terminal object, hence the identity.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.toSchemeHom_fromTrivial {K : Type u} [Field K] (A : AbelianVariety K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (Hom.toSchemeHom A.fromTrivial) = A.zeroSection

The scheme morphism underlying fromTrivial A is the zero section of A, after transporting its domain from Spec K.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.isTerminalTrivial (K : Type u) [Field K] : CategoryTheory.Limits.IsTerminal (trivial K)

The trivial abelian variety is terminal: the only homomorphism to it from an abelian variety over K is that variety's structure morphism to Spec K.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.isTerminalTrivial K = CategoryTheory.Limits.IsTerminal.ofUnique (TauCeti.AlgebraicGeometry.AbelianVariety.trivial K)

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.isInitialTrivial (K : Type u) [Field K] : CategoryTheory.Limits.IsInitial (trivial K)

The trivial abelian variety is initial: the only homomorphism from it to an abelian variety over K is that variety's unit section, because a homomorphism of group schemes preserves the unit and the unit of the trivial group scheme is the identity.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.isInitialTrivial K = CategoryTheory.Limits.IsInitial.ofUnique (TauCeti.AlgebraicGeometry.AbelianVariety.trivial K)

theorem TauCeti.AlgebraicGeometry.AbelianVariety.isZeroTrivial (K : Type u) [Field K] : CategoryTheory.Limits.IsZero (trivial K)

The trivial abelian variety is a zero object of the category of abelian varieties over K.

instance TauCeti.AlgebraicGeometry.AbelianVariety.instHasZeroObject (K : Type u) [Field K] : CategoryTheory.Limits.HasZeroObject (AbelianVariety K)

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.toTrivial_comp_fromTrivial {K : Type u} [Field K] (A B : AbelianVariety K) : CategoryTheory.CategoryStruct.comp A.toTrivial B.fromTrivial = 1

Factoring through the trivial abelian variety gives the identity element of the group of homomorphisms A ⟶ B: the zero object of the category and the neutral element of the pointwise group law agree.

Base change

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.isTerminalBaseChangeTrivial (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] : CategoryTheory.Limits.IsTerminal ((trivial K).baseChange L)

The base change of the trivial abelian variety along K → L is terminal in the category of abelian varieties over L.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.baseChangeTrivialIso (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] : (trivial K).baseChange L ≅ trivial L

Base change along a field extension K → L carries the trivial abelian variety over K to the trivial abelian variety over L: both are terminal in the category of abelian varieties over L.

Equations

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

theorem TauCeti.AlgebraicGeometry.AbelianVariety.dim_baseChange_trivial (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] : ((trivial K).baseChange L).dim = 0

The base change of the trivial abelian variety still has dimension 0.