AlgebraicCurve.Divisor.evalFun_mapDomain_of_comap
Divisor evaluation commutes with a field embedding and an injective map of places whose valuation rings have the prescribed comap.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace AlgebraicCurve.DivisorLean source · statement
theorem evalFun_mapDomain_of_comap
{K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F']
[Algebra K F] [Algebra K' F']
(τ : K →+* K') (φ : F →+* F')
(hφ : ∀ a : K, φ (algebraMap K F a) = algebraMap K' F' (τ a))
(ι : Place K F → Place K' F') (hι : Function.Injective ι)
(hcomap : ∀ v, (ι v).toValuationSubring.comap φ = v.toValuationSubring)
(D : Divisor K F) (f : F)
(hrat : ∀ v ∈ D.support, v.IsRational)
(hmem : ∀ v ∈ D.support, f ∈ v.toValuationSubring) :
evalFun (φ f) (Finsupp.mapDomain ι D) = τ (evalFun f D)