The endomorphism ring of an abelian variety

The endomorphisms of an abelian variety A over a field K form a ring: addition is the pointwise group law of A, multiplication is composition. This file constructs that ring and the multiplication-by-n endomorphism [n] : A ⟶ A as the image of n : ℤ in it.

The pointwise group law on homomorphisms of abelian varieties is written multiplicatively in TauCeti.AlgebraicGeometry.AbelianVariety.MorphismGroup, matching the multiplicative encoding (GrpObj, μ, η, ι) of a group object. A ring is written additively, so the endomorphism ring is the additive reindexing Additive (A ⟶ A) of that group rather than the hom-set itself; this keeps the multiplicative convention on all hom-sets intact. (Declaring AbelianVariety K CategoryTheory.Preadditive instead would put an AddCommGroup (A ⟶ B) on the very hom-sets that already carry AbelianVariety.Hom.instCommGroup for the same operation — the situation Additive exists to avoid — and would mean re-deriving that group law additively rather than transporting Mathlib's multiplicative CategoryTheory.MonObj.Hom.commGroup; that is a change to already-merged material, not part of this file.) Reindexing only the additive structure leaves End A the same type as Mathlib's CategoryTheory.End A, so the multiplicative monoid here is Mathlib's, and conjugation by an isomorphism is Mathlib's CategoryTheory.Iso.conj. AbelianVariety.End.toHom and AbelianVariety.End.ofHom translate between the two views, and the toHom_* lemmas turn every ring operation into a group or categorical operation on morphisms.

• AbelianVariety.End A: the endomorphism ring, with AbelianVariety.End.instRing, and AbelianVariety.End.instUnique recognizing it as the zero ring when A has one endomorphism;
• AbelianVariety.mulBy A n: the endomorphism [n], with AbelianVariety.mulBy_eq_zpow identifying it with the n-th power map and AbelianVariety.mulBy_comp recording that every homomorphism of abelian varieties commutes with it;
• AbelianVariety.End.congr: an isomorphism of abelian varieties conjugates one endomorphism ring isomorphically onto the other.

The specialization to the trivial abelian variety is in TauCeti.AlgebraicGeometry.AbelianVariety.End.Trivial, which is where the trivial-variety theory gets imported.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer E, "Abelian variety = smooth, proper, geometrically connected group scheme over k; basic API", and its item "[n] as an isogeny" — the endomorphism ring is where [n] lives, and where the homomorphism produced by Layer F's universal property of the Abel–Jacobi map is compared with others. That [n] is an isogeny needs the dimension and torsion theory of Layer E and is not proved here. No external mathematics is vendored; the ring is assembled from Tau Ceti's homomorphism-group API, Mathlib's Additive type synonym, Mathlib's CategoryTheory.End monoid and CategoryTheory.Iso.conj, with only the distributivity supplied by AbelianVariety.Hom.mul_comp and AbelianVariety.Hom.comp_mul proved here — the same assembly as Mathlib's Ring (CategoryTheory.End X) for preadditive categories.

def TauCeti.AlgebraicGeometry.AbelianVariety.End {K : Type u} [Field K] (A : AbelianVariety K) : Type u

The endomorphism ring of an abelian variety A: the endomorphisms of A, with addition the pointwise group law of A and multiplication composition.

Since the pointwise group law on A ⟶ A is written multiplicatively (see AbelianVariety.Hom.instCommGroup) while a ring is written additively, this is the additive reindexing of the group A ⟶ A; use AbelianVariety.End.toHom and AbelianVariety.End.ofHom to pass between an element of the ring and the endomorphism it denotes.

Equations

• A.End = Additive (A ⟶ A)

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom {K : Type u} [Field K] {A : AbelianVariety K} (x : A.End) : A ⟶ A

The endomorphism of A denoted by an element of the endomorphism ring End A.

Equations

• x.toHom = Additive.toMul x

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.End.ofHom {K : Type u} [Field K] {A : AbelianVariety K} (f : A ⟶ A) : A.End

An endomorphism of A, viewed as an element of the endomorphism ring End A.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.End.ofHom f = Additive.ofMul f

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_ofHom {K : Type u} [Field K] {A : AbelianVariety K} (f : A ⟶ A) : (ofHom f).toHom = f

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.ofHom_toHom {K : Type u} [Field K] {A : AbelianVariety K} (x : A.End) : ofHom x.toHom = x

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_injective {K : Type u} [Field K] {A : AbelianVariety K} : Function.Injective toHom

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.ext {K : Type u} [Field K] {A : AbelianVariety K} {x y : A.End} (h : x.toHom = y.toHom) : x = y

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.ext_iff {K : Type u} [Field K] {A : AbelianVariety K} {x y : A.End} : x = y ↔ x.toHom = y.toHom

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_inj {K : Type u} [Field K] {A : AbelianVariety K} {x y : A.End} : x.toHom = y.toHom ↔ x = y

The additive group

Addition in End A is the pointwise group law of the target, so each additive operation translates into the corresponding multiplicative one on morphisms.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.End.instAddCommGroup {K : Type u} [Field K] (A : AbelianVariety K) : AddCommGroup A.End

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_zero {K : Type u} [Field K] {A : AbelianVariety K} : toHom 0 = 1

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_add {K : Type u} [Field K] {A : AbelianVariety K} (x y : A.End) : (x + y).toHom = x.toHom * y.toHom

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_neg {K : Type u} [Field K] {A : AbelianVariety K} (x : A.End) : (-x).toHom = x.toHom⁻¹

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_sub {K : Type u} [Field K] {A : AbelianVariety K} (x y : A.End) : (x - y).toHom = x.toHom / y.toHom

The two scalar-multiplication lemmas are deliberately not @[simp], unlike the rest of this section: simp rewrites a scalar multiple in a ring to a product (nsmul_eq_mul, zsmul_eq_mul), so their left-hand sides are not in simp normal form. Use AbelianVariety.End.toHom_natCast or AbelianVariety.End.toHom_intCast together with AbelianVariety.End.toHom_mul instead.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_nsmul {K : Type u} [Field K] {A : AbelianVariety K} (n : ℕ) (x : A.End) : (n • x).toHom = x.toHom ^ n

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_zsmul {K : Type u} [Field K] {A : AbelianVariety K} (n : ℤ) (x : A.End) : (n • x).toHom = x.toHom ^ n

The multiplicative monoid

Multiplication in End A is composition, in the order of Function.comp rather than of CategoryTheory.CategoryStruct.comp. Since End A reindexes only the additive structure of A ⟶ A, it is the same type as Mathlib's CategoryTheory.End A, so the multiplicative monoid is Mathlib's CategoryTheory.End.monoid rather than a new one.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.End.instMonoid {K : Type u} [Field K] (A : AbelianVariety K) : Monoid A.End

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_one {K : Type u} [Field K] {A : AbelianVariety K} : toHom 1 = CategoryTheory.CategoryStruct.id A

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_mul {K : Type u} [Field K] {A : AbelianVariety K} (x y : A.End) : (x * y).toHom = CategoryTheory.CategoryStruct.comp y.toHom x.toHom

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.ofHom_comp {K : Type u} [Field K] {A : AbelianVariety K} (f g : A ⟶ A) : ofHom (CategoryTheory.CategoryStruct.comp f g) = ofHom g * ofHom f

Composing two endomorphisms is multiplying them in the endomorphism ring, in the reversed order.

The ring

Composition of homomorphisms of abelian varieties is bimultiplicative for the pointwise group law (AbelianVariety.Hom.mul_comp and AbelianVariety.Hom.comp_mul), which is exactly distributivity of multiplication over addition in End A.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.End.instSemiring {K : Type u} [Field K] (A : AbelianVariety K) : Semiring A.End

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.End.instRing {K : Type u} [Field K] (A : AbelianVariety K) : Ring A.End

Equations

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

@[instance_reducible]

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

An abelian variety with only one endomorphism has the zero ring as its endomorphism ring.

This is Mathlib's Unique (Additive α) instance; it is stated here, rather than reproved wherever a hom-set is known to be a singleton, because unfolding End A to Additive (A ⟶ A) is only possible in this module.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.End.instUnique = { default := TauCeti.AlgebraicGeometry.AbelianVariety.End.instUnique._aux_1, uniq := ⋯ }

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_natCast {K : Type u} [Field K] {A : AbelianVariety K} (n : ℕ) : (↑n).toHom = CategoryTheory.CategoryStruct.id A ^ n

The natural number n acts in the endomorphism ring as the n-th power of the identity for the pointwise group law.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_intCast {K : Type u} [Field K] {A : AbelianVariety K} (n : ℤ) : (↑n).toHom = CategoryTheory.CategoryStruct.id A ^ n

The integer n acts in the endomorphism ring as the n-th power of the identity for the pointwise group law.

Transport along an isomorphism

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.End.congr {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) : A.End ≃+* B.End

Conjugation by an isomorphism e : A ≅ B of abelian varieties, as an isomorphism of endomorphism rings End A ≃+* End B.

The multiplicative part is Mathlib's CategoryTheory.Iso.conj; only additivity — that conjugation respects the pointwise group law — has to be proved here.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.End.congr e = { toEquiv := e.conj.toEquiv, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_congr {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) (x : A.End) : ((congr e) x).toHom = CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.CategoryStruct.comp x.toHom e.hom)

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_congr_symm {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) (y : B.End) : ((congr e).symm y).toHom = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp y.toHom e.inv)

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.congr_refl {K : Type u} [Field K] (A : AbelianVariety K) : congr (CategoryTheory.Iso.refl A) = RingEquiv.refl A.End

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.congr_trans {K : Type u} [Field K] {A B C : AbelianVariety K} (e : A ≅ B) (f : B ≅ C) : congr (e ≪≫ f) = (congr e).trans (congr f)

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.mulBy {K : Type u} [Field K] (A : AbelianVariety K) (n : ℤ) : A ⟶ A

The multiplication-by-n endomorphism [n] : A ⟶ A of an abelian variety, that is, the image of n : ℤ in the endomorphism ring AbelianVariety.End A.

The name is the standard one for abelian varieties, whose group law is conventionally written additively. Here the group law on morphisms is written multiplicatively, so [n] is concretely the n-th power map for that law: see AbelianVariety.mulBy_eq_zpow.

Equations

• A.mulBy n = (↑n).toHom

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.ofHom_mulBy {K : Type u} [Field K] (A : AbelianVariety K) (n : ℤ) : ofHom (A.mulBy n) = ↑n

Viewed back in the endomorphism ring, [n] is the integer n.

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

[n] is the n-th power map for the pointwise group law on endomorphisms.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.mulBy_zero {K : Type u} [Field K] (A : AbelianVariety K) : A.mulBy 0 = 1

[0] is the constant endomorphism through the unit section, the identity of the pointwise group law.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.mulBy_one {K : Type u} [Field K] (A : AbelianVariety K) : A.mulBy 1 = CategoryTheory.CategoryStruct.id A

[1] is the identity.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.mulBy_add {K : Type u} [Field K] (A : AbelianVariety K) (m n : ℤ) : A.mulBy (m + n) = A.mulBy m * A.mulBy n

[m + n] is the pointwise product of [m] and [n].

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.mulBy_neg {K : Type u} [Field K] (A : AbelianVariety K) (n : ℤ) : A.mulBy (-n) = (A.mulBy n)⁻¹

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.mulBy_sub {K : Type u} [Field K] (A : AbelianVariety K) (m n : ℤ) : A.mulBy (m - n) = A.mulBy m / A.mulBy n

[m - n] is the pointwise quotient of [m] and [n].

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.mulBy_mul {K : Type u} [Field K] (A : AbelianVariety K) (m n : ℤ) : A.mulBy (m * n) = CategoryTheory.CategoryStruct.comp (A.mulBy n) (A.mulBy m)

[m * n] is [m] composed with [n].

theorem TauCeti.AlgebraicGeometry.AbelianVariety.mulBy_comp {K : Type u} [Field K] {A B : AbelianVariety K} (n : ℤ) (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (A.mulBy n) f = CategoryTheory.CategoryStruct.comp f (B.mulBy n)

Every homomorphism of abelian varieties commutes with multiplication by n.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.congr_ofHom_mulBy {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) (n : ℤ) : (End.congr e) (End.ofHom (A.mulBy n)) = End.ofHom (B.mulBy n)

Conjugating [n] by an isomorphism of abelian varieties gives [n].

Deliberately not @[simp]: AbelianVariety.End.ofHom_mulBy rewrites both sides to an integer cast, so this left-hand side is not in simp normal form, and what is left is Mathlib's map_intCast.