Morphisms of abelian varieties preserving the identity are homomorphisms

A morphism f : A.toOver ⟶ B.toOver of the underlying schemes over Spec K that sends the identity of A to the identity of B is automatically a homomorphism of group schemes. The defect h (x, y) = f (x + y) - f x - f y is a morphism A.toOver ⊗ A.toOver ⟶ B.toOver that vanishes on A × {0}, so by TauCeti.AlgebraicGeometry.eq_snd_comp_lift_comp it depends only on y, and it vanishes on {0} × A.

Consequently the homomorphisms A ⟶ B of abelian varieties are exactly the pointed morphisms A.toOver ⟶ B.toOver over Spec K. This is how morphisms of abelian varieties arise in practice, for instance from the universal property of the Jacobian, where a morphism of schemes is produced first and only then recognised as a homomorphism.

Main declarations

• TauCeti.AlgebraicGeometry.isMonHom_of_one_hom: a morphism from a monoid scheme to a group scheme preserving the identity is a homomorphism when the source is proper and geometrically integral;
• TauCeti.AlgebraicGeometry.AbelianVariety.Hom.equivPointed: homomorphisms A ⟶ B are equivalent to the morphisms A.toOver ⟶ B.toOver preserving the identity.

References

• D. Mumford, Abelian Varieties, Section 4, Corollary 1 to the rigidity lemma.
• J. S. Milne, Abelian Varieties, Corollary 1.2.

theorem TauCeti.AlgebraicGeometry.isMonHom_of_one_hom {K : Type u} [Field K] {A B : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} [CategoryTheory.MonObj A] [CategoryTheory.GrpObj B] [AlgebraicGeometry.IsProper A.hom] [AlgebraicGeometry.GeometricallyIntegral A.hom] [AlgebraicGeometry.IsSeparated B.hom] [AlgebraicGeometry.LocallyOfFiniteType B.hom] (f : A ⟶ B) (hf : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one) : CategoryTheory.IsMonHom f

A morphism of monoid schemes over K from a proper geometrically integral source to a separated locally finite type group scheme is a homomorphism if it preserves the identity.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.equivPointed {K : Type u} [Field K] (A B : AbelianVariety K) : (A ⟶ B) ≃ { f : A.toOver ⟶ B.toOver // CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one }

Homomorphisms of abelian varieties are exactly the morphisms of the underlying schemes over Spec K preserving the identity.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverHom_equivPointed_symm_apply {K : Type u} [Field K] {A B : AbelianVariety K} (f : { f : A.toOver ⟶ B.toOver // CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one }) : toOverHom ((equivPointed A B).symm f) = ↑f

The homomorphism attached to a pointed morphism has that morphism as its morphism over Spec K.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.coe_equivPointed_apply {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) : ↑((Hom.equivPointed A B) f) = Hom.toOverHom f

The pointed morphism underlying a homomorphism is its morphism over Spec K.