theorem
L28 ↗correspondence_single
AlgebraicCurve.Divisor.correspondence_single
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_correspondence_single
open AlgebraicCurve AlgebraicCurve.SemilinearAut
open scoped Pointwise
noncomputable sectionLean source · statement
theorem _root_.AlgebraicCurve.Divisor.correspondence_single {K F F' : Type*} [Field K] [Field F]
[Field F'] [Algebra K F] [Algebra K F'] [HasPrincipalDivisors K F'] (φ ψ : F →ₐ[K] F') (hφ :
φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral) (v : Place K F) (n : ℤ) :
Divisor.correspondence φ ψ hφ hψ (Finsupp.single v n) = ∑ w ∈ Place.fiberAlong φ hφ v,
Finsupp.single (w.restrictAlong ψ hψ) (n * (w.ramificationIndexAlong φ : ℤ) * (w.inertiaDegAlong
ψ hψ : ℤ))