Module

ResidueTheoremK_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheoremK_of_isAlgClosed

4 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

The rational-function-field residue theorem and fibre trace identities give the residue theorem over algebraically closed base fields.

Imports5

Imported by6

theorem

subsingleton_canonicalLocalResidueDataK_of_surj

L37 ↗

AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheoremK_of_isAlgClosed.AlgebraicCurve.subsingleton_canonicalLocalResidueDataK_of_surj

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheoremK_of_isAlgClosed
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve

Lean source · statement

theorem subsingleton_canonicalLocalResidueDataK_of_surj
    {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
    (hsurj : Function.Surjective (algebraMap K v.ResidueField)) :
    Subsingleton v.CanonicalLocalResidueDataK

theorem

subsingleton_canonicalLocalResidueDataK_of_isAlgClosed

L52 ↗

AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheoremK_of_isAlgClosed.AlgebraicCurve.subsingleton_canonicalLocalResidueDataK_of_isAlgClosed

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheoremK_of_isAlgClosed
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve

Lean source · statement

theorem subsingleton_canonicalLocalResidueDataK_of_isAlgClosed
    {K F : Type*} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
    (v : Place K F) [v.FiniteResidue] :
    Subsingleton v.CanonicalLocalResidueDataK

theorem

residueTheoremK_of_residueTheorem_isAlgClosed

L63 ↗

AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheoremK_of_isAlgClosed.AlgebraicCurve.residueTheoremK_of_residueTheorem_isAlgClosed

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheoremK_of_isAlgClosed
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve

Lean source · statement

theorem residueTheoremK_of_residueTheorem_isAlgClosed
    {K F : Type*} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
    [HasCanonicalLocalResidueKStar K F] [∀ v : Place K F, v.FiniteResidue]
    [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    (hRT : ∀ [HasPrincipalDivisors K F], ResidueTheorem K F) : ResidueTheoremK K F

theorem