Documentation

TauCeti.AlgebraicGeometry.AbelianVariety.Hom.Basic

Homomorphisms of abelian varieties #

This file supplies the morphism part of the basic abelian-variety API. A homomorphism of abelian varieties over K is a morphism over Spec K preserving the unit and multiplication of the underlying group schemes. Such morphisms form the category AbelianVariety K, inherited from Mathlib's category of commutative group objects.

The category morphism type A ⟶ B is the type required by the Jacobian's universal property: the factorization from the Jacobian to another abelian variety must preserve the group law, rather than being only a morphism of the underlying schemes. The characteristic lemmas expose preservation of the unit, multiplication, and inverse, as well as the forgetful functors to schemes over Spec K and to schemes.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer E, "Abelian variety = smooth, proper, geometrically connected group scheme over k; basic API", and prepares Layer F's unique "homomorphism of abelian varieties". No external mathematics is vendored; the implementation reuses Mathlib's CommGrp category and its IsMonHom API for group objects in a cartesian monoidal category.

source
@[instance_reducible]
noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.instCategory {K : Type u} [Field K] :
CategoryTheory.Category.{u, u + 1} (AbelianVariety K)

Abelian varieties over a fixed field form a category with group-scheme homomorphisms.

Equations
  • One or more equations did not get rendered due to their size.
source
noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.mk' {K : Type u} [Field K] {A B : AbelianVariety K} (f : A.toOver ⟶ B.toOver) (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.MonObj.mul := by cat_disch) :
A ⟶ B

Construct a homomorphism of abelian varieties from a morphism over Spec K and proofs that it preserves the unit and multiplication.

Equations
Instances For
    source
    noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverFunctor {K : Type u} [Field K] :
    CategoryTheory.Functor (AbelianVariety K) (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K))

    The forgetful functor from abelian varieties to schemes over Spec K.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverHom {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
      A.toOver ⟶ B.toOver

      The underlying morphism of group schemes over Spec K.

      Equations
      Instances For
        source
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverHom_id {K : Type u} [Field K] (A : AbelianVariety K) :
        toOverHom (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id A.toOver

        toOverHom sends the identity homomorphism to the identity over Spec K.

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

        toOverHom sends composition to composition over Spec K.

        source
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverHom_comp_assoc {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g : B ⟶ C) {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} (h : C.toOver ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (toOverHom (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (toOverHom f) (CategoryTheory.CategoryStruct.comp (toOverHom g) h)

        toOverHom sends composition to composition over Spec K.

        source
        instance TauCeti.AlgebraicGeometry.AbelianVariety.instIsMonHomOverSchemeSpecOfToOverHom {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
        CategoryTheory.IsMonHom (Hom.toOverHom f)

        The underlying morphism of an abelian-variety homomorphism preserves the group-object structure.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toOverHom_mk' {K : Type u} [Field K] {A B : AbelianVariety K} (f : A.toOver ⟶ B.toOver) (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.MonObj.mul := by cat_disch) :
        toOverHom (mk' f one_f mul_f) = f

        The underlying morphism over Spec K of a homomorphism built by Hom.mk' is the supplied morphism.

        source
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.one_hom {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
        CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (toOverHom f) = CategoryTheory.MonObj.one

        A homomorphism of abelian varieties preserves the unit section.

        source
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.one_hom_assoc {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} (h : B.toOver ⟶ Z) :
        CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp (toOverHom f) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h

        A homomorphism of abelian varieties preserves the unit section.

        source
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.mul_hom {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
        CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (toOverHom f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (toOverHom f) (toOverHom f)) CategoryTheory.MonObj.mul

        A homomorphism of abelian varieties preserves multiplication.

        source
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.mul_hom_assoc {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} (h : B.toOver ⟶ Z) :
        CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp (toOverHom f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (toOverHom f) (toOverHom f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)

        A homomorphism of abelian varieties preserves multiplication.

        source
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.inv_hom {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
        CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv (toOverHom f) = CategoryTheory.CategoryStruct.comp (toOverHom f) CategoryTheory.GrpObj.inv

        A homomorphism of abelian varieties preserves inverses.

        source
        theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.inv_hom_assoc {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)} (h : B.toOver ⟶ Z) :
        CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv (CategoryTheory.CategoryStruct.comp (toOverHom f) h) = CategoryTheory.CategoryStruct.comp (toOverHom f) (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h)

        A homomorphism of abelian varieties preserves inverses.

        source
        noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeFunctor {K : Type u} [Field K] :
        CategoryTheory.Functor (AbelianVariety K) AlgebraicGeometry.Scheme

        The forgetful functor from abelian varieties to their underlying schemes.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeFunctor_obj {K : Type u} [Field K] (A : AbelianVariety K) :
          toSchemeFunctor.obj A = A.toScheme

          The object map of Hom.toSchemeFunctor returns the underlying scheme.

          source
          @[reducible, inline]
          noncomputable abbrev TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeHom {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
          A.toScheme ⟶ B.toScheme

          The underlying morphism between the schemes of two abelian varieties.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeFunctor_map {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
            toSchemeFunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (toSchemeHom f) (CategoryTheory.eqToHom ⋯))

            The morphism map of Hom.toSchemeFunctor returns the underlying scheme morphism, transported along its object-map equalities.

            source
            @[simp]
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeHom_mk' {K : Type u} [Field K] {A B : AbelianVariety K} (f : A.toOver ⟶ B.toOver) (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.MonObj.mul := by cat_disch) :
            toSchemeHom (mk' f one_f mul_f) = CategoryTheory.Over.Hom.left f

            The underlying scheme morphism of a homomorphism built by Hom.mk' is the supplied morphism's left component.

            source
            @[simp]
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeHom_id {K : Type u} [Field K] (A : AbelianVariety K) :
            toSchemeHom (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id A.toScheme

            toSchemeHom sends the identity homomorphism to the identity scheme morphism.

            source
            @[simp]
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeHom_comp {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g : B ⟶ C) :
            toSchemeHom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (toSchemeHom f) (toSchemeHom g)

            toSchemeHom sends composition to composition of scheme morphisms.

            source
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeHom_comp_assoc {K : Type u} [Field K] {A B C : AbelianVariety K} (f : A ⟶ B) (g : B ⟶ C) {Z : AlgebraicGeometry.Scheme} (h : C.toScheme ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (toSchemeHom (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (toSchemeHom f) (CategoryTheory.CategoryStruct.comp (toSchemeHom g) h)

            toSchemeHom sends composition to composition of scheme morphisms.

            source
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeHom_comp_hom {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
            CategoryTheory.CategoryStruct.comp (toSchemeHom f) B.toOver.hom = A.toOver.hom

            The underlying scheme morphism of an abelian-variety homomorphism commutes with the structure morphisms to Spec K.

            source
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.toSchemeHom_comp_hom_assoc {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧K ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (toSchemeHom f) (CategoryTheory.CategoryStruct.comp B.toOver.hom h) = CategoryTheory.CategoryStruct.comp A.toOver.hom h

            The underlying scheme morphism of an abelian-variety homomorphism commutes with the structure morphisms to Spec K.

            source
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.ext {K : Type u} [Field K] {A B : AbelianVariety K} {f g : A ⟶ B} (h : toSchemeHom f = toSchemeHom g) :
            f = g

            Two homomorphisms of abelian varieties are equal when their underlying scheme morphisms are equal.

            source
            theorem TauCeti.AlgebraicGeometry.AbelianVariety.Hom.ext_iff {K : Type u} [Field K] {A B : AbelianVariety K} {f g : A ⟶ B} :
            f = g ↔ toSchemeHom f = toSchemeHom g
            source
            instance TauCeti.AlgebraicGeometry.AbelianVariety.instFaithfulOverSchemeSpecOfToOverFunctor {K : Type u} [Field K] :
            Hom.toOverFunctor.Faithful

            Forgetting an abelian-variety homomorphism to its underlying morphism over Spec K is faithful.

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

            Two homomorphisms of abelian varieties with the same underlying morphism over Spec K are equal.