structure CurveMorphismData : Type (max (u_1 + 1) (u_2 + 1))

Algebraic data for a morphism of smooth curves: a pair of Dedekind domains R → S corresponding to the coordinate rings of the source and target curves.

• R : Type u_1
• S : Type u_2
• commRingR : CommRing self.R
• commRingS : CommRing self.S
• isDedekindR : IsDedekindDomain self.R
• isDedekindS : IsDedekindDomain self.S
• algebraRS : Algebra self.R self.S

noncomputable def CurveMorphismData.ramificationIndex (φ : CurveMorphismData) (P : IsDedekindDomain.HeightOneSpectrum φ.S) : ℕ

The local ramification index e_P = d_P at a height-one prime P of the target ring, the multiplicity with which f^*(f(P)) contains P.

noncomputable def CurveMorphismData.ramificationDivisorCoeff (φ : CurveMorphismData) (P : IsDedekindDomain.HeightOneSpectrum φ.S) : ℤ

Coefficient d_P − 1 of the ramification divisor at the prime P.

noncomputable def CurveMorphismData.ramificationDivisor (φ : CurveMorphismData) : IsDedekindDomain.HeightOneSpectrum φ.S → ℤ

The ramification divisor R = Σ (d_x − 1) x as a function on the height-one spectrum of the target curve (Lec 21).

noncomputable def CurveMorphismData.ramificationDivisorDegree (φ : CurveMorphismData) (s : Finset (IsDedekindDomain.HeightOneSpectrum φ.S)) : ℤ

Degree of the ramification divisor over a finite set of primes, i.e. deg R = Σ_P (d_P − 1).

def CurveMorphismData.IsRamifiedAt (φ : CurveMorphismData) (P : IsDedekindDomain.HeightOneSpectrum φ.S) : Prop

Predicate P is a ramification point: ramification index strictly greater than 1.