AlgebraicCurve.eq_genusFF_of_forall_ell_sub_ell_eq
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Eq_genusFF_of_forall_ell_sub_ell_eq
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
AlgebraicCurve.Place.instIsPrimeCenter AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] 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.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
universe u v
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.eq_genusFF_of_forall_ell_sub_ell_eq
{K : Type u} {F : Type v} [Field K] [PerfectField K] [Field F] [Algebra K F]
[Algebra.EssFiniteType K F] [IsCurveOver K F] (hC : ConstantsAreBase K F)
{Kc : Divisor K F} {g : ℕ}
(hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g) :
g = genusFF K F