Documentation

TauCeti.AlgebraicGeometry.AbelianVariety.Hom.Iso

Isomorphisms of abelian varieties #

This file supplies the scheme-level interface to isomorphisms in the category of abelian varieties. An isomorphism e : A ≅ B forgets first to an isomorphism of schemes over Spec K, then to an isomorphism of the underlying schemes.

As a first geometric consequence, isomorphic abelian varieties have the same dimension. This is the interface needed to compare constructions characterized by the Jacobian's universal property and to state its base-change compatibility as an isomorphism of abelian varieties.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer E, “Abelian variety = smooth, proper, geometrically connected group scheme over k; basic API, dim,” and prepares the isomorphisms in the end goal and Layer F. No external mathematics is vendored. The implementation reuses Mathlib's Functor.mapIso, Over.forget.mapIso, and invariance of topological Krull dimension under homeomorphism.

source
noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.isoToOver {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
A.toOver ≅ B.toOver

The isomorphism of schemes over Spec K underlying an isomorphism of abelian varieties.

Equations
Instances For
    source
    noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.isoToScheme {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
    A.toScheme ≅ B.toScheme

    The isomorphism of schemes underlying an isomorphism of abelian varieties.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToOver_hom {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
      (isoToOver e).hom = Hom.toOverHom e.hom

      The forward map of the underlying Over isomorphism is the underlying homomorphism.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToOver_inv {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
      (isoToOver e).inv = Hom.toOverHom e.inv

      The inverse map of the underlying Over isomorphism is the underlying homomorphism.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToScheme_hom {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
      (isoToScheme e).hom = Hom.toSchemeHom e.hom

      The forward map of the underlying scheme isomorphism is the underlying scheme morphism.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToScheme_inv {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
      (isoToScheme e).inv = Hom.toSchemeHom e.inv

      The inverse map of the underlying scheme isomorphism is the underlying scheme morphism.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToOver_refl {K : Type u} [Field K] (A : AbelianVariety K) :
      isoToOver (CategoryTheory.Iso.refl A) = CategoryTheory.Iso.refl A.toOver

      The underlying Over isomorphism of the identity isomorphism is the identity.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToOver_symm {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
      isoToOver e.symm = (isoToOver e).symm

      Forgetting an inverse isomorphism over the base commutes with taking inverses.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToOver_trans {K : Type u} [Field K] {A B C : AbelianVariety K} (e : A ≅ B) (f : B ≅ C) :
      isoToOver (e ≪≫ f) = isoToOver e ≪≫ isoToOver f

      Forgetting a composite isomorphism over the base commutes with composition.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToScheme_refl {K : Type u} [Field K] (A : AbelianVariety K) :
      isoToScheme (CategoryTheory.Iso.refl A) = CategoryTheory.Iso.refl A.toScheme

      The underlying scheme isomorphism of the identity isomorphism is the identity.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToScheme_symm {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
      isoToScheme e.symm = (isoToScheme e).symm

      Forgetting an inverse isomorphism of schemes commutes with taking inverses.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isoToScheme_trans {K : Type u} [Field K] {A B C : AbelianVariety K} (e : A ≅ B) (f : B ≅ C) :
      isoToScheme (e ≪≫ f) = isoToScheme e ≪≫ isoToScheme f

      Forgetting a composite isomorphism of schemes commutes with composition.

      source
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.dim_eq_of_iso {K : Type u} [Field K] {A B : AbelianVariety K} (e : A ≅ B) :
      A.dim = B.dim

      Isomorphic abelian varieties have equal topological Krull dimension.