AlgebraicCurve.degree_canonicalDivisor_eq_of_isAlgClosed
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Degree_canonicalDivisor_eq_of_isAlgClosed
attribute [-instance]
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
instIsScalarTowerResidueFieldRestrictPushforward
instAlgebraResidueFieldRestrictPushforward
instIsLocalHomRestrictInclusion
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal
kw_ffgc_finiteDimensional_adicCompletion
kw_ffgc_isScalarTower_integersIntegersCompletion
ModularCurve.KwF4gRRTate.instAlgebraKAdicCompletionIntegers
kw_ffgc_continuousSMul_adicCompletionComap
kw_ffgc_isScalarTower_integersCompletionCompletion
AlgebraicCurve.instHasCanonicalLocalResidueK
instAlgebra_restrictResidueField
instIsScalarTower_restrictResidueField
AlgebraicCurve.instHasLocalResidue
AlgebraicCurve.HasSeparableResidue.of_perfectField_of_isCurveOver
AlgebraicCurve.HasSeparableResidue.of_perfectField
instIsLocalHom_restrictSubringHom
AlgebraicCurve.instHasCanonicalLocalResidueKStar
ModularCurve.KwNo6Pin.isLocalRing_completion
AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupPic0
AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupDivisor
AlgebraicCurve.Pic0.instModuleZModTorsion
AlgebraicCurve.SemilinearAut.instSMulSubtypeProdRingAutMemSubgroupPlace
AlgebraicCurve.SemilinearAut.instDistribMulActionTorsion
AlgebraicCurve.SemilinearAut.instSMulSubtypeProdRingAutMemSubgroupPic0
AlgebraicCurve.SemilinearAut.instSMulTorsion
AlgebraicCurve.SemilinearAut.instMulActionSubtypeProdRingAutMemSubgroupPlace
AlgebraicCurve.SemilinearAut.instSMulCommClassZModTorsion
AlgebraicCurve.SemilinearAut.instMulSemiringActionSubtypeProdRingAutMemSubgroup
attribute [-simp] 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.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.Place.kw_ffgc_adicCompletionComapIntegers_coe
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.sizeOf_spec
AlgebraicCurve.Place.mem_simplePoleSubmodule AlgebraicCurve.Place.coe_uniformizerSubring
ModularCurve.Lg37.Lg37CompletionSection.mk.injEq
AlgebraicCurve.Place.CoefficientFieldSection.mk.injEq
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.injEq
ModularCurve.Lg37.Lg37CompletionSection.mk.sizeOf_spec
AlgebraicCurve.Place.CoefficientFieldSection.mk.sizeOf_spec
AlgebraicCurve.Place.poleSubmodule_one AlgebraicCurve.Place.mem_poleSubmodule
AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.Divisor.degree_pushforwardAlong
AlgebraicCurve.Pic0.coe_degZeroCorrespondence AlgebraicCurve.Place.mem_fiberAlong
AlgebraicCurve.SemilinearAut.toRingAut_inv AlgebraicCurve.SemilinearAut.smul_def
AlgebraicCurve.SemilinearAut.smul_single AlgebraicCurve.SemilinearAut.smul_toValuationSubring
AlgebraicCurve.SemilinearAut.baseAut_inv AlgebraicCurve.SemilinearAut.baseAut_ofAlgAut
AlgebraicCurve.SemilinearAut.toRingAut_ofAlgAut AlgebraicCurve.SemilinearAut.toRingAut_one
AlgebraicCurve.SemilinearAut.deg_smul AlgebraicCurve.SemilinearAut.degree_smul
AlgebraicCurve.SemilinearAut.coe_degZeroSMulHom AlgebraicCurve.SemilinearAut.baseAut_mul
AlgebraicCurve.SemilinearAut.coe_smulValuationSubringEquiv_apply
AlgebraicCurve.SemilinearAut.baseAut_one AlgebraicCurve.SemilinearAut.ofAlgAut_smul
AlgebraicCurve.SemilinearAut.coe_torsion_smul AlgebraicCurve.SemilinearAut.toRingAut_mulLean source · statement
theorem _root_.AlgebraicCurve.degree_canonicalDivisor_eq_of_isAlgClosed
{K F : Type*} [Field K] [IsAlgClosed K]
[Field F] [Algebra K F]
[AlgebraicCurve.HasCanonicalDivisor (K := K) (F := F)]
[∀ w : AlgebraicCurve.Place K F, w.DCoordGenerates]
[Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
[Algebra.IsIntegral (RatFunc K) F]
[AlgebraicCurve.HasLocalResidue K F]
[∀ w : AlgebraicCurve.Place K F, w.FiniteResidue]
[Nontrivial Ω[F⁄K]]
[AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.IsCurveOver K (RatFunc K)]
[∀ u : AlgebraicCurve.Place K (RatFunc K), u.FiniteResidue]
[AlgebraicCurve.HasCanonicalLocalResidueKStar K F]
[Algebra.IsSeparable (RatFunc K) F]
[Nontrivial Ω[(RatFunc K)⁄K]] [∀ v : AlgebraicCurve.Place K (RatFunc K), v.DCoordGenerates]
[FiniteDimensional (RatFunc K) F] [AlgebraicCurve.HasSeparableResidue K F]
{ω : Ω[F⁄K]} (hω : ω ≠ 0) :
AlgebraicCurve.Divisor.degree (AlgebraicCurve.canonicalDivisorOf hω) = 2 *
(AlgebraicCurve.genus K F : ℤ) - 2