The endomorphism ring of the trivial abelian variety

The trivial abelian variety AbelianVariety.trivial K has a unique endomorphism, so its endomorphism ring is the zero ring and the multiplication-by-n endomorphism [n] is the identity for every n — a check that the construction of TauCeti.AlgebraicGeometry.AbelianVariety.End.Basic is not vacuous.

• AbelianVariety.mulBy_trivial: [n] = 𝟙 (trivial K).

That End (trivial K) is the zero ring needs no declaration here: AbelianVariety.End.instUnique turns the uniqueness of homomorphisms into the trivial abelian variety (AbelianVariety.uniqueHomToTrivial) into Unique (End (trivial K)) by instance search, which the example below records.

This is the specialization of the endomorphism ring to the trivial abelian variety, kept apart from End.Basic so that the generic construction does not depend on the trivial-variety theory. It advances the same roadmap item, TauCetiRoadmap/JacobianChallenge/README.md, Layer E, "[n] as an isogeny". No external mathematics is vendored: both facts come from the uniqueness of homomorphisms out of the zero object, already proved in TauCeti.AlgebraicGeometry.AbelianVariety.Trivial.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.mulBy_trivial {K : Type u} [Field K] (n : ℤ) : (trivial K).mulBy n = CategoryTheory.CategoryStruct.id (trivial K)

Every endomorphism of the trivial abelian variety, in particular every [n], is the identity.