Documentation

TauCeti.AlgebraicGeometry.AbelianVariety.End.BaseChange

Base change of the endomorphism ring of an abelian variety #

Extending the base field along K → L sends an endomorphism of an abelian variety A over K to an endomorphism of A.baseChange L. This assignment is a ring homomorphism AbelianVariety.End.baseChange : End A →+* End (A.baseChange L): it is additive because base change respects the pointwise group law on homomorphisms (AbelianVariety.Hom.baseChangeMonoidHom), and multiplicative because it is functorial (AbelianVariety.Hom.baseChange_comp).

The last statement is the concrete check that the ring homomorphism is the expected one: [n] is the image of the integer n in the endomorphism ring, and a ring homomorphism preserves integers, so [n] is intrinsic to the abelian variety and does not depend on the base field. That is also what a later Layer E statement about [n] being an isogeny needs in order to be checked after base change to an algebraic closure.

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", together with the base-change compatibility required in the roadmap's end goal: the Jacobian's universal property produces homomorphisms of abelian varieties, and comparing them after base change is exactly comparing them in the base-changed endomorphism ring.

No external mathematics is vendored. The ring structure is Mathlib's, transported along the already-established base-change functoriality of abelian-variety homomorphisms.

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

Extension of the base field along K → L, as a ring homomorphism between endomorphism rings.

Addition in an endomorphism ring is the pointwise group law of the abelian variety and multiplication is composition, so additivity is AbelianVariety.Hom.baseChange_mul and multiplicativity is AbelianVariety.Hom.baseChange_comp (composition being taken in the reversed order in which AbelianVariety.End multiplies).

The action is characterized by AbelianVariety.End.toHom_baseChange and AbelianVariety.End.baseChange_ofHom, so the implementation is not exposed.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.toHom_baseChange {K : Type u} [Field K] {A : AbelianVariety K} {L : Type u} [Field L] [Algebra K L] (x : A.End) :
    ((baseChange A L) x).toHom = Hom.baseChange x.toHom L

    The endomorphism denoted by a base-changed element of the endomorphism ring is the base change of the endomorphism denoted by that element.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.baseChange_ofHom {K : Type u} [Field K] {A : AbelianVariety K} {L : Type u} [Field L] [Algebra K L] (f : A ⟶ A) :
    (baseChange A L) (ofHom f) = ofHom (Hom.baseChange f L)

    Base change of an endomorphism, read back in the endomorphism ring.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.AbelianVariety.End.baseChange_congr {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) (L : Type u) [Field L] [Algebra K L] (x : A.End) :
    (baseChange B L) ((congr e) x) = (congr (CategoryTheory.eqToIso ⋯ ≪≫ (baseChangeFunctor L).mapIso e ≪≫ CategoryTheory.eqToIso ⋯)) ((baseChange A L) x)

    Base change commutes with conjugation by an isomorphism of abelian varieties: conjugating and then extending the base field is the same as extending the base field and conjugating by the base-changed isomorphism, CategoryTheory.Functor.mapIso for AbelianVariety.baseChangeFunctor.

    Functor.mapIso produces an isomorphism (baseChangeFunctor L).obj A ≅ (baseChangeFunctor L).obj B and AbelianVariety.baseChangeFunctor_obj identifies its endpoints with the base changes, so the conjugating isomorphism is the composite of the three; writing it that way keeps the statement type-correct without unfolding the functor.

    Multiplication by n #

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChange_mulBy {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] (n : ℤ) :
    Hom.baseChange (A.mulBy n) L = (A.baseChange L).mulBy n

    Multiplication by n is compatible with extension of the base field.