AlgebraicGeometry.RelPicard.HasChartSections.forall_geometricFibre_riemannRoch_imp_eq
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.HasChartSections_forall_geometricFibre_riemannRoch_imp_eq
attribute [-instance]
AlgebraicCurve.IsCurveOver.instNontrivialKaehler
AlgebraicCurve.IsCurveOver.instFreeKaehler
AlgebraicCurve.IsCurveOver.toHasPrincipalDivisors
AlgebraicCurve.IsCurveOver.instFiniteResidue
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
AlgebraicCurve.Place.instIsPrimeCenter
AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp]
AlgebraicCurve.Divisor.evalFun_zero
AlgebraicCurve.Place.evalAt_one
AlgebraicCurve.Divisor.mapRestrict_single
AlgebraicCurve.Divisor.pushforward_single
AlgebraicCurve.Place.coe_restrictInclusion
AlgebraicCurve.Place.mem_fiber
AlgebraicCurve.Place.restrict_toValuationSubring
AlgebraicCurve.Divisor.degree_pushforward
AlgebraicCurve.Place.restrictResidueMap_residue
AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
AlgebraicCurve.Place.differentialCoeff_zero
AlgebraicCurve.Place.differentialCoeff_dCoord
AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
AlgebraicCurve.IntegralBasisInLSpace.mk.injEq
AlgebraicCurve.TranscendenceTower.mk.injEq
AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec
AlgebraicCurve.PoleDivisorPackage.mk.injEq
attribute [-simp]
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfra AlgebraicCurveLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.HasChartSections.forall_geometricFibre_riemannRoch_imp_eq
{R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
{n g r : ℕ} {γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
(hγ : HasChartSections c γ) :
∀ (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
(L : Type u) [Field L] [Algebra k L] (M : CurveModel k L) (e : M.C ≅ pullback c s)
(_ : e.hom ≫ pullback.snd c s = M.toBase) (Kc : Divisor k L) (g' : ℕ),
(∀ D : Divisor k L, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g') → g' = g