Nyll.JacobianVarieties.Albanese.AbelJacobiHomDetection

Module documentation

Abel–Jacobi maps detect group homomorphisms

For a pointed smooth proper geometrically integral curve model over an algebraically closed field, choose the actual group law and Abel–Jacobi morphism supplied by the Picard representation. Two morphisms from that representation into a separated group scheme are equal if they preserve multiplication and agree after Abel–Jacobi.

The proof uses the proved generation of Pic0 by point differences, the actual Picard-to-points equivalence, and density of geometric points on a reduced scheme. This proves uniqueness of a possible Albanese factorization. Existence of that factorization, and descent of arbitrary-target sums, are separate assertions.

theorem

exists_abelJacobi_detects_hom_of_curveModel

L47 ↗

AlgebraicGeometry.RelPicard.exists_abelJacobi_detects_hom_of_curveModel

Documentation

The actual Abel–Jacobi morphism detects multiplicative morphisms out of the Picard representation. No properness or commutativity is required of the target group.

Source context 8 commands

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

noncomputable section
universe u v
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
open AlgebraicCurves.Geometry.Schemes.Proofs
open SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
open RigKerGeomPoints renaming ext_of_forall_geometric_point → geometricHomExt in

Lean source · statement

theorem exists_abelJacobi_detects_hom_of_curveModel
    {K : Type u} [Field K] [IsAlgClosed K]
    {F : Type v} [Field F] [Algebra K F] [IsCurveOver K F]
    (M : CurveModel K F) [GeometricallyIntegral M.toBase]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase)
    (D : RelativePic0Designation K M.toBase)
    (hD : RepresentsRelSubPic M.toBase ε (algEquivZeroCut M.toBase ε) D)
    (hsm : Smooth D.toBase) (hpr : IsProper D.toBase)
    (hgc : GeometricallyConnected D.toBase) :
    ∃ (L : RelativeGroupLaw K D.toBase) (aj : SchemeHomOver M.toBase D.toBase),
      AbelianSchemePropertyBundle K D.toBase ∧
      (L.one (𝟙 (Spec (CommRingCat.of K)))).1 = D.zeroSection ∧
      ε.1 ≫ aj.1 = D.zeroSection ∧
      ∀ (B : Scheme.{u}) (b : B ⟶ Spec (CommRingCat.of K)), IsSeparated b →
        ∀ (G : RelativeGroupLaw K b) (φ ψ : SchemeHomOver D.toBase b),
          (∀ x y : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) D.toBase,
            NeronModelInfra.schemeHomOverComp (L.mul _ x y) φ =
              G.mul _ (NeronModelInfra.schemeHomOverComp x φ)
                (NeronModelInfra.schemeHomOverComp y φ)) →
          (∀ x y : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) D.toBase,
            NeronModelInfra.schemeHomOverComp (L.mul _ x y) ψ =
              G.mul _ (NeronModelInfra.schemeHomOverComp x ψ)
                (NeronModelInfra.schemeHomOverComp y ψ)) →
          aj.1 ≫ φ.1 = aj.1 ≫ ψ.1 → φ = ψ

Module documentation

Abel–Jacobi maps detect group homomorphisms

Declarations

exists_abelJacobi_detects_hom_of_curveModel