@[reducible, inline]
Weil divisors on a curve Y: finitely supported integer-valued functions on the
underlying point set.
Instances For
theorem
Prop24Picard.fiber_dimension_formula
(k : Type u_2)
[Field k]
{S : Type u_3}
[CommRing S]
[IsDomain S]
{ι : Type u_4}
[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)
:
Fiber-dimension formula: for a free k[X]-module S of rank |ι| and a nonzero
p ∈ k[X], the k-dimension of S / (p) equals |ι| · deg p.
theorem
Prop24Picard.prop24_degree_principal_divisor_eq_zero
(k : Type u_2)
[Field k]
{S : Type u_3}
[CommRing S]
[IsDomain S]
{ι : Type u_4}
[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})) = 0
Proposition 24: the degree of a principal divisor (p) − (q) of two polynomials of
the same degree is zero.
theorem
Prop24Picard.fiber_dimension_eq_rank
(k : Type u_2)
[Field k]
{S : Type u_3}
[CommRing S]
[IsDomain S]
{ι : Type u_4}
[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 ι
Specialisation of the fiber-dimension formula at a linear polynomial X - c:
the fiber over a point has dimension equal to the rank of the basis.
theorem
Prop24Picard.fiber_dimension_constant
(k : Type u_2)
[Field k]
{S : Type u_3}
[CommRing S]
[IsDomain S]
{ι : Type u_4}
[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 two different constants c₁, c₂ coincide.
noncomputable def
Prop24Picard.degPic
{Y : Type u_1}
(P : AddSubgroup (WeilDiv Y))
(hP : ∀ D ∈ P, weilDegree D = 0)
:
The degree homomorphism descends from Weil divisors to Pic(Y) = WeilDiv / P when
P is a subgroup of degree-zero divisors.
Instances For
theorem
Prop24Picard.degPic_mk
{Y : Type u_1}
(P : AddSubgroup (WeilDiv Y))
(hP : ∀ D ∈ P, weilDegree D = 0)
(D : WeilDiv Y)
:
The degree map on the Picard group computes the Weil degree of a chosen lift.