theorem DegreeFormula.sum_sub_ones {ι : Type u_1} (s : Finset ι) (f : ι → ℕ) (hf : ∀ x ∈ s, 1 ≤ f x) : ∑ x ∈ s, (f x - 1) = s.sum f - s.card

Arithmetic helper: for a finite sum of natural numbers all at least one, ∑ (f x - 1) = (∑ f x) - |s|.

theorem cor27_fundamental_identity {A : Type u_1} {B : Type u_2} (K : Type u_3) (L : Type u_4) [CommRing A] [CommRing B] [Field K] [Field L] [IsDomain A] [IsDomain B] [IsDedekindDomain A] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (𝔭 : Ideal A) [h𝔭p : 𝔭.IsPrime] (h𝔭 : 𝔭 ≠ ⊥) : ∑ 𝔔 ∈ primesOverFinset 𝔭 B, 𝔭.ramificationIdx 𝔔 * 𝔭.inertiaDeg 𝔔 = Module.finrank K L

Corollary 27 (fundamental identity ∑ e_i f_i = n): for a finite extension B/A of Dedekind domains with fraction fields L/K and a nonzero prime 𝔭 ⊂ A, ∑_{𝔔 ∣ 𝔭} e(𝔔/𝔭) · f(𝔔/𝔭) = [L : K].

theorem cor27_ramification_formula {A : Type u_1} {B : Type u_2} (K : Type u_3) (L : Type u_4) [CommRing A] [CommRing B] [Field K] [Field L] [IsDomain A] [IsDomain B] [IsDedekindDomain A] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (𝔭 : Ideal A) [h𝔭p : 𝔭.IsPrime] (h𝔭 : 𝔭 ≠ ⊥) (hf : ∀ 𝔔 ∈ primesOverFinset 𝔭 B, 𝔭.inertiaDeg 𝔔 = 1) : ∑ 𝔔 ∈ primesOverFinset 𝔭 B, (𝔭.ramificationIdx 𝔔 - 1) = Module.finrank K L - (primesOverFinset 𝔭 B).card

Specialization of Corollary 27 when all inertia degrees f(𝔔/𝔭) are one (e.g. for a separable extension over an algebraically closed residue field): the total ramification above 𝔭 equals [L:K] minus the number of primes above 𝔭.

class CompleteSmoothCurve (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] : Type

Abstract type-class data attached to a complete smooth curve Spec A, recording the degree of its canonical divisor.

• degCanonical : ℤ

noncomputable def degRamificationDivisor {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDedekindDomain B] [Algebra A B] (S : Finset (Ideal A)) : ℤ

The degree of the ramification divisor over a finite set S of primes of A, defined as ∑_{𝔭 ∈ S} ∑_{𝔔 ∣ 𝔭} (e(𝔔/𝔭) - 1).

theorem cor27_degree_formula {A : Type u_1} {B : Type u_2} (K : Type u_3) (L : Type u_4) [CommRing A] [CommRing B] [Field K] [Field L] [IsDomain A] [IsDomain B] [IsDedekindDomain A] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [CompleteSmoothCurve A] [CompleteSmoothCurve B] (S : Finset (Ideal A)) (hS : ∀ 𝔭 ∈ S, 𝔭.IsPrime ∧ 𝔭 ≠ ⊥) (hf : ∀ 𝔭 ∈ S, ∀ 𝔔 ∈ primesOverFinset 𝔭 B, 𝔭.inertiaDeg 𝔔 = 1) (h_unram_outside : ∀ (𝔭 : Ideal A), 𝔭.IsPrime → 𝔭 ≠ ⊥ → 𝔭 ∉ S → ∀ 𝔔 ∈ primesOverFinset 𝔭 B, 𝔭.ramificationIdx 𝔔 = 1) : CompleteSmoothCurve.degCanonical B = ↑(Module.finrank K L) * CompleteSmoothCurve.degCanonical A + degRamificationDivisor S

Corollary 27 (degree formula for the canonical divisor): for a finite separable covering B/A of complete smooth curves, ramified only over a finite set S, deg K_B = [L : K] · deg K_A + deg R, where R is the ramification divisor.

theorem cor27_degree_formula_pullback {A : Type u_1} {B : Type u_2} (K : Type u_3) (L : Type u_4) [CommRing A] [CommRing B] [Field K] [Field L] [IsDomain A] [IsDomain B] [IsDedekindDomain A] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [CompleteSmoothCurve A] [CompleteSmoothCurve B] (S : Finset (Ideal A)) (hS : ∀ 𝔭 ∈ S, 𝔭.IsPrime ∧ 𝔭 ≠ ⊥) (hf : ∀ 𝔭 ∈ S, ∀ 𝔔 ∈ primesOverFinset 𝔭 B, 𝔭.inertiaDeg 𝔔 = 1) (h_unram_outside : ∀ (𝔭 : Ideal A), 𝔭.IsPrime → 𝔭 ≠ ⊥ → 𝔭 ∉ S → ∀ 𝔔 ∈ primesOverFinset 𝔭 B, 𝔭.ramificationIdx 𝔔 = 1) (deg_fKY : ℤ) (h_pullback : deg_fKY = ↑(Module.finrank K L) * CompleteSmoothCurve.degCanonical A) : CompleteSmoothCurve.degCanonical B = deg_fKY + degRamificationDivisor S

Restatement of the degree formula in terms of the pulled-back canonical degree: deg K_B = deg(f* K_A) + deg R.