Nyll.JacobianVarieties.Albanese.AbelJacobiMorphismDetectionField

Module documentation

Uniqueness of pointed Abel–Jacobi factorizations over any field

The actual Picard representation supplies an Abel–Jacobi map for which a pointed map into an abelian variety has at most one factorization among all scheme morphisms. Each candidate preserves the identity because its restriction to the curve is pointed. Rigidity then proves multiplication preservation on every test scheme, so Abel–Jacobi homomorphism detection applies over an algebraic closure.

The group law and Abel–Jacobi map are the same witnesses supplied by the existing arbitrary-field construction. No characteristic or genus restriction is imposed. This theorem proves uniqueness; existence of a factorization is a separate claim.

theorem

exists_abelJacobi_detects_pointed_factorizations_of_field

L47 ↗

AlgebraicGeometry.RelPicard.exists_abelJacobi_detects_pointed_factorizations_of_field

Documentation

The constructed Abel–Jacobi map admits at most one scheme-morphism factorization of any pointed map to an abelian variety, over any field.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra GoodReductionJacobian
open CategoryTheory.MonoidalCategory
namespace AlgebraicGeometry.RelPicard

Lean source · statement

theorem exists_abelJacobi_detects_pointed_factorizations_of_field
    (K : Type u) [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    (D : RelativePic0Designation K c)
    (hD : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (hsm : Smooth D.toBase) (hpr : IsProper D.toBase)
    (hgc : GeometricallyConnected D.toBase) :
    ∃ (L : RelativeGroupLaw K D.toBase) (aj : SchemeHomOver c D.toBase),
      AbelianSchemePropertyBundle K D.toBase ∧
      (L.one (𝟙 (Spec (CommRingCat.of K)))).1 = D.zeroSection ∧
      ε.1 ≫ aj.1 = D.zeroSection ∧
      (∀ (k : Type u) [Field k] (t : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of K))
          (x : SchemeHomOver t c),
        Nonempty ((hD.poincare.pullbackAlong
            ⟨x.1 ≫ aj.1, (Category.assoc _ _ _).trans ((congrArg (x.1 ≫ ·) aj.2).trans x.2)⟩).L ≅
          (RelEffCartierDiv.ofPoint c x.1 x.2).lineBundle ⊗
            (RelEffCartierDiv.ofPoint c (t ≫ ε.1)
              ((Category.assoc _ _ _).trans
                  ((congrArg (t ≫ ·) ε.2).trans (Category.comp_id t)))).idealModule)) ∧
      ∀ (B : Scheme.{u}) (b : B ⟶ Spec (CommRingCat.of K))
        (G : RelativeGroupLaw K b), AbelianSchemePropertyBundle K b →
        ∀ (q : SchemeHomOver c b),
          NeronModelInfra.schemeHomOverComp ε q =
            G.one (𝟙 (Spec (CommRingCat.of K))) →
          ∀ (φ ψ : SchemeHomOver D.toBase b),
            aj.1 ≫ φ.1 = q.1 → aj.1 ≫ ψ.1 = q.1 → φ = ψ

Module documentation

Uniqueness of pointed Abel–Jacobi factorizations over any field

Declarations

exists_abelJacobi_detects_pointed_factorizations_of_field