noncomputable def principalDivisorDegree (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] (I J : Ideal A) : ℤ

The degree of a principal divisor: difference of k-dimensions of A/I and A/J, where I, J are two ideals representing a divisor of the form (p) - (q).

theorem fiber_dimension_eq_rank (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) (c : k) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c)}) = Fintype.card ι

The fiber dimension at a closed point X - c equals the rank of S as a k[X]-module.

theorem fiber_dimension_constant (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) (c₁ c₂ : k) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c₁)}) = Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c₂)})

The fiber dimension at any closed point X - c is constant (equals the generic rank); a finite map has constant fiber dimension on a curve.

def IsPrincipalDivisorData (k : Type u_1) [Field k] (S : Type u_2) [CommRing S] [IsDomain S] [Algebra (Polynomial k) S] (p q : Polynomial k) : Prop

Witness for principal-divisor data on S: there exists s ∈ S{0} with q·s = p in S, i.e. p/q is a regular function in some sense.

class IsCompleteCurveAlg (k : Type u_1) [Field k] (S : Type u_2) [CommRing S] [IsDomain S] [Algebra (Polynomial k) S] : Prop

Type class encoding the completeness condition for a curve algebra S over k[X]: principal divisors of regular functions have equal numerator and denominator degrees.

• deg_eq_of_principal (p q : Polynomial k) : p ≠ 0 → q ≠ 0 → IsPrincipalDivisorData k S p q → p.natDegree = q.natDegree

theorem PrincipalDivisorDegZero.algebraMap_ne_zero_of_ne_zero (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) {p : Polynomial k} (hp : p ≠ 0) : (algebraMap (Polynomial k) S) p ≠ 0

Pushing a nonzero polynomial into S via the structure map yields a nonzero element (when S has a basis over k[X]).

theorem PrincipalDivisorDegZero.fiber_dimension_eq_rank_mul_natDegree (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) {p : Polynomial k} (hp : p ≠ 0) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) p}) = Fintype.card ι * p.natDegree

General fiber-dimension formula: dim_k(S/(p)) equals (rank of S) × (degree of p).

theorem PrincipalDivisorDegZero.fiber_dimension_linear_eq_rank (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) (c : k) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c)}) = Fintype.card ι

For a linear polynomial X - c, the fiber dimension equals the rank of S.

theorem PrincipalDivisorDegZero.fiber_dimension_linear_constant (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) (c₁ c₂ : k) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c₁)}) = Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c₂)})

Fiber dimensions at two linear polynomials X - c_1 and X - c_2 are equal.

theorem PrincipalDivisorDegZero.fiber_dimension_eq_of_natDegree_eq (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) (hdeg : p.natDegree = q.natDegree) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) p}) = Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) q})

Two polynomials of the same degree give equal fiber dimensions in S.

noncomputable def PrincipalDivisorDegZero.principalDivisorDeg (k : Type u_1) [Field k] (S : Type u_2) [CommRing S] [IsDomain S] [Algebra k S] (I J : Ideal S) : ℤ

Degree of a principal divisor in S: dim_k(S/I) - dim_k(S/J).

theorem PrincipalDivisorDegZero.principalDivisorDeg_eq_rank_mul_degDiff (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) : principalDivisorDeg k S (Ideal.span {(algebraMap (Polynomial k) S) p}) (Ideal.span {(algebraMap (Polynomial k) S) q}) = ↑(Fintype.card ι) * (↑p.natDegree - ↑q.natDegree)

Principal-divisor degree formula: equals the rank of S over k[X] times the difference of degrees of numerator and denominator.

theorem PrincipalDivisorDegZero.principal_divisor_deg_zero_of_natDegree_eq (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) (hdeg : p.natDegree = q.natDegree) : principalDivisorDeg k S (Ideal.span {(algebraMap (Polynomial k) S) p}) (Ideal.span {(algebraMap (Polynomial k) S) q}) = 0

When numerator and denominator have equal degree, the principal divisor degree vanishes.

theorem PrincipalDivisorDegZero.principal_divisor_deg_zero (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] [IsCompleteCurveAlg k S] (b : Module.Basis ι (Polynomial k) S) {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) (hpd : IsPrincipalDivisorData k S p q) : principalDivisorDeg k S (Ideal.span {(algebraMap (Polynomial k) S) p}) (Ideal.span {(algebraMap (Polynomial k) S) q}) = 0

Principal divisor degree zero (Proposition 24, Lecture 15; Proposition 25, Lecture 16): on a complete curve, the degree of a principal divisor is zero.

theorem PrincipalDivisorDegZero.principal_divisor_deg_zero_linear (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) (c₁ c₂ : k) : principalDivisorDeg k S (Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c₁)}) (Ideal.span {(algebraMap (Polynomial k) S) (Polynomial.X - Polynomial.C c₂)}) = 0

The principal divisor of (X - c_1) - (X - c_2) has degree zero: both linear factors contribute the same fiber dimension.

theorem PrincipalDivisorDegZero.principalDivisorDeg_affine_eq (k : Type u_1) [Field k] (p q : Polynomial k) : principalDivisorDeg k (Polynomial k) (Ideal.span {p}) (Ideal.span {q}) = ↑p.natDegree - ↑q.natDegree

For S = k[X] itself, the principal divisor degree equals the actual difference of degrees deg(p) - deg(q).

theorem proposition_25_fiber_dimension_formula (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] (b : Module.Basis ι (Polynomial k) S) {p : Polynomial k} (hp : p ≠ 0) : Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) p}) = Fintype.card ι * p.natDegree

Proposition 25 fiber-dimension formula: dim_k(S/(p)) = (rank S over k[X]) · deg(p).

theorem proposition_25_principal_divisor_deg_zero (k : Type u_1) [Field k] {S : Type u_2} [CommRing S] [IsDomain S] {ι : Type u_3} [Fintype ι] [Algebra (Polynomial k) S] [Algebra k S] [IsScalarTower k (Polynomial k) S] [IsCompleteCurveAlg k S] (b : Module.Basis ι (Polynomial k) S) {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) (hpd : IsPrincipalDivisorData k S p q) : ↑(Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) p})) - ↑(Module.finrank k (S ⧸ Ideal.span {(algebraMap (Polynomial k) S) q})) = 0

Proposition 25 in textbook form: on a complete smooth curve, every principal divisor has total degree zero (Proposition 24/25, Lectures 15-16).