Documentation

TauCeti.AlgebraicGeometry.GroupScheme.Isogeny.FactorisationDual

The factorisation dual of an isogeny of commutative group schemes #

For a locally finitely presented isogeny f : A ⟶ B of commutative group schemes of constant degree n, its kernel is killed by n. Multiplication by n therefore factors uniquely through f, giving a homomorphism factorisationDual f hf : B ⟶ A. Both composites are multiplication by n, on their respective group schemes. The construction uses fpqc descent, so also applies in characteristics dividing the degree and over nonreduced bases.

Uniqueness of the factorisation gives the formal properties of the dual. It reverses composition, commutes with arbitrary base change, and is computed on multiplication maps. If multiplication by n on A is an isogeny of degree n * k and multiplication by n on B is finite, the dual is an isogeny of degree k. When the dual again has degree n, its own factorisation dual is f.

For elliptic curves, apply this API to A = E.toCommGrp and B = E'.toCommGrp; local finite presentation is automatic, and multiplication by n has degree n². This gives the factorisation construction before comparison with the Picard dual.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.GroupScheme.factorisationDual {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} (hf : IsogenyOfDegree f.hom n) :
B ⟶ A

The factorisation dual of a constant-degree isogeny, characterized by comp_factorisationDual. It is a homomorphism from B to A.

Instances For
    source
    @[simp]
    theorem TauCeti.GroupScheme.comp_factorisationDual {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} (hf : IsogenyOfDegree f.hom n) :
    CategoryTheory.CategoryStruct.comp f (factorisationDual f hf) = (↑n).asHom

    Composing f : A ⟶ B with its factorisation dual B ⟶ A is [n] on A.

    source
    @[simp]
    theorem TauCeti.GroupScheme.comp_factorisationDual_assoc {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} (hf : IsogenyOfDegree f.hom n) {Z : CategoryTheory.CommGrp (CategoryTheory.Over S)} (h : A ⟶ Z) :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (factorisationDual f hf) h) = CategoryTheory.CategoryStruct.comp (↑n).asHom h

    Composing f : A ⟶ B with its factorisation dual B ⟶ A is [n] on A.

    source
    theorem TauCeti.GroupScheme.eq_factorisationDual {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} (hf : IsogenyOfDegree f.hom n) (g : B ⟶ A) (hg : CategoryTheory.CategoryStruct.comp f g = (↑n).asHom) :
    g = factorisationDual f hf

    A homomorphism B ⟶ A whose composite with f is [n] equals the factorisation dual.

    source
    @[simp]
    theorem TauCeti.GroupScheme.factorisationDual_comp {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} (hf : IsogenyOfDegree f.hom n) :
    CategoryTheory.CategoryStruct.comp (factorisationDual f hf) f = (↑n).asHom

    Composing the factorisation dual B ⟶ A with f : A ⟶ B is [n] on B.

    source
    @[simp]
    theorem TauCeti.GroupScheme.factorisationDual_comp_assoc {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} (hf : IsogenyOfDegree f.hom n) {Z : CategoryTheory.CommGrp (CategoryTheory.Over S)} (h : B ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (factorisationDual f hf) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (↑n).asHom h

    Composing the factorisation dual B ⟶ A with f : A ⟶ B is [n] on B.

    Isogeny, degree and involutivity #

    source
    theorem TauCeti.GroupScheme.isogenyOfDegree_factorisationDual {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} (hf : IsogenyOfDegree f.hom n) {k : ℕ} (hA : IsogenyOfDegree (↑n).asHom.hom (n * k)) [AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left (↑n).asHom.hom.hom.hom)] :
    IsogenyOfDegree (factorisationDual f hf).hom k

    The factorisation dual is an isogeny. Let f : A ⟶ B be an isogeny of degree n. If multiplication by n on A is an isogeny of degree n * k and multiplication by n on B is finite, then the factorisation dual B ⟶ A is an isogeny of degree k. For elliptic curves, multiplication by n has degree n², so the dual of an isogeny of degree n again has degree n.

    source
    @[simp]
    theorem TauCeti.GroupScheme.factorisationDual_factorisationDual {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} (hf : IsogenyOfDegree f.hom n) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left (factorisationDual f hf).hom.hom.hom)] (hf' : IsogenyOfDegree (factorisationDual f hf).hom n) :
    factorisationDual (factorisationDual f hf) hf' = f

    The factorisation dual is involutive. If the factorisation dual of an isogeny f of degree n is again an isogeny of degree n, then its own factorisation dual is f.

    Composition and multiplication maps #

    source
    theorem TauCeti.GroupScheme.factorisationDual_comp_eq_comp {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} {C : CategoryTheory.CommGrp (CategoryTheory.Over S)} (g : B ⟶ C) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left g.hom.hom.hom)] [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp f g).hom.hom.hom)] {m : ℕ} (hf : IsogenyOfDegree f.hom m) (hg : IsogenyOfDegree g.hom n) (hfg : IsogenyOfDegree (CategoryTheory.CategoryStruct.comp f g).hom (m * n)) :
    factorisationDual (CategoryTheory.CategoryStruct.comp f g) hfg = CategoryTheory.CategoryStruct.comp (factorisationDual g hg) (factorisationDual f hf)

    The factorisation dual reverses composition. For isogenies f : A ⟶ B of degree m and g : B ⟶ C of degree n, the factorisation dual of f ≫ g : A ⟶ C, of degree m * n, is the composite C ⟶ B ⟶ A of the factorisation duals of g and of f.

    source
    theorem TauCeti.GroupScheme.factorisationDual_intCast {S : AlgebraicGeometry.Scheme} {A : CategoryTheory.CommGrp (CategoryTheory.Over S)} (m k : ℤ) {d : ℕ} [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left (↑m).asHom.hom.hom.hom)] (h : IsogenyOfDegree (↑m).asHom.hom d) (hd : ↑d = m * k) :
    factorisationDual (↑m).asHom h = (↑k).asHom

    The factorisation dual of a multiplication map. If multiplication by an integer m is an isogeny of degree d with d = m * k, then its factorisation dual is multiplication by k. For elliptic curves, multiplication by m ≠ 0 has degree m², so it is its own factorisation dual.

    Base change #

    source
    theorem TauCeti.GroupScheme.pullback_mapCommGrp_map_factorisationDual {S : AlgebraicGeometry.Scheme} {A B : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : A ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)] {n : ℕ} {T : AlgebraicGeometry.Scheme} (s : T ⟶ S) (hf : IsogenyOfDegree f.hom n) [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback s).mapCommGrp.map f).hom.hom.hom)] (hf' : IsogenyOfDegree ((CategoryTheory.Over.pullback s).mapCommGrp.map f).hom n) :
    (CategoryTheory.Over.pullback s).mapCommGrp.map (factorisationDual f hf) = factorisationDual ((CategoryTheory.Over.pullback s).mapCommGrp.map f) hf'

    The factorisation dual commutes with base change. For an isogeny f of degree n and a morphism s : T ⟶ S, the factorisation dual of the base change of f along s is the base change of the factorisation dual of f.