The Albanese property of a pointed morphism to an abelian variety

Let X be a scheme over a field K with a K-rational point x₀ : Spec K ⟶ X, written as a morphism 𝟙_ (Over (Spec K)) ⟶ X over Spec K. A pointed morphism a : X ⟶ J to an abelian variety J (one sending x₀ to the identity of J) has the Albanese property if every pointed morphism f : X ⟶ A to an abelian variety A factors as f = a ≫ φ through a unique homomorphism φ : J ⟶ A of abelian varieties. This is the universal property characterizing the Jacobian Jac X = Pic⁰ X of a smooth proper geometrically connected curve together with its Abel–Jacobi morphism aj : X ⟶ Jac X, x₀ ↦ 0: for curves the Jacobian is the Albanese variety.

The universal property makes any two solutions canonically isomorphic (IsAlbanese.uniqueUpToIso), so independently built Jacobians are compared through it rather than through their constructions. A pointed isomorphism onto an abelian variety has the Albanese property (isAlbanese_of_isIso), because pointed morphisms between abelian varieties are homomorphisms (AbelianVariety.Hom.equivPointed, a consequence of the rigidity lemma); in particular every abelian variety A, pointed at its identity, is its own Albanese variety via the identity morphism (isAlbanese_id). Combined with IsAlbanese.uniqueUpToIso, any Albanese morphism a : A ⟶ J for (A, 0) therefore identifies J with A; this is the form of the genus-one comparison Jac (E, O) ≅ E once an elliptic curve is known to be an abelian variety.

Main declarations

• AbelianVariety.IsAlbanese x₀ a: the pointed morphism a : X ⟶ J.toOver has the Albanese property;
• AbelianVariety.IsAlbanese.homEquiv: homomorphisms J ⟶ A are in bijection with pointed morphisms X ⟶ A.toOver, by composition with a;
• AbelianVariety.IsAlbanese.lift, AbelianVariety.IsAlbanese.fac, AbelianVariety.IsAlbanese.hom_ext: the factorization of a pointed morphism through a and its uniqueness;
• AbelianVariety.IsAlbanese.uniqueUpToIso: two Albanese morphisms from the same pointed scheme have isomorphic targets, compatibly with the morphisms;
• AbelianVariety.IsAlbanese.of_iso: the Albanese property is transported along isomorphisms of the target;
• AbelianVariety.isAlbanese_of_isIso: a pointed isomorphism onto an abelian variety has the Albanese property;
• AbelianVariety.isAlbanese_id: an abelian variety pointed at its identity is its own Albanese variety;
• AbelianVariety.isAlbanese_trivial: the Albanese variety of Spec K is the trivial abelian variety.

References

• J. S. Milne, Jacobian varieties, in Arithmetic Geometry (G. Cornell and J. H. Silverman, eds.), Springer, 1986, Section 6 (the universal property of the Abel–Jacobi map).
• J. S. Milne, Abelian Varieties, Corollary 1.2 (pointed morphisms of abelian varieties are homomorphisms).

structure TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} (x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X) {J : AbelianVariety K} (a : X ⟶ J.toOver) : Prop

A pointed morphism a : X ⟶ J.toOver from a scheme X over K with a K-rational point x₀ to an abelian variety J has the Albanese property if every morphism f : X ⟶ A.toOver to an abelian variety sending x₀ to the identity factors as f = a ≫ φ through a unique homomorphism φ : J ⟶ A of abelian varieties.

• comp_eq_one : CategoryTheory.CategoryStruct.comp x₀ a = CategoryTheory.MonObj.one

  The morphism a sends the base point x₀ to the identity of J.

• existsUnique_fac (A : AbelianVariety K) (f : X ⟶ A.toOver) (hf : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.MonObj.one) : ∃! φ : J ⟶ A, CategoryTheory.CategoryStruct.comp a (Hom.toOverHom φ) = f

  Every pointed morphism to an abelian variety factors uniquely through a by a homomorphism.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.comp_toOverHom_eq_one {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J A : AbelianVariety K} {a : X ⟶ J.toOver} (ha : CategoryTheory.CategoryStruct.comp x₀ a = CategoryTheory.MonObj.one) (φ : J ⟶ A) : CategoryTheory.CategoryStruct.comp x₀ (CategoryTheory.CategoryStruct.comp a (Hom.toOverHom φ)) = CategoryTheory.MonObj.one

Composing a pointed morphism with a homomorphism of abelian varieties gives a pointed morphism.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.homEquiv {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) (A : AbelianVariety K) : (J ⟶ A) ≃ { f : X ⟶ A.toOver // CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.MonObj.one }

Homomorphisms out of the Albanese variety J are the pointed morphisms out of X: a homomorphism φ : J ⟶ A corresponds to a ≫ φ.

Equations

• h.homEquiv A = Equiv.ofBijective (fun (φ : J ⟶ A) => ⟨CategoryTheory.CategoryStruct.comp a (TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverHom φ), ⋯⟩) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.coe_homEquiv_apply {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A : AbelianVariety K} (φ : J ⟶ A) : ↑((h.homEquiv A) φ) = CategoryTheory.CategoryStruct.comp a (Hom.toOverHom φ)

homEquiv sends a homomorphism φ : J ⟶ A to the pointed morphism a ≫ φ.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.lift {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A : AbelianVariety K} (f : X ⟶ A.toOver) (hf : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.MonObj.one) : J ⟶ A

The homomorphism J ⟶ A through which a pointed morphism f : X ⟶ A.toOver factors.

Equations

• h.lift f hf = (h.homEquiv A).symm ⟨f, hf⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.homEquiv_symm_apply {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A : AbelianVariety K} (f : { f : X ⟶ A.toOver // CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.MonObj.one }) : (h.homEquiv A).symm f = h.lift ↑f ⋯

The inverse of homEquiv is lift.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.fac {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A : AbelianVariety K} (f : X ⟶ A.toOver) (hf : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp a (Hom.toOverHom (h.lift f hf)) = f

The homomorphism lift f factors f through the Albanese morphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.fac_assoc {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A : AbelianVariety K} (f : X ⟶ A.toOver) (hf : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.MonObj.one) {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} (h✝ : A.toOver ⟶ Z) : CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (Hom.toOverHom (h.lift f hf)) h✝) = CategoryTheory.CategoryStruct.comp f h✝

The homomorphism lift f factors f through the Albanese morphism.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.hom_ext {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A : AbelianVariety K} {φ ψ : J ⟶ A} (e : CategoryTheory.CategoryStruct.comp a (Hom.toOverHom φ) = CategoryTheory.CategoryStruct.comp a (Hom.toOverHom ψ)) : φ = ψ

Two homomorphisms out of the Albanese variety agree once they agree after composition with the Albanese morphism.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.eq_lift_iff {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A : AbelianVariety K} {f : X ⟶ A.toOver} (hf : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.MonObj.one) {φ : J ⟶ A} : φ = h.lift f hf ↔ CategoryTheory.CategoryStruct.comp a (Hom.toOverHom φ) = f

A homomorphism out of the Albanese variety is the lift of a pointed morphism exactly when it factors that morphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.lift_comp_toOverHom {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A : AbelianVariety K} (φ : J ⟶ A) : h.lift (CategoryTheory.CategoryStruct.comp a (Hom.toOverHom φ)) ⋯ = φ

Lifting the composite of the Albanese morphism with a homomorphism recovers the homomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.lift_self {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) : h.lift a ⋯ = CategoryTheory.CategoryStruct.id J

The lift of the Albanese morphism itself is the identity.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.lift_comp {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {A B : AbelianVariety K} (f : X ⟶ A.toOver) (hf : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.MonObj.one) (ψ : A ⟶ B) : CategoryTheory.CategoryStruct.comp (h.lift f hf) ψ = h.lift (CategoryTheory.CategoryStruct.comp f (Hom.toOverHom ψ)) ⋯

Lifting is compatible with composition by a homomorphism on the target.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.uniqueUpToIso {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {J' : AbelianVariety K} {a' : X ⟶ J'.toOver} (h' : IsAlbanese x₀ a') : J ≅ J'

The Albanese variety is unique up to unique isomorphism: if a : X ⟶ J and a' : X ⟶ J' both have the Albanese property for the base point x₀, then J ≅ J' by the isomorphism carrying a to a'.

Equations

• h.uniqueUpToIso h' = { hom := h.lift a' ⋯, inv := h'.lift a ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.comp_uniqueUpToIso_hom {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {J' : AbelianVariety K} {a' : X ⟶ J'.toOver} (h' : IsAlbanese x₀ a') : CategoryTheory.CategoryStruct.comp a (Hom.toOverHom (h.uniqueUpToIso h').hom) = a'

The isomorphism uniqueUpToIso carries the first Albanese morphism to the second.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.comp_uniqueUpToIso_hom_assoc {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {J' : AbelianVariety K} {a' : X ⟶ J'.toOver} (h' : IsAlbanese x₀ a') {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} (h✝ : J'.toOver ⟶ Z) : CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (Hom.toOverHom (h.uniqueUpToIso h').hom) h✝) = CategoryTheory.CategoryStruct.comp a' h✝

The isomorphism uniqueUpToIso carries the first Albanese morphism to the second.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.comp_uniqueUpToIso_inv {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {J' : AbelianVariety K} {a' : X ⟶ J'.toOver} (h' : IsAlbanese x₀ a') : CategoryTheory.CategoryStruct.comp a' (Hom.toOverHom (h.uniqueUpToIso h').inv) = a

The inverse of uniqueUpToIso carries the second Albanese morphism to the first.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.comp_uniqueUpToIso_inv_assoc {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {J' : AbelianVariety K} {a' : X ⟶ J'.toOver} (h' : IsAlbanese x₀ a') {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} (h✝ : J.toOver ⟶ Z) : CategoryTheory.CategoryStruct.comp a' (CategoryTheory.CategoryStruct.comp (Hom.toOverHom (h.uniqueUpToIso h').inv) h✝) = CategoryTheory.CategoryStruct.comp a h✝

The inverse of uniqueUpToIso carries the second Albanese morphism to the first.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.eq_uniqueUpToIso_hom {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {J' : AbelianVariety K} {a' : X ⟶ J'.toOver} (h' : IsAlbanese x₀ a') {φ : J ⟶ J'} (e : CategoryTheory.CategoryStruct.comp a (Hom.toOverHom φ) = a') : φ = (h.uniqueUpToIso h').hom

The isomorphism uniqueUpToIso is the only homomorphism carrying the first Albanese morphism to the second.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.of_iso {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {J : AbelianVariety K} {a : X ⟶ J.toOver} (h : IsAlbanese x₀ a) {J' : AbelianVariety K} (e : J ≅ J') : IsAlbanese x₀ (CategoryTheory.CategoryStruct.comp a (Hom.toOverHom e.hom))

The Albanese property is transported along an isomorphism of the target abelian variety.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.isAlbanese_of_isIso {K : Type u} [Field K] {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} {x₀ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ X} {A : AbelianVariety K} (a : X ⟶ A.toOver) [CategoryTheory.IsIso a] (ha : CategoryTheory.CategoryStruct.comp x₀ a = CategoryTheory.MonObj.one) : IsAlbanese x₀ a

A pointed isomorphism a : X ⟶ A.toOver onto an abelian variety has the Albanese property: for a pointed morphism f : X ⟶ B.toOver, the composite inv a ≫ f is a pointed morphism of abelian varieties, hence a homomorphism by rigidity.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.isAlbanese_id {K : Type u} [Field K] (A : AbelianVariety K) : IsAlbanese CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id A.toOver)

An abelian variety, pointed at its identity, is its own Albanese variety via the identity morphism: by rigidity, every pointed morphism A ⟶ B to an abelian variety is a homomorphism.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.isAlbanese_trivial {K : Type u} [Field K] : IsAlbanese (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)))) CategoryTheory.MonObj.one

The Albanese variety of Spec K, pointed by the identity, is the trivial abelian variety: the unit section of the trivial abelian variety is an isomorphism, both its source and target being terminal.