Documentation

TauCeti.AlgebraicGeometry.AbelianVariety.Isogeny

Isogenies of abelian varieties #

An isogeny of abelian varieties is a homomorphism whose underlying scheme morphism is finite and surjective. This definition works over an arbitrary field: it does not impose separability, so it includes inseparable isogenies in positive characteristic.

Rather than duplicate Mathlib's two scheme-morphism properties, AbelianVariety.isogenies K is their infimum pulled back along AbelianVariety.Hom.toSchemeFunctor. Consequently identities, composites, and morphisms isomorphic to isogenies are handled by Mathlib's generic MorphismProperty API. The abbreviation AbelianVariety.IsIsogeny f gives the usual predicate on a homomorphism.

Main results #

This is the property-level prerequisite for TauCetiRoadmap/JacobianChallenge/README.md, Layer E, item "[n] as an isogeny". The general theorem for nonzero n requires the later torsion theory and is not asserted here. No external formalization is vendored. The definition and closure proofs reuse Mathlib's AlgebraicGeometry.IsFinite and AlgebraicGeometry.Surjective morphism properties, including their stability under composition, isomorphism, and base change.

source
def TauCeti.AlgebraicGeometry.AbelianVariety.isogenies (K : Type u) [Field K] :
CategoryTheory.MorphismProperty (AbelianVariety K)

The morphism property of being an isogeny of abelian varieties over K: the underlying scheme morphism is finite and surjective.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.AlgebraicGeometry.AbelianVariety.IsIsogeny {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
    Prop

    A homomorphism of abelian varieties is an isogeny if its underlying scheme morphism is finite and surjective.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isIsogeny_iff {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) :
      IsIsogeny f ↔ AlgebraicGeometry.IsFinite (Hom.toSchemeHom f) ∧ AlgebraicGeometry.Surjective (Hom.toSchemeHom f)

      A homomorphism is an isogeny exactly when its underlying scheme morphism is finite and surjective.

      source
      instance TauCeti.AlgebraicGeometry.AbelianVariety.instIsMultiplicativeIsogenies {K : Type u} [Field K] :
      (isogenies K).IsMultiplicative

      Isogenies contain identities and are stable under composition.

      source
      instance TauCeti.AlgebraicGeometry.AbelianVariety.instRespectsIsoIsogenies {K : Type u} [Field K] :
      (isogenies K).RespectsIso

      Being an isogeny is invariant under isomorphisms of arrows.

      source
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isIsogeny_id {K : Type u} [Field K] (A : AbelianVariety K) :
      IsIsogeny (CategoryTheory.CategoryStruct.id A)

      The identity homomorphism is an isogeny.

      source
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isIsogeny_of_isIso {K : Type u} [Field K] {A B : AbelianVariety K} (f : A ⟶ B) [CategoryTheory.IsIso f] :
      IsIsogeny f

      Every isomorphism of abelian varieties is an isogeny.

      source
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsIsogeny.isFinite {K : Type u} [Field K] {A B : AbelianVariety K} {f : A ⟶ B} (hf : IsIsogeny f) :
      AlgebraicGeometry.IsFinite (Hom.toSchemeHom f)

      The underlying scheme morphism of an isogeny is finite.

      source
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsIsogeny.surjective {K : Type u} [Field K] {A B : AbelianVariety K} {f : A ⟶ B} (hf : IsIsogeny f) :
      AlgebraicGeometry.Surjective (Hom.toSchemeHom f)

      The underlying scheme morphism of an isogeny is surjective.

      source
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsIsogeny.comp {K : Type u} [Field K] {A B C : AbelianVariety K} {f : A ⟶ B} {g : B ⟶ C} (hf : IsIsogeny f) (hg : IsIsogeny g) :
      IsIsogeny (CategoryTheory.CategoryStruct.comp f g)

      A composite of isogenies is an isogeny.

      source
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.IsIsogeny.baseChange {K : Type u} [Field K] {A B : AbelianVariety K} {f : A ⟶ B} (hf : IsIsogeny f) (L : Type u) [Field L] [Algebra K L] :
      IsIsogeny (Hom.baseChange f L)

      Extending the ground field preserves isogenies.

      A multiplication isogeny #

      source
      theorem TauCeti.AlgebraicGeometry.AbelianVariety.isIsogeny_mulBy_neg_one {K : Type u} [Field K] (A : AbelianVariety K) :
      IsIsogeny (A.mulBy (-1))

      Multiplication by negative one is an isogeny.