noncomputable def PullbackCanonical.pullbackDivisor (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDomain S] [IsDedekindDomain S] [Algebra R S] [Module.IsTorsionFree R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [Algebra S L] [IsFractionRing S L] : FractionalIdeal (nonZeroDivisors R) K →+* FractionalIdeal (nonZeroDivisors S) L

The pullback ring homomorphism on fractional ideals along R → S: extension of scalars from fractional ideals in the fraction field K of R to fractional ideals in the fraction field L of S.

theorem PullbackCanonical.pullbackDivisor_coeIdeal (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDomain S] [IsDedekindDomain S] [Algebra R S] [Module.IsTorsionFree R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [Algebra S L] [IsFractionRing S L] (I : Ideal R) : (pullbackDivisor R S K L) ↑I = ↑(Ideal.map (algebraMap R S) I)

On the embedding of an ordinary ideal I of R, the pullback agrees with the extension I · S.

theorem PullbackCanonical.pullbackDivisor_mul (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDomain S] [IsDedekindDomain S] [Algebra R S] [Module.IsTorsionFree R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [Algebra S L] [IsFractionRing S L] (I J : FractionalIdeal (nonZeroDivisors R) K) : (pullbackDivisor R S K L) (I * J) = (pullbackDivisor R S K L) I * (pullbackDivisor R S K L) J

The pullback respects multiplication of fractional ideals.

theorem PullbackCanonical.pullbackDivisor_one (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDomain S] [IsDedekindDomain S] [Algebra R S] [Module.IsTorsionFree R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [Algebra S L] [IsFractionRing S L] : (pullbackDivisor R S K L) 1 = 1

The pullback sends the unit fractional ideal to the unit fractional ideal.

noncomputable def PullbackCanonical.extensionDegree (R : Type u_1) [CommRing R] [IsDomain R] (S : Type u_2) [CommRing S] [IsDomain S] [Algebra R S] [Module.IsTorsionFree R S] : ℕ

The degree [Frac S : Frac R] of the field extension of fraction fields.

theorem PullbackCanonical.absNorm_pullbackIdeal (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDomain S] [IsDedekindDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] [Module.Free ℤ R] [Module.Free ℤ S] [Module.Finite ℤ S] [Module.Finite ℤ R] (I : Ideal R) : Ideal.absNorm (Ideal.map (algebraMap R S) I) = Ideal.absNorm I ^ extensionDegree R S

For a finite extension of Dedekind domains, the absolute norm of the pulled-back ideal I · S equals (N(I))^[Frac S : Frac R].

theorem PullbackCanonical.degPullback_canonical (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [IsDomain S] [IsDedekindDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S] [Module.Free ℤ R] [Module.Free ℤ S] [Module.Finite ℤ S] [Module.Finite ℤ R] (K_Y : Ideal R) : Ideal.absNorm (Ideal.map (algebraMap R S) K_Y) = Ideal.absNorm K_Y ^ extensionDegree R S

Degree-of-pullback formula for the canonical divisor: deg(K_Y · S) = deg(K_Y) · [Frac S : Frac R], stated at the level of absolute norms.