NYLL
Module

UnpointedAbelJacobi.lean

Nyll.JacobianVarieties.Picard.UnpointedAbelJacobi
10 declarations indexed from sourceView source ↗

Module documentation

Abel–Jacobi maps into one unpointed Jacobian

Every basepoint gives an actual point-minus-basepoint classifying morphism into the same Jacobian constructed without a rational point. The fixed comparison of Picard representations transports both the morphism and its identity formula.

Imports7
Imported by3

Declarations

instance

curveIntegral

L37 ↗
JacobianVarieties.Picard.Unpointed.curveIntegral
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
Lean source · statement
instance curveIntegral : GeometricallyIntegral c
structure

PointedAbelJacobiData

L43 ↗
JacobianVarieties.Picard.Unpointed.PointedAbelJacobiData
Documentation

All chosen pointed data are supplied by actual Picard existence and the proved point-minus-basepoint construction.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · full declaration
structure PointedAbelJacobiData where
  /-- The Picard scheme supplied by pointed representability. -/
  designation : RelativePic0Designation K c
  /-- Its classification of actual rigidified line bundles. -/
  representation : RepresentsRelSubPic c ε (algEquivZeroCut c ε) designation
  /-- The constructed point-minus-basepoint morphism. -/
  map : SchemeHomOver c designation.toBase
  /-- The original basepoint is carried to the Picard zero section. -/
  basepoint : ε.1 ≫ map.1 = designation.zeroSection
  /-- The actual Poincare class is the point-minus-basepoint line bundle. -/
  pointClass : ∀ (L : Type u) [Field L] (t : Spec (CommRingCat.of L) ⟶ Spec (CommRingCat.of K))
      (x : SchemeHomOver t c),
    Nonempty ((representation.poincare.pullbackAlong
        ⟨x.1 ≫ map.1, (Category.assoc _ _ _).trans ((congrArg (x.1 ≫ ·) map.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)
  /-- Rigidity and geometric point generation detect every pointed factorization
  through this same constructed morphism. -/
  factorization_unique : ∀ (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 designation.toBase b),
          map.1 ≫ φ.1 = q.1 → map.1 ≫ ψ.1 = q.1 → φ = ψ
theorem

nonempty_pointedAbelJacobiData

L70 ↗
JacobianVarieties.Picard.Unpointed.nonempty_pointedAbelJacobiData
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · statement
theorem nonempty_pointedAbelJacobiData : Nonempty (PointedAbelJacobiData c ε)
def

pointedAbelJacobiData

L77 ↗
JacobianVarieties.Picard.Unpointed.pointedAbelJacobiData
Documentation

One choice of the actual pointed construction for a specified basepoint.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · statement
def pointedAbelJacobiData : PointedAbelJacobiData c ε
def

abelJacobiComparison

L81 ↗
JacobianVarieties.Picard.Unpointed.abelJacobiComparison
Documentation

The comparison used to transport the actual pointed construction.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · statement
def abelJacobiComparison : Jacobian K c ≅ (pointedAbelJacobiData c ε).designation.P
def

abelJacobi

L86 ↗
JacobianVarieties.Picard.Unpointed.abelJacobi
Documentation

The actual Abel–Jacobi map into the Jacobian whose carrier is independent of the selected rational basepoint.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · statement
def abelJacobi : SchemeHomOver c (toBase K c)
theorem

abelJacobi_comp_comparison

L94 ↗
JacobianVarieties.Picard.Unpointed.abelJacobi_comp_comparison
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · statement
theorem abelJacobi_comp_comparison :
    (abelJacobi c ε).1 ≫ (abelJacobiComparison c ε).hom =
      (pointedAbelJacobiData c ε).map.1
theorem

abelJacobi_basepoint

L102 ↗
JacobianVarieties.Picard.Unpointed.abelJacobi_basepoint
Documentation

The selected basepoint maps to the identity of the same fixed group law.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · statement
theorem abelJacobi_basepoint :
    ε.1 ≫ (abelJacobi c ε).1 = ((groupLaw K c).one (𝟙 (Spec (CommRingCat.of K)))).1
theorem

abelJacobi_classifies_point_difference

L111 ↗
JacobianVarieties.Picard.Unpointed.abelJacobi_classifies_point_difference
Documentation

After the actual Picard comparison, every field-valued point classifies the line bundle of that point minus the chosen basepoint.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · full declaration
theorem abelJacobi_classifies_point_difference
    (L : Type u) [Field L] (t : Spec (CommRingCat.of L) ⟶ Spec (CommRingCat.of K))
    (x : SchemeHomOver t c) :
    let M := pointedAbelJacobiData c ε
    let z : SchemeHomOver t M.designation.toBase :=
      ⟨x.1 ≫ (abelJacobi c ε).1 ≫ (abelJacobiComparison c ε).hom, by
        rw [abelJacobi_comp_comparison, Category.assoc, M.map.2, x.2]⟩
    Nonempty ((M.representation.poincare.pullbackAlong z).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) := by
  intro M z
  have hz : z = ⟨x.1 ≫ M.map.1,
      (Category.assoc _ _ _).trans ((congrArg (x.1 ≫ ·) M.map.2).trans x.2)⟩ := by
    apply Subtype.ext
    exact congrArg (x.1 ≫ ·) (abelJacobi_comp_comparison c ε)
  rw [hz]
  exact M.pointClass L t x
theorem

abelJacobi_factorization_unique

L133 ↗
JacobianVarieties.Picard.Unpointed.abelJacobi_factorization_unique
Documentation

Every pointed map has at most one factorization through the actual selected Abel–Jacobi map into the fixed unpointed Jacobian.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
local instance curveIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c
Lean source · statement
theorem abelJacobi_factorization_unique
    {B : Scheme.{u}} (b : B ⟶ Spec (CommRingCat.of K))
    (G : RelativeGroupLaw K b) (hB : AbelianSchemePropertyBundle K b)
    (q : SchemeHomOver c b)
    (hq : NeronModelInfra.schemeHomOverComp ε q = G.one (𝟙 (Spec (CommRingCat.of K))))
    (φ ψ : SchemeHomOver (toBase K c) b)
    (hφ : (abelJacobi c ε).1 ≫ φ.1 = q.1)
    (hψ : (abelJacobi c ε).1 ≫ ψ.1 = q.1) : φ = ψ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.