AlgebraicCurve.CartierB.finite_and_card_torsion_le_pow_genusFF
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Cartier.Proofs
namespace CartierB_finite_and_card_torsion_le_pow_genusFF
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
instIsScalarTowerResidueFieldRestrictPushforward
instAlgebraResidueFieldRestrictPushforward
instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
AlgebraicCurve.Place.differentialCoeff_dCoord AlgebraicCurve.KwCfx.kw_cfx_tau_coe
AlgebraicCurve.kw_hwcd_dlog_zero AlgebraicCurve.kw_hwcd_mem_regularDifferentials_iff
AlgebraicCurve.kw_hwcd_dlog_one AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
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
universe u vLean source · statement
theorem _root_.AlgebraicCurve.CartierB.finite_and_card_torsion_le_pow_genusFF
{K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
[AlgebraicCurve.IsCurveOver K F] (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectField K]
[FiniteDimensional K (AlgebraicCurve.regularDiffs K F)]
(x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
(hg : Module.finrank K (AlgebraicCurve.regularDiffs K F) = AlgebraicCurve.genusFF K F) :
Finite (AlgebraicCurve.Pic0.torsion K F p) ∧
Nat.card (AlgebraicCurve.Pic0.torsion K F p) ≤ p ^ AlgebraicCurve.genusFF K F