Module

AlbaneseFactorizationField.lean

Nyll.JacobianVarieties.Albanese.AlbaneseFactorizationField

3 declarations indexed from sourceView source ↗

Module documentation

Actual Abel--Jacobi factorization over an arbitrary field

The factorization over a finite separable extension is identified with the native scalar extension of one fixed Abel--Jacobi morphism. Faithfully flat descent then gives a factorization over the original field.

Imports17

Imported by2

theorem

pointed_baseChange

L42 ↗

JacobianVarieties.Albanese.pointed_baseChange

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Albanese

Lean source · statement

theorem pointed_baseChange
    {K L : Type u} [Field K] [Field L] [Algebra K L] {C B : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of K)} {b : B ⟶ Spec (CommRingCat.of K)}
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    (G : RelativeGroupLaw K b) (q : SchemeHomOver c b)
    (hq : NeronModelInfra.schemeHomOverComp ε q = G.one (𝟙 _)) :
    NeronModelInfra.schemeHomOverComp (sectionBaseChange L ε)
      (fibreRestrictAlong (specMap K L) b c q) =
      (G.baseChange (specMap K L)).one (𝟙 _)

theorem

exists_native_local_factorization

L68 ↗

JacobianVarieties.Albanese.exists_native_local_factorization

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Albanese

Lean source · statement

theorem exists_native_local_factorization
    (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) [Smooth D.toBase] [IsSeparated D.toBase]
    (hD : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (aj : SchemeHomOver c D.toBase)
    (hclass : ∀ (F : Type u) [Field F]
      (t : Spec (CommRingCat.of F) ⟶ 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)) [Smooth b] [IsProper b]
    [GeometricallyIntegral b] (G : RelativeGroupLaw K b) (q : SchemeHomOver c b)
    (hq : NeronModelInfra.schemeHomOverComp ε q = G.one (𝟙 _)) :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra K L) (_ : Module.Finite K L)
      (_ : Algebra.IsSeparable K L)
      (ψ : SchemeHomOver (D.baseChange L).toBase (pullback.snd b (specMap K L))),
      (fibreRestrictAlong (specMap K L) D.toBase c aj).1 ≫ ψ.1 =
        (fibreRestrictAlong (specMap K L) b c q).1

theorem

exists_abelJacobi_factorization_of_field

L124 ↗

JacobianVarieties.Albanese.exists_abelJacobi_factorization_of_field

Documentation

Over any field, one actual Abel--Jacobi morphism factors every pointed morphism to a smooth proper geometrically integral group scheme. The factorization is constructed over a finite separable extension by divisor sums and descended to the original field.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Albanese

Lean source · statement

theorem exists_abelJacobi_factorization_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) [LocallyOfFiniteType D.toBase]
    (hD : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) :
    ∃ aj : SchemeHomOver c D.toBase,
      ε.1 ≫ aj.1 = D.zeroSection ∧
      (∀ (F : Type u) [Field F] (t : Spec (CommRingCat.of F) ⟶ 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)) [Smooth b] [IsProper b]
        [GeometricallyIntegral b] (G : RelativeGroupLaw K b) (q : SchemeHomOver c b),
        NeronModelInfra.schemeHomOverComp ε q = G.one (𝟙 _) →
          ∃ ψ : SchemeHomOver D.toBase b, aj.1 ≫ ψ.1 = q.1

Module documentation

Actual Abel--Jacobi factorization over an arbitrary field

Declarations

pointed_baseChange

exists_native_local_factorization

exists_abelJacobi_factorization_of_field