JacobianVarieties.Albanese.exists_albanese_isIso_of_finrank_H1_eq_one
A pointed smooth proper integral genus-one curve, with genus measured by actual coherent cohomology, has an actual Albanese isomorphism, and every pointed morphism to an abelian variety factors uniquely as a homomorphism.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve NeronModelInfra
open GoodReductionJacobian AlgebraicGeometry.RelPicard
namespace JacobianVarieties.AlbaneseLean source · statement
theorem exists_albanese_isIso_of_finrank_H1_eq_one
{K : Type} [Field K] [IsAlgClosed K] [CharZero K]
(X : Scheme) [IsIntegral X] (c : X ⟶ Spec (.of K))
[IsProper c] [SmoothOfRelativeDimension 1 c] (V : X.TwoAffineOpenCover)
(hg : Module.finrank K (V.structureSheafSections c).H1 = 1)
(ε : SchemeHomOver (𝟙 (Spec (.of K))) c) :
∃ (A : Scheme) (f : A ⟶ Spec (.of K)) (G : RelativeGroupLaw K f),
G.IsCommutative ∧ ∃ aj : SchemeHomOver c f,
Smooth f ∧ IsProper f ∧ GeometricallyConnected f ∧ IsIso aj.1 ∧
ε.1 ≫ aj.1 = (G.one (𝟙 (Spec (.of K)))).1 ∧
∀ (B : Scheme) (b : B ⟶ Spec (.of K)) (H : RelativeGroupLaw K b),
AbelianSchemePropertyBundle K b →
∀ (q : SchemeHomOver c b),
NeronModelInfra.schemeHomOverComp ε q = H.one (𝟙 (Spec (.of K))) →
∃! φ : SchemeHomOver f b,
aj.1 ≫ φ.1 = q.1 ∧
∀ {T : Scheme} (t : T ⟶ Spec (.of K)) (x y : SchemeHomOver t f),
NeronModelInfra.schemeHomOverComp (G.mul t x y) φ =
H.mul t (NeronModelInfra.schemeHomOverComp x φ)
(NeronModelInfra.schemeHomOverComp y φ)