The group of homomorphisms of abelian varieties

For abelian varieties A B : AbelianVariety K, the homomorphisms A ⟶ B form a commutative group under the pointwise group law of the target: since the group scheme underlying B is commutative, the pointwise product f * g := lift f g ≫ μ[B] of two homomorphisms is again a homomorphism. This file transports Mathlib's group structure on morphisms into a commutative group object (CategoryTheory.MonObj.Hom.commGroup, applied in the category of group objects over Spec K) onto A ⟶ B, and records how the underlying morphism over Spec K interacts with the group operations.

The group law is written multiplicatively, matching the multiplicative encoding (GrpObj, μ, η, ι) of the group-object structure carried by an AbelianVariety; for the Jacobian this pointwise product is the tensor product of line bundles.

• AbelianVariety.Hom.instCommGroup: the commutative group structure on A ⟶ B (a scoped instance);
• AbelianVariety.Hom.homMulEquiv: the identification of A ⟶ B with homomorphisms of the underlying commutative group objects as a multiplicative equivalence;
• AbelianVariety.Hom.toOverHom_mul, toOverHom_one, toOverHom_inv, toOverHom_div: the underlying morphism over Spec K is a homomorphism of these groups;
• AbelianVariety.Hom.mul_comp and AbelianVariety.Hom.comp_mul: composition is bimultiplicative, so AbelianVariety K behaves like a preadditive category with respect to this group law;
• AbelianVariety.Hom.leftComp and AbelianVariety.Hom.rightComp: the same bimultiplicativity in bundled form, as homomorphisms of the homomorphism groups, with Hom.comp_zpow and Hom.zpow_comp the resulting integer-power laws.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer E, "Abelian variety = smooth, proper, geometrically connected group scheme over k; basic API", by supplying the group structure on the homomorphism sets. Layer F's universal property produces a unique homomorphism of abelian varieties; the group law here is the ambient structure in which that uniqueness and the Albanese functoriality are expressed. No external mathematics is vendored; the group structure is transported from Mathlib's CategoryTheory.MonObj.Hom.commGroup on morphisms into a commutative group object, via the existing Tau Ceti abelian-variety homomorphism API.

@[instance_reducible]

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.instCommGroup {K : Type u} [Field K] (A B : AbelianVariety K) : CommGroup (A ⟶ B)

Homomorphisms of abelian varieties over K form a commutative group under the pointwise group law of the target, transported from Mathlib's group structure on morphisms into a commutative group object.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.Hom.instCommGroup A B = (CategoryTheory.InducedCategory.homEquiv.trans CategoryTheory.InducedCategory.homEquiv).commGroup

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.homMulEquiv {K : Type u} [Field K] (A B : AbelianVariety K) : (A ⟶ B) ≃* ({ X := A.toOver, grp := A.grpObj, comm := ⋯ }.toGrp ⟶ { X := B.toOver, grp := B.grpObj, comm := ⋯ }.toGrp)

Identifying a homomorphism of abelian varieties with its underlying homomorphism of commutative group objects is a group isomorphism onto the latter's group of homomorphisms.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.Hom.homMulEquiv A B = { toEquiv := CategoryTheory.InducedCategory.homEquiv.trans CategoryTheory.InducedCategory.homEquiv, map_mul' := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.homMulEquiv_apply {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) : (homMulEquiv A B) f = f.hom.hom

The hom-set multiplicative equivalence evaluates to the nested underlying group-object homomorphism.

@[simp]

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

The underlying morphism over Spec K sends the product of two homomorphisms to the pointwise product.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverHom_one {K : Type u} [Field K] {A B : AbelianVariety K} : toOverHom 1 = 1

The underlying morphism over Spec K sends the identity of the group of homomorphisms to the identity element toUnit A.toOver ≫ η[B.toOver] (the constant homomorphism through the unit section).

@[simp]

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

The underlying morphism over Spec K sends the inverse of a homomorphism to the pointwise inverse.

@[simp]

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

The underlying morphism over Spec K sends the quotient of two homomorphisms to the pointwise quotient.

Bilinearity of composition

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.mul_comp {K : Type u} [Field K] {A B C : AbelianVariety K} (f g : A ⟶ B) (h : B ⟶ C) : CategoryTheory.CategoryStruct.comp (f * g) h = CategoryTheory.CategoryStruct.comp f h * CategoryTheory.CategoryStruct.comp g h

Composition of homomorphisms of abelian varieties distributes over the pointwise product on the right: post-composition by a homomorphism is multiplicative.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.mul_comp_assoc {K : Type u} [Field K] {A B C : AbelianVariety K} (f g : A ⟶ B) (h : B ⟶ C) {Z : AbelianVariety K} (h✝ : C ⟶ Z) : CategoryTheory.CategoryStruct.comp (f * g) (CategoryTheory.CategoryStruct.comp h h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h * CategoryTheory.CategoryStruct.comp g h) h✝

Composition of homomorphisms of abelian varieties distributes over the pointwise product on the right: post-composition by a homomorphism is multiplicative.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.comp_mul {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g h : B ⟶ C) : CategoryTheory.CategoryStruct.comp f (g * h) = CategoryTheory.CategoryStruct.comp f g * CategoryTheory.CategoryStruct.comp f h

Composition of homomorphisms of abelian varieties distributes over the pointwise product on the left: pre-composition by a homomorphism is multiplicative.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.comp_mul_assoc {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g h : B ⟶ C) {Z : AbelianVariety K} (h✝ : C ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g * h) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g * CategoryTheory.CategoryStruct.comp f h) h✝

Composition of homomorphisms of abelian varieties distributes over the pointwise product on the left: pre-composition by a homomorphism is multiplicative.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.one_comp {K : Type u} [Field K] {A B C : AbelianVariety K} (h : B ⟶ C) : CategoryTheory.CategoryStruct.comp 1 h = 1

Post-composition sends the identity element of a homomorphism group to the identity element.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.comp_one {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp f 1 = 1

Pre-composition sends the identity element of a homomorphism group to the identity element.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.inv_comp {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (h : B ⟶ C) : CategoryTheory.CategoryStruct.comp f⁻¹ h = (CategoryTheory.CategoryStruct.comp f h)⁻¹

Post-composition preserves pointwise inverses of homomorphisms.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.div_comp {K : Type u} [Field K] {A B C : AbelianVariety K} (f g : A ⟶ B) (h : B ⟶ C) : CategoryTheory.CategoryStruct.comp (f / g) h = CategoryTheory.CategoryStruct.comp f h / CategoryTheory.CategoryStruct.comp g h

Post-composition preserves pointwise quotients of homomorphisms.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.comp_inv {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g : B ⟶ C) : CategoryTheory.CategoryStruct.comp f g⁻¹ = (CategoryTheory.CategoryStruct.comp f g)⁻¹

Pre-composition preserves pointwise inverses of homomorphisms.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.comp_div {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g h : B ⟶ C) : CategoryTheory.CategoryStruct.comp f (g / h) = CategoryTheory.CategoryStruct.comp f g / CategoryTheory.CategoryStruct.comp f h

Pre-composition preserves pointwise quotients of homomorphisms.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.leftComp {K : Type u} [Field K] {A B : AbelianVariety K} (C : AbelianVariety K) (f : A ⟶ B) : (B ⟶ C) →* (A ⟶ C)

Pre-composition by a fixed homomorphism, bundled as a homomorphism of the pointwise homomorphism groups. This is Hom.comp_mul in bundled form; the name follows Mathlib's CategoryTheory.Preadditive.leftComp.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.Hom.leftComp C f = { toFun := fun (g : B ⟶ C) => CategoryTheory.CategoryStruct.comp f g, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.rightComp {K : Type u} [Field K] (A : AbelianVariety K) {B C : AbelianVariety K} (g : B ⟶ C) : (A ⟶ B) →* (A ⟶ C)

Post-composition by a fixed homomorphism, bundled as a homomorphism of the pointwise homomorphism groups. This is Hom.mul_comp in bundled form; the name follows Mathlib's CategoryTheory.Preadditive.rightComp.

Equations

• TauCeti.AlgebraicGeometry.AbelianVariety.Hom.rightComp A g = { toFun := fun (f : A ⟶ B) => CategoryTheory.CategoryStruct.comp f g, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.comp_zpow {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g : B ⟶ C) (n : ℤ) : CategoryTheory.CategoryStruct.comp f (g ^ n) = CategoryTheory.CategoryStruct.comp f g ^ n

Pre-composition by a homomorphism preserves pointwise integer powers.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.zpow_comp {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g : B ⟶ C) (n : ℤ) : CategoryTheory.CategoryStruct.comp (f ^ n) g = CategoryTheory.CategoryStruct.comp f g ^ n

Post-composition by a homomorphism preserves pointwise integer powers.