theorem fundamental_identity_ramification {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [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 ≠ ⊥) : ∑ P ∈ primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P = Module.finrank K L

Fundamental identity in ramification theory: the sum over primes P of S above a maximal ideal p of R of e_P · f_P equals the field extension degree [L : K].

theorem fundamental_identity_local {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [IsLocalRing S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) = Module.finrank K L

Fundamental identity in the local case (DVR extension): e · f = [L : K].

@[reducible, inline]

abbrev IsUnramifiedAt' {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [P.IsPrime] [P.LiesOver p] : Prop

Abbreviation for Algebra.IsUnramifiedAt R P, naming the property that an algebra R → S is unramified at the prime P of S lying over p.

def IsUnramifiedOver {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (p : Ideal R) : Prop

R → S is unramified over p if it is unramified at every prime P of S lying over p.

theorem ramificationIdx_eq_one_of_isUnramifiedAt' {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [P.IsPrime] [hlo : P.LiesOver p] [IsDomain S] [IsNoetherianRing S] [Algebra.EssFiniteType R S] (h : IsUnramifiedAt' p P) (hP : P ≠ ⊥) : p.ramificationIdx P = 1

Being unramified at P implies the ramification index e_P = 1.

theorem isUnramifiedAt'_iff_ramificationIdx_eq_one {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [P.IsPrime] [hlo : P.LiesOver p] [IsDedekindDomain S] [Algebra.EssFiniteType R S] [IsDomain R] [Module.Finite ℤ R] [CharZero R] [Algebra.IsIntegral R S] (hP : P ≠ ⊥) : IsUnramifiedAt' p P ↔ p.ramificationIdx P = 1

For Dedekind domains in good characteristic, being unramified at P is equivalent to e_P = 1.

theorem discriminant_ne_zero_of_separable {ι : Type u_1} [DecidableEq ι] [Fintype ι] (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [Module.Finite K L] [Algebra.IsSeparable K L] (b : Module.Basis ι K L) : Algebra.discr K ⇑b ≠ 0

For a finite separable field extension K ⊆ L, the discriminant with respect to any basis is non-zero.

theorem discriminant_isUnit_of_separable {ι : Type u_1} [DecidableEq ι] [Fintype ι] (K : Type u_2) {L : Type u_3} [Field K] [Field L] [Algebra K L] [Module.Finite K L] [Algebra.IsSeparable K L] (b : Module.Basis ι K L) : IsUnit (Algebra.discr K ⇑b)

For a finite separable field extension, the discriminant is a unit.

theorem card_primes_over_le_finrank {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : (primesOverFinset p S).card ≤ Module.finrank K L

The number of primes above p is bounded by [L : K].

theorem sum_ramificationIdx_le_finrank {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : ∑ P ∈ primesOverFinset p S, p.ramificationIdx P ≤ Module.finrank K L

Sum of ramification indices over primes above p is bounded by [L : K].

theorem ramificationIdx_le_finrank' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [P.IsPrime] [P.LiesOver p] : p.ramificationIdx P ≤ Module.finrank K L

Each ramification index e_P is bounded by [L : K].

theorem inertiaDeg_le_finrank' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [P.IsPrime] [P.LiesOver p] (hp0 : p ≠ ⊥) : p.inertiaDeg P ≤ Module.finrank K L

Each inertia degree f_P is bounded by [L : K].

theorem dedekind_lying_over (R : Type u_1) (S : Type u_2) [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] [Module.Finite R S] [FaithfulSMul R S] (p : Ideal R) [hp : p.IsPrime] (_hp0 : p ≠ ⊥) : ∃ (P : Ideal S), P.IsPrime ∧ P.LiesOver p

Lying-over for Dedekind domains: any non-zero prime p of R has a prime P of S lying over it, when R ⊆ S is a finite faithfully flat extension.

theorem dedekind_contraction_is_prime (R : Type u_1) (S : Type u_2) [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] (P : Ideal S) [hP : P.IsPrime] : (Ideal.comap (algebraMap R S) P).IsPrime

The contraction of a prime ideal of S is a prime ideal of R.

instance dedekind_liesOver_contraction (R : Type u_1) (S : Type u_2) [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDedekindDomain S] [Algebra R S] (P : Ideal S) : P.LiesOver (Ideal.under R P)

Every prime ideal P of S lies over its contraction P ∩ R.

theorem primes_over_finite {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : (p.primesOver S).Finite

The set of primes of S above a non-zero maximal ideal p of R is finite.

noncomputable def totalRamificationAt {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] (p : Ideal R) [p.IsMaximal] (_hp0 : p ≠ ⊥) : ℤ

Local contribution at p to the ramification divisor: the sum ∑_{P|p} (e_P - 1).

theorem totalRamificationAt_nonneg {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : 0 ≤ totalRamificationAt S p hp0

The local ramification at p is non-negative.

theorem totalRamificationAt_le_finrank {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : totalRamificationAt S p hp0 ≤ ↑(Module.finrank K L)

The local ramification at p is bounded by the field extension degree [L : K].

theorem totalRamificationAt_eq_zero_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDedekindDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : totalRamificationAt S p hp0 = 0 ↔ ∀ P ∈ primesOverFinset p S, p.ramificationIdx P = 1

The local ramification at p vanishes iff every prime above p is unramified.

theorem riemann_hurwitz_formula (n g_X g_Y deg_R deg_KX deg_KY deg_pullback : ℤ) (h_deg_KX : deg_KX = 2 * g_X - 2) (h_deg_KY : deg_KY = 2 * g_Y - 2) (h_pullback : deg_pullback = n * deg_KY) (h_canonical : deg_KX = deg_pullback + deg_R) : 2 * g_X - 2 = n * (2 * g_Y - 2) + deg_R

Numerical Riemann–Hurwitz: given pullback identity and canonical decomposition, 2 g_X - 2 = n(2 g_Y - 2) + deg R.

theorem riemann_hurwitz_ramification_eq (n g_X g_Y R : ℤ) (hRH : 2 * g_X - 2 = n * (2 * g_Y - 2) + R) : R = 2 * g_X - 2 - n * (2 * g_Y - 2)

Solving Riemann–Hurwitz for the ramification divisor degree.

theorem riemann_hurwitz_genus_bound (n g_X g_Y R : ℤ) (hR : 0 ≤ R) (hRH : 2 * g_X - 2 = n * (2 * g_Y - 2) + R) : g_X ≥ n * g_Y - n + 1

Riemann–Hurwitz genus bound: g_X ≥ n g_Y - n + 1.

theorem riemann_hurwitz_with_arithmeticGenus (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra k B] [Module.Finite k B] (n total_ramification : ℤ) (h_formula : 2 * ↑(RiemannRochGeneral.arithmeticGenus k B) - 2 = n * (2 * ↑(RiemannRochGeneral.arithmeticGenus k A) - 2) + total_ramification) : total_ramification = 2 * ↑(RiemannRochGeneral.arithmeticGenus k B) - 2 - n * (2 * ↑(RiemannRochGeneral.arithmeticGenus k A) - 2)

Riemann–Hurwitz formulated using the algebraic arithmeticGenus.

theorem riemann_hurwitz_hyperelliptic (g : ℤ) : 2 * g - 2 = 2 * (2 * 0 - 2) + (2 * g + 2)

Numerical Riemann–Hurwitz identity for a hyperelliptic double cover of ℙ¹.

theorem riemann_hurwitz_hyperelliptic_ramification (g R : ℤ) (hRH : 2 * g - 2 = 2 * (2 * 0 - 2) + R) : R = 2 * g + 2

The ramification divisor of a hyperelliptic curve of genus g over ℙ¹ has degree 2g + 2.