AlgebraicCurve.Divisor.correspondence_single_eq_finrankAlong_smul
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_correspondence_single_eq_finrankAlong_smul
open AlgebraicCurve AlgebraicCurve.SemilinearAut
open scoped Pointwise
noncomputable sectionLean source · statement
theorem _root_.AlgebraicCurve.Divisor.correspondence_single_eq_finrankAlong_smul {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) (hfin : FiniteAlong K φ)
(hsep : SeparableAlong K φ) (v : Place K F) (hcoll : ∀ w ∈ Place.fiberAlong φ hφ v,
w.restrictAlong ψ hψ = v) (hfψ : ∀ w ∈ Place.fiberAlong φ hφ v, w.inertiaDegAlong ψ hψ = 1) (hfφ
: ∀ w ∈ Place.fiberAlong φ hφ v, w.inertiaDegAlong φ hφ = 1) (n : ℤ) : Divisor.correspondence φ ψ
hφ hψ (Finsupp.single v n) = (finrankAlong K φ : ℤ) • Finsupp.single v n