JacobianVarieties.Picard.conorm_algPoints_of_point_formulas
The Picard point comparisons supplied by the Abel--Jacobi construction intertwine actual conorm with extension of coefficients on algebraic points.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicCurve
open NeronModelInfra GoodReductionJacobian AlgebraicGeometry.SmoothProperCurve
open AlgebraicCurve.CurveModel
open JacobianVarieties.Pic0.Proofs.ConormInjectivity.AlgebraicCurve.ConDesc
namespace JacobianVarieties.Picard
attribute [local instance] IsCurveOver.toHasPrincipalDivisorsLean source · statement
theorem conorm_algPoints_of_point_formulas
{K F K' F' : Type} [Field K] [Field F] [Field K'] [Field F']
[Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
[IsScalarTower K K' F'] [IsScalarTower K F F']
[IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
(hfg : ∃ x : F, Transcendental K x ∧
FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
(hfg' : ∃ x : F', Transcendental K' x ∧
FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
(hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
(M₀ : CurveModel K F) (M : CurveModel K' F')
(eC : M.C ≅ pullback M₀.toBase (specMap K K'))
(heC : eC.hom ≫ pullback.snd M₀.toBase (specMap K K') = M.toBase)
(hsq : ∀ (U : M₀.C.Opens) [Nonempty (Scheme.Opens.toScheme U)]
[Nonempty (Scheme.Opens.toScheme
((eC.hom ≫ pullback.fst M₀.toBase (specMap K K')) ⁻¹ᵁ U))]
(s : Γ(M₀.C, U)),
M.ffEquiv.symm (M.C.germToFunctionField
((eC.hom ≫ pullback.fst M₀.toBase (specMap K K')) ⁻¹ᵁ U)
(((eC.hom ≫ pullback.fst M₀.toBase (specMap K K')).app U).hom s)) =
algebraMap F F' (M₀.ffEquiv.symm (M₀.C.germToFunctionField U s)))
(ε : SchemeHomOver (𝟙 (Spec (.of K))) M₀.toBase)
{J : Scheme} {b : J ⟶ Spec (.of K)}
(G : RelativeGroupLaw K b) (hc : G.IsCommutative)
(aj : SchemeHomOver M₀.toBase b)
(e₀ : Pic0 K F ≃+ G.AlgPoints hc K)
(e : Pic0 K' F' ≃+ G.AlgPoints hc K')
(hpoint₀ : ∀ x : SchemeHomOver (𝟙 (Spec (.of K))) M₀.toBase,
∃ D : Divisor.degZero (K := K) (F := F),
(D : Divisor K F) = Finsupp.single (M₀.pointEquivPlace x) 1 -
Finsupp.single (M₀.pointEquivPlace ε) 1 ∧
(RelativeGroupLaw.AlgPoints.toPoint (e₀ (Pic0.mk D))).1 = x.1 ≫ aj.1)
(hpoint : ∀ x s : SchemeHomOver (𝟙 (Spec (.of K'))) M.toBase,
s.1 ≫ eC.hom ≫ pullback.fst M₀.toBase (specMap K K') = specMap K K' ≫ ε.1 →
∃ D : Divisor.degZero (K := K') (F := F'),
(D : Divisor K' F') = Finsupp.single (M.pointEquivPlace x) 1 -
Finsupp.single (M.pointEquivPlace s) 1 ∧
(RelativeGroupLaw.AlgPoints.toPoint (e (Pic0.mk D))).1 =
x.1 ≫ eC.hom ≫ pullback.fst M₀.toBase (specMap K K') ≫ aj.1)
(z : Pic0 K F) :
e (conPic0 hfg hfg' hgen z) =
RelativeGroupLaw.AlgPoints.map (Algebra.ofId K K') (e₀ z)