AlgebraicCurve.residueTheorem_of_residueTheorem_ratFunc_of_residueTraceCompletionCommute
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace ResidueTheorem_of_residueTheorem_ratFunc_of_residueTraceCompletionCommute
noncomputable section
open _root_.AlgebraicCurve
open FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates.AlgebraicCurve
(exists_kaehlerPullback_ne_zero
residueTheorem_of_fiberKaehlerCotraceResidueIdentity
fiberKaehlerCotraceResidueIdentity_of_rtcc_cts)
inLean source · statement
theorem
_root_.AlgebraicCurve.residueTheorem_of_residueTheorem_ratFunc_of_residueTraceCompletionCommute
{K F : Type*} [Field K] [PerfectField K]
[Field F] [Algebra K F]
[HasCanonicalDivisor (K := K) (F := F)]
[∀ w : Place K F, w.DCoordGenerates]
[Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
[Algebra.IsIntegral (RatFunc K) F] [Module.Finite (RatFunc K) F]
[∀ w : Place K F, w.FiniteResidue]
[Nontrivial Ω[F⁄K]]
[IsCurveOver K F] [IsCurveOver K (RatFunc K)]
[∀ u : Place K (RatFunc K), u.FiniteResidue]
[Algebra.IsSeparable (RatFunc K) F]
[HasCanonicalDivisor (K := K) (F := RatFunc K)]
[Nontrivial Ω[(RatFunc K)⁄K]] [∀ v : Place K (RatFunc K), v.DCoordGenerates]
(hP1 : ResidueTheorem K (RatFunc K))
(hRTCC : ModularCurve.KwF4R1V391a.KwF4R1V391aResidueTraceCompletionCommute K F (RatFunc K)) :
ResidueTheorem K F