Products of abelian varieties

This file constructs the product of two abelian varieties over a field. Its underlying scheme is the fibre product over the base field, equipped with the componentwise group law. The projections and pairing operation exhibit this construction as the categorical binary product in AbelianVariety K.

Finite products are part of the basic abelian-variety API required in Layer E of TauCetiRoadmap/JacobianChallenge/README.md. In particular, the theorem of the cube and the duality and polarization theory in that layer use powers of an abelian variety. No external formalization is vendored; the construction reuses Mathlib's cartesian monoidal structures on Over (Spec K) and on internal commutative groups.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.prod {K : Type u} [Field K] (A B : AbelianVariety K) : AbelianVariety K

The product of two abelian varieties over K. Its underlying scheme is their fibre product over Spec K, and its group law is componentwise.

Equations

• A.prod B = TauCeti.AlgebraicGeometry.AbelianVariety.ofGeometricallyIntegral (CategoryTheory.MonoidalCategoryStruct.tensorObj A.toOver B.toOver)

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod_toOver {K : Type u} [Field K] (A B : AbelianVariety K) : (A.prod B).toOver = CategoryTheory.MonoidalCategoryStruct.tensorObj A.toOver B.toOver

The group scheme underlying a product is the fibre product group scheme.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod_toScheme {K : Type u} [Field K] (A B : AbelianVariety K) : (A.prod B).toScheme = CategoryTheory.Limits.pullback A.toOver.hom B.toOver.hom

The scheme underlying a product is the fibre product of the two underlying schemes over Spec K.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod_one {K : Type u} [Field K] (A B : AbelianVariety K) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.eqToHom ⋯) = CategoryTheory.MonObj.one

The unit section of a product is the componentwise unit section.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod_mul {K : Type u} [Field K] (A B : AbelianVariety K) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) CategoryTheory.MonObj.mul

The multiplication on a product is componentwise multiplication.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod_inv {K : Type u} [Field K] (A B : AbelianVariety K) : CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) CategoryTheory.GrpObj.inv

Inversion on a product is componentwise inversion.

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

The first projection from a product of abelian varieties.

Equations

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

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

The second projection from a product of abelian varieties.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.prod.lift {K : Type u} [Field K] {A B C : AbelianVariety K} (f : C ⟶ A) (g : C ⟶ B) : C ⟶ A.prod B

Pair two homomorphisms with a common source to obtain a homomorphism into a product.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.toOverHom_fst {K : Type u} [Field K] (A B : AbelianVariety K) : Hom.toOverHom (fst A B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toOver B.toOver)

The morphism over Spec K underlying the first projection is the pullback projection.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.toOverHom_snd {K : Type u} [Field K] (A B : AbelianVariety K) : Hom.toOverHom (snd A B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.SemiCartesianMonoidalCategory.snd A.toOver B.toOver)

The morphism over Spec K underlying the second projection is the pullback projection.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.toOverHom_lift {K : Type u} [Field K] {A B C : AbelianVariety K} (f : C ⟶ A) (g : C ⟶ B) : Hom.toOverHom (lift f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (Hom.toOverHom f) (Hom.toOverHom g)) (CategoryTheory.eqToHom ⋯)

The morphism over Spec K underlying a pairing is the corresponding pullback lift.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.lift_fst {K : Type u} [Field K] {A B C : AbelianVariety K} (f : C ⟶ A) (g : C ⟶ B) : CategoryTheory.CategoryStruct.comp (lift f g) (fst A B) = f

The first projection of a pairing is its first component.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.lift_snd {K : Type u} [Field K] {A B C : AbelianVariety K} (f : C ⟶ A) (g : C ⟶ B) : CategoryTheory.CategoryStruct.comp (lift f g) (snd A B) = g

The second projection of a pairing is its second component.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.hom_ext {K : Type u} [Field K] {A B C : AbelianVariety K} {f g : C ⟶ A.prod B} (hfst : CategoryTheory.CategoryStruct.comp f (fst A B) = CategoryTheory.CategoryStruct.comp g (fst A B)) (hsnd : CategoryTheory.CategoryStruct.comp f (snd A B) = CategoryTheory.CategoryStruct.comp g (snd A B)) : f = g

Homomorphisms into a product are determined by their two projections.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.hom_ext_iff {K : Type u} [Field K] {A B C : AbelianVariety K} {f g : C ⟶ A.prod B} : f = g ↔ CategoryTheory.CategoryStruct.comp f (fst A B) = CategoryTheory.CategoryStruct.comp g (fst A B) ∧ CategoryTheory.CategoryStruct.comp f (snd A B) = CategoryTheory.CategoryStruct.comp g (snd A B)

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.comp_lift {K : Type u} [Field K] {A B C D : AbelianVariety K} (h : D ⟶ C) (f : C ⟶ A) (g : C ⟶ B) : CategoryTheory.CategoryStruct.comp h (lift f g) = lift (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)

Precomposing a pairing composes each of its components.

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

Precomposing a pairing composes each of its components.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.prod.lift_comp_fst_snd {K : Type u} [Field K] {A B C : AbelianVariety K} (f : C ⟶ A.prod B) : lift (CategoryTheory.CategoryStruct.comp f (fst A B)) (CategoryTheory.CategoryStruct.comp f (snd A B)) = f

Pairing the two projections of a homomorphism into a product recovers that homomorphism.

instance TauCeti.AlgebraicGeometry.AbelianVariety.hasBinaryProduct {K : Type u} [Field K] (A B : AbelianVariety K) : CategoryTheory.Limits.HasBinaryProduct A B

The concrete product supplies the categorical binary product of abelian varieties.

instance TauCeti.AlgebraicGeometry.AbelianVariety.hasBinaryProducts {K : Type u} [Field K] : CategoryTheory.Limits.HasBinaryProducts (AbelianVariety K)

Abelian varieties over a field have categorical binary products.

instance TauCeti.AlgebraicGeometry.AbelianVariety.hasFiniteProducts {K : Type u} [Field K] : CategoryTheory.Limits.HasFiniteProducts (AbelianVariety K)

Abelian varieties over a field have all finite products.