@[reducible, inline]

abbrev LinearEquivDivisors.WeilDivisorGroup (Y : Type u_1) : Type u_1

The group of Weil divisors on Y as finitely supported functions Y → ℤ.

def LinearEquivDivisors.WeilDivisor.IsEffective {Y : Type u_1} (D : WeilDivisorGroup Y) : Prop

A Weil divisor D is effective iff all of its coefficients are nonnegative.

def LinearEquivDivisors.CartierDivisor.LinearlyEquivalent (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (I J : ↥(nonZeroDivisors (Ideal A))) : Prop

Two Cartier divisors (nonzero ideals of a Dedekind domain) are linearly equivalent iff they represent the same element of the class group.

@[reducible, inline]

abbrev LinearEquivDivisors.PrincipalDivisors (Y : Type u_2) : Type u_2

The subgroup of principal Weil divisors inside the full Weil divisor group.

def LinearEquivDivisors.WeilLinearlyEquivalent {Y : Type u_1} (P : PrincipalDivisors Y) (D₁ D₂ : WeilDivisorGroup Y) : Prop

Linear equivalence of Weil divisors modulo a chosen subgroup P of principal divisors: D₁ ~ D₂ iff D₁ - D₂ ∈ P (Def 32, Lec 16).

theorem LinearEquivDivisors.weilLinearlyEquivalent_equivalence {Y : Type u_1} (P : PrincipalDivisors Y) : Equivalence (WeilLinearlyEquivalent P)

Linear equivalence of Weil divisors is an equivalence relation.

theorem LinearEquivDivisors.WeilLinearlyEquivalent.refl {Y : Type u_1} (P : PrincipalDivisors Y) (D : WeilDivisorGroup Y) : WeilLinearlyEquivalent P D D

Linear equivalence of Weil divisors is reflexive.

theorem LinearEquivDivisors.WeilLinearlyEquivalent.symm {Y : Type u_1} (P : PrincipalDivisors Y) {D₁ D₂ : WeilDivisorGroup Y} (h : WeilLinearlyEquivalent P D₁ D₂) : WeilLinearlyEquivalent P D₂ D₁

Linear equivalence of Weil divisors is symmetric.

theorem LinearEquivDivisors.WeilLinearlyEquivalent.trans {Y : Type u_1} (P : PrincipalDivisors Y) {D₁ D₂ D₃ : WeilDivisorGroup Y} (h₁ : WeilLinearlyEquivalent P D₁ D₂) (h₂ : WeilLinearlyEquivalent P D₂ D₃) : WeilLinearlyEquivalent P D₁ D₃

Linear equivalence of Weil divisors is transitive.

def LinearEquivDivisors.weilLinearEquivSetoid {Y : Type u_1} (P : PrincipalDivisors Y) : Setoid (WeilDivisorGroup Y)

The setoid on Weil divisors given by linear equivalence relative to P.

def LinearEquivDivisors.WeilDivisor.degree {Y : Type u_1} (D : WeilDivisorGroup Y) : ℤ

The degree of a Weil divisor is the sum of its coefficients.

theorem LinearEquivDivisors.WeilDivisor.degree_zero {Y : Type u_1} : degree 0 = 0

The zero divisor has degree zero.

theorem LinearEquivDivisors.WeilDivisor.degree_add {Y : Type u_1} [DecidableEq Y] (D₁ D₂ : WeilDivisorGroup Y) : degree (D₁ + D₂) = degree D₁ + degree D₂

Degree is additive on sums of Weil divisors.

theorem LinearEquivDivisors.WeilDivisor.degree_neg {Y : Type u_1} (D : WeilDivisorGroup Y) : degree (-D) = -degree D

Negating a Weil divisor negates its degree.

theorem LinearEquivDivisors.WeilDivisor.degree_sub {Y : Type u_1} [DecidableEq Y] (D₁ D₂ : WeilDivisorGroup Y) : degree (D₁ - D₂) = degree D₁ - degree D₂

Degree is additive on differences of Weil divisors.

theorem LinearEquivDivisors.WeilDivisor.degree_eq_of_linearlyEquiv {Y : Type u_1} [DecidableEq Y] {P : PrincipalDivisors Y} (hP : ∀ D ∈ P, degree D = 0) {D₁ D₂ : WeilDivisorGroup Y} (h : WeilLinearlyEquivalent P D₁ D₂) : degree D₁ = degree D₂

If every divisor in the principal subgroup P has degree zero, then linearly equivalent Weil divisors have equal degree.

def LinearEquivDivisors.completeLinearSystem {Y : Type u_1} (P : PrincipalDivisors Y) (D : WeilDivisorGroup Y) : Set (WeilDivisorGroup Y)

The complete linear system |D|: all effective Weil divisors linearly equivalent to D.

theorem LinearEquivDivisors.mem_completeLinearSystem_isEffective {Y : Type u_1} (P : PrincipalDivisors Y) {D D' : WeilDivisorGroup Y} (h : D' ∈ completeLinearSystem P D) : WeilDivisor.IsEffective D'

Every member of |D| is effective.

theorem LinearEquivDivisors.mem_completeLinearSystem_equiv {Y : Type u_1} (P : PrincipalDivisors Y) {D D' : WeilDivisorGroup Y} (h : D' ∈ completeLinearSystem P D) : WeilLinearlyEquivalent P D' D

Every member of |D| is linearly equivalent to D.

theorem LinearEquivDivisors.self_mem_completeLinearSystem {Y : Type u_1} (P : PrincipalDivisors Y) {D : WeilDivisorGroup Y} (hD : WeilDivisor.IsEffective D) : D ∈ completeLinearSystem P D

An effective Weil divisor belongs to its own complete linear system.

theorem LinearEquivDivisors.completeLinearSystem_top_eq {Y : Type u_1} (D : WeilDivisorGroup Y) : completeLinearSystem ⊤ D = {D' : WeilDivisorGroup Y | WeilDivisor.IsEffective D'}

With the full principal subgroup, the complete linear system is the set of all effective divisors.

theorem LinearEquivDivisors.completeLinearSystem_bot_eq {Y : Type u_1} (D : WeilDivisorGroup Y) : completeLinearSystem ⊥ D = {D' : WeilDivisorGroup Y | WeilDivisor.IsEffective D' ∧ D' = D}

With trivial principal subgroup, the complete linear system reduces to {D} intersected with the effective cone.

theorem LinearEquivDivisors.cartierLinearlyEquivalent_equivalence (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] : Equivalence fun (I J : ↥(nonZeroDivisors (Ideal A))) => CartierDivisor.LinearlyEquivalent A I J

Linear equivalence of Cartier divisors on a Dedekind domain is an equivalence relation.

theorem LinearEquivDivisors.cartierDivisor_principal_iff_trivialClass (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] (I : Ideal A) (hI : I ∈ nonZeroDivisors (Ideal A)) : ClassGroup.mk0 ⟨I, hI⟩ = 1 ↔ Submodule.IsPrincipal I

A nonzero ideal is principal iff its image in the class group is trivial.

noncomputable def LinearEquivDivisors.completeLinearSystemDim (k : Type u_2) [Field k] (V : Type u_3) [AddCommGroup V] [Module k V] [Module.Finite k V] : ℤ

Dimension of a complete linear system, defined as dim_k V - 1 where V is the global sections module.

theorem LinearEquivDivisors.completeLinearSystemDim_eq (k : Type u_2) [Field k] (V : Type u_3) [AddCommGroup V] [Module k V] [Module.Finite k V] : completeLinearSystemDim k V = ↑(Module.finrank k V) - 1

Definitional unfolding of completeLinearSystemDim.

theorem LinearEquivDivisors.completeLinearSystemDim_nonneg (k : Type u_2) [Field k] (V : Type u_3) [AddCommGroup V] [Module k V] [Module.Finite k V] (hV : 0 < Module.finrank k V) : 0 ≤ completeLinearSystemDim k V

If V has positive k-dimension, the linear system dimension is nonneg.

theorem LinearEquivDivisors.completeLinearSystem_nonempty_of_nontrivial (k : Type u_2) [Field k] (V : Type u_3) [AddCommGroup V] [Module k V] [Nontrivial V] : Nonempty (Projectivization k V)

Nontriviality of V yields a nonempty projectivization, so a nonempty linear system.

theorem LinearEquivDivisors.WeilDivisor.IsEffective_zero {Y : Type u_1} : IsEffective 0

The zero divisor is effective.

theorem LinearEquivDivisors.WeilDivisor.IsEffective_add {Y : Type u_1} {D₁ D₂ : WeilDivisorGroup Y} (h₁ : IsEffective D₁) (h₂ : IsEffective D₂) : IsEffective (D₁ + D₂)

The sum of two effective Weil divisors is effective.