noncomputable def closedPointDegree (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [Algebra k R] (p : Ideal R) : ℕ

The degree $[\kappa(\mathfrak{p}) : k]$ of a closed point $\mathfrak{p} \subseteq R$ over the base field $k$, defined as the dimension of the residue field $R/\mathfrak{p}$ as a $k$-vector space.

noncomputable def pullbackDivisorDegree (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [IsDedekindDomain R] [Algebra k R] (S : Type u_3) [CommRing S] [IsDedekindDomain S] [Algebra R S] [Algebra k S] (p : Ideal R) : ℕ

The degree of the pullback divisor of a prime $\mathfrak{p}$ under the inclusion $R \hookrightarrow S$: the weighted sum $\sum_{\mathfrak{P} \mid \mathfrak{p}} e(\mathfrak{P}/\mathfrak{p}) \cdot \deg(\mathfrak{P})$ over primes of $S$ lying above $\mathfrak{p}$.

theorem degree_pullback_eq_mul_degree (k : Type u_1) [Field k] (R : Type u_2) [CommRing R] [IsDedekindDomain R] [Algebra k R] (S : Type u_3) [CommRing S] [IsDedekindDomain S] [Algebra R S] [Algebra k S] [IsScalarTower k R S] [Module.IsTorsionFree R S] (K : Type u_4) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_5) [Field L] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] (p : Ideal R) [p.IsMaximal] (hp0 : p ≠ ⊥) : pullbackDivisorDegree k R S p = Module.finrank K L * closedPointDegree k R p

The degree of the pullback of a point under a finite morphism of Dedekind domains equals $[L:K] \cdot \deg(\mathfrak{p})$, where $K, L$ are the fraction fields: $\sum_{\mathfrak{P} \mid \mathfrak{p}} e(\mathfrak{P}/\mathfrak{p}) f(\mathfrak{P}/\mathfrak{p}) = [L:K]$.