AlgebraicCurve.RationalFunctionField.trace_localResidue_finitePlace_add_trace_localResidue_placeInfty_eq_zero
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
open _root_.AlgebraicCurves.Differentials.Residues.Proofs
open ResidueTheoremK_ratFunc_of_isAlgClosed.AlgebraicCurve (
dX)
open ResidueTheoremK_ratFunc_of_isAlgClosed.AlgebraicCurve (
ordDifferentialWellDefined_ratFunc_of_perfectField)
open ResidueTheoremK_ratFunc_of_isAlgClosed.AlgebraicCurve (
p0n21_rtk_kaehlerResidueTermKFam_atom_mOne_two_place_sum)
open ResidueTheoremK_ratFunc_of_isAlgClosed.AlgebraicCurve (
p1PrincipalPartAtom)
namespace AlgebraicCurve.RationalFunctionField
open _root_.PolynomialLean source · statement
theorem trace_localResidue_finitePlace_add_trace_localResidue_placeInfty_eq_zero
(K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
[AlgebraicCurve.HasCanonicalLocalResidueKStar K (RatFunc K)]
[∀ v : AlgebraicCurve.Place K (RatFunc K), v.DCoordGenerates]
[Nontrivial Ω[(RatFunc K)⁄K]]
{p c : K[X]} (hmon : p.Monic) (hp : Irreducible p) (hc : c.degree < p.degree) :
Algebra.trace K (AlgebraicCurve.RationalFunctionField.finitePlace K hp).ResidueField
((AlgebraicCurve.RationalFunctionField.finitePlace K hp).localResidue
(algebraMap K[X] (RatFunc K) c / algebraMap K[X] (RatFunc K) p
* (AlgebraicCurve.RationalFunctionField.finitePlace K hp).differentialCoeff
(KaehlerDifferential.D K (RatFunc K) (RatFunc.X : RatFunc K))))
+ Algebra.trace K (AlgebraicCurve.RationalFunctionField.placeInfty K).ResidueField
((AlgebraicCurve.RationalFunctionField.placeInfty K).localResidue
(algebraMap K[X] (RatFunc K) c / algebraMap K[X] (RatFunc K) p
* (AlgebraicCurve.RationalFunctionField.placeInfty K).differentialCoeff
(KaehlerDifferential.D K (RatFunc K) (RatFunc.X : RatFunc K)))) = 0