Module

FibreIdentity.lean

Nyll.AlgebraicCurves.Differentials.Residues.FibreIdentity

1 declaration indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

The compatibility of residue sums over a place fibre with differential pullback and field trace.

Imports3

Imported by6

def

FibreResidueIdentityAlong

L34 ↗

AlgebraicCurve.FibreResidueIdentityAlong

Documentation

For each base place, the sum of pulled-back differential residues over its fibre equals the residue of the traced function.

Source context 4 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

def FibreResidueIdentityAlong [HasPrincipalDivisors K F']
    [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) : Prop

Module documentation

Differentials, residues, and divisor correspondences

Declarations

FibreResidueIdentityAlong