Base change of abelian-variety homomorphisms

This file makes extension of the base field functorial on abelian varieties. For a field extension K → L, pullback from schemes over Spec K to schemes over Spec L carries an abelian-variety homomorphism A ⟶ B to a homomorphism A.baseChange L ⟶ B.baseChange L. These maps assemble into AbelianVariety.baseChangeFunctor.

Base change also respects the pointwise group law on homomorphisms of TauCeti.AlgebraicGeometry.AbelianVariety.MorphismGroup: AbelianVariety.Hom.baseChangeMonoidHom bundles it as a homomorphism (A ⟶ B) →* (A.baseChange L ⟶ B.baseChange L) of the homomorphism groups, with AbelianVariety.Hom.baseChange_one, baseChange_mul, baseChange_inv, baseChange_div and baseChange_zpow its unbundled forms.

The construction advances TauCetiRoadmap/JacobianChallenge/README.md, Layer E's basic abelian-variety API and the base-change compatibility required in the end goal. It will allow the Jacobian base-change comparison to be stated and used as an isomorphism of abelian varieties, not merely as an isomorphism of their underlying schemes.

No external mathematics is vendored. The implementation uses Mathlib's lax monoidal pullback functor on Over categories, whose action on group objects proves that the pulled-back morphism preserves the unit and multiplication, together with Mathlib's multiplicativity of a monoidal functor on morphisms into a monoid object (CategoryTheory.Functor.map_mul).

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

Base change of a homomorphism of abelian varieties along a field extension.

This is the morphism obtained by applying pullback in the appropriate Over category. The monoidal structure on pullback ensures that it is again a group-scheme homomorphism.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverHom_baseChange {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) (L : Type u) [Field L] [Algebra K L] : toOverHom (baseChange f L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).map (toOverHom f)) (CategoryTheory.eqToHom ⋯))

The underlying morphism over Spec L of a base-changed homomorphism is the pullback of its underlying morphism over Spec K.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeHom_baseChange {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) (L : Type u) [Field L] [Algebra K L] : toSchemeHom (baseChange f L) = CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).map (toOverHom f)) (CategoryTheory.eqToHom ⋯)))

The underlying scheme morphism of a base-changed homomorphism is the left component of the pulled-back morphism in the Over category.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChange_id {K : Type u} [Field K] (A : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : baseChange (CategoryTheory.CategoryStruct.id A) L = CategoryTheory.CategoryStruct.id (A.baseChange L)

Base change preserves identity homomorphisms.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChange_comp {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g : B ⟶ C) (L : Type u) [Field L] [Algebra K L] : baseChange (CategoryTheory.CategoryStruct.comp f g) L = CategoryTheory.CategoryStruct.comp (baseChange f L) (baseChange g L)

Base change preserves composition of homomorphisms.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.baseChangeFunctor {K : Type u} [Field K] (L : Type u) [Field L] [Algebra K L] : CategoryTheory.Functor (AbelianVariety K) (AbelianVariety L)

Extension of the base field defines a functor between the categories of abelian varieties.

Its action is characterized by AbelianVariety.baseChangeFunctor_obj and AbelianVariety.baseChangeFunctor_map.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChangeFunctor_obj {K : Type u} [Field K] (L : Type u) [Field L] [Algebra K L] (A : AbelianVariety K) : (baseChangeFunctor L).obj A = A.baseChange L

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.baseChangeFunctor_map {K : Type u} [Field K] {A B : AbelianVariety K} (L : Type u) [Field L] [Algebra K L] (f : A ⟶ B) : (baseChangeFunctor L).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (Hom.baseChange f L) (CategoryTheory.eqToHom ⋯))

Compatibility with the pointwise group law

Base change is a homomorphism for the pointwise group law of TauCeti.AlgebraicGeometry.AbelianVariety.MorphismGroup, not merely a functor. The two private instances below say that the transport isomorphism eqToHom (baseChange_toOver A L) between the group scheme underlying A.baseChange L and the pullback of the one underlying A is an isomorphism of monoid objects; they are proof support for the two lemmas that follow, which together with Mathlib's multiplicativity of a monoidal functor on morphisms into a monoid object give the public interface.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChange_one {K : Type u} [Field K] (A B : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : baseChange 1 L = 1

Base change carries the identity element of the group of homomorphisms — the homomorphism factoring through the unit section — to the identity element.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChange_mul {K : Type u} [Field K] {A B : AbelianVariety K} (f g : A ⟶ B) (L : Type u) [Field L] [Algebra K L] : baseChange (f * g) L = baseChange f L * baseChange g L

Base change is multiplicative for the pointwise group law: pulling back the pointwise product of two homomorphisms gives the pointwise product of their pullbacks.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChangeMonoidHom {K : Type u} [Field K] (A B : AbelianVariety K) (L : Type u) [Field L] [Algebra K L] : (A ⟶ B) →* (A.baseChange L ⟶ B.baseChange L)

Base change along a field extension, as a homomorphism of the groups of homomorphisms of abelian varieties.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChangeMonoidHom_apply {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) (L : Type u) [Field L] [Algebra K L] : (baseChangeMonoidHom A B L) f = baseChange f L

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChange_inv {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) (L : Type u) [Field L] [Algebra K L] : baseChange f⁻¹ L = (baseChange f L)⁻¹

Base change preserves pointwise inverses of homomorphisms.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChange_div {K : Type u} [Field K] {A B : AbelianVariety K} (f g : A ⟶ B) (L : Type u) [Field L] [Algebra K L] : baseChange (f / g) L = baseChange f L / baseChange g L

Base change preserves pointwise quotients of homomorphisms.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.baseChange_zpow {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) (n : ℤ) (L : Type u) [Field L] [Algebra K L] : baseChange (f ^ n) L = baseChange f L ^ n

Base change preserves pointwise integer powers of homomorphisms.