Module

UnpointedAlbanese.lean

Nyll.JacobianVarieties.Picard.UnpointedAlbanese

1 declaration indexed from sourceView source ↗

Module documentation

The actual Albanese factorization for the fixed, unpointed Jacobian.

Imports10

Imported by2

theorem

exists_unique_abelJacobi_factorization

L30 ↗

JacobianVarieties.Picard.Unpointed.exists_unique_abelJacobi_factorization

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Picard.Unpointed

Lean source · statement

theorem exists_unique_abelJacobi_factorization
    {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)
    {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 (𝟙 _)) :
    ∃! φ : SchemeHomOver (toBase K c) b, (abelJacobi c ε).1 ≫ φ.1 = q.1

Module documentation

Declarations

exists_unique_abelJacobi_factorization