def torsionSubmodule (R : Type u_3) [CommRing R] (M : Type u_4) [AddCommGroup M] [Module R M] : Submodule R M

The torsion submodule of M: the submodule of elements killed by some non-zero-divisor of R. This realizes Definition 39 (torsion subsheaf) on curves.

def Submodule.saturation {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (N : Submodule R M) : Submodule R M

The saturation of a submodule N ⊆ M: the preimage under M → M/N of the torsion submodule of M/N. Realizes Definition 40 (saturation) on curves.

theorem Submodule.le_saturation {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (N : Submodule R M) : N ≤ N.saturation

A submodule is contained in its saturation.

theorem Submodule.saturation_map_mkQ {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (N : Submodule R M) : map N.mkQ N.saturation = torsion R (M ⧸ N)

The image of the saturation N.saturation in M/N equals the torsion submodule of M/N.

theorem isTorsionFree_of_linearEquiv {R : Type u_1} [CommRing R] [IsDomain R] {N : Type u_3} {P : Type u_4} [AddCommGroup N] [AddCommGroup P] [Module R N] [Module R P] (e : N ≃ₗ[R] P) (h : Module.IsTorsionFree R N) : Module.IsTorsionFree R P

Being torsion-free is preserved under linear isomorphism.

theorem Submodule.quotient_saturation_isTorsionFree {R : Type u_1} [CommRing R] [IsDomain R] {M : Type u_2} [AddCommGroup M] [Module R M] (N : Submodule R M) : Module.IsTorsionFree R (M ⧸ N.saturation)

The quotient M / N.saturation is torsion-free, by construction of the saturation.

noncomputable def CoherentSheavesCurves.sheafRank (R : Type u_1) [CommRing R] (K : Type u_2) [Field K] [Algebra R K] (M : Type u_3) [AddCommGroup M] [Module R M] : ℕ

The rank of an R-module M (Definition 41): the K-dimension of K ⊗_R M, where K is a field over R (typically the fraction field).

theorem CoherentSheavesCurves.sheafRank_additive (R : Type u_1) [CommRing R] (K : Type u_2) [Field K] [Algebra R K] {A : Type u_3} {B : Type u_4} {C : Type u_5} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] (f : A →ₗ[R] B) (g : B →ₗ[R] C) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (H : Function.Exact ⇑f ⇑g) [Module.Flat R K] [FiniteDimensional K (TensorProduct R K B)] : sheafRank R K B = sheafRank R K A + sheafRank R K C

The rank is additive on short exact sequences (when K is R-flat and the middle term has finite dimensional base-change).

theorem CoherentSheavesCurves.sheafRank_additive_fractionRing {R : Type u_3} [CommRing R] [IsDomain R] {K : Type u_4} [Field K] [Algebra R K] [IsFractionRing R K] {A : Type u_5} {B : Type u_6} {C : Type u_7} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] (f : A →ₗ[R] B) (g : B →ₗ[R] C) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (H : Function.Exact ⇑f ⇑g) [FiniteDimensional K (TensorProduct R K B)] : sheafRank R K B = sheafRank R K A + sheafRank R K C

Specialization of sheafRank_additive to the case where K is the fraction field of an integral domain R, automatically supplying flatness.

@[reducible, inline]

abbrev CoherentSheavesCurves.K0 (R : Type u_1) [Ring R] : Type (u_1 + 1)

The Grothendieck group K_0 of coherent sheaves on a curve, abbreviated through the abstract construction GrothendieckGroupK0.

@[reducible, inline]

abbrev CoherentSheavesCurves.K0.classOf (R : Type u_1) [Ring R] (M : ModuleCat R) : K0 R

The class of an R-module M in the Grothendieck group K_0(R).

theorem CoherentSheavesCurves.K0.ses_relation (R : Type u_1) [Ring R] {A B C : ModuleCat R} (f : ↑A →ₗ[R] ↑B) (g : ↑B →ₗ[R] ↑C) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hex : Function.Exact ⇑f ⇑g) : classOf R B = classOf R A + classOf R C

A short exact sequence 0 → A → B → C → 0 induces the additivity relation [B] = [A] + [C] in K_0.

theorem CoherentSheavesCurves.K0.classOf_iso (R : Type u_1) [Ring R] (M N : ModuleCat R) (e : ↑M ≃ₗ[R] ↑N) : classOf R M = classOf R N

Isomorphic modules have equal classes in the Grothendieck group.

theorem CoherentSheavesCurves.K0.classOf_prod (R : Type u_1) [Ring R] (M N : ModuleCat R) : classOf R (ModuleCat.of R (↑M × ↑N)) = classOf R M + classOf R N

The class of a direct product equals the sum of the classes of the factors in K_0.

noncomputable def CoherentSheavesCurves.K0.lift (R : Type u_1) [Ring R] {G : Type u_2} [AddCommGroup G] (φ : ModuleCat R → G) (hφ : DegreeAdditivity.IsSESAdditive R φ) : K0 R →+ G

Universal property of K_0: any short-exact-sequence-additive function ModuleCat R → G lifts uniquely to a group homomorphism K_0(R) →+ G.

theorem CoherentSheavesCurves.K0.lift_classOf (R : Type u_1) [Ring R] {G : Type u_2} [AddCommGroup G] (φ : ModuleCat R → G) (hφ : DegreeAdditivity.IsSESAdditive R φ) (M : ModuleCat R) : (lift R φ hφ) (classOf R M) = φ M

The universal lift agrees with the original additive function on each class.

theorem CoherentSheavesCurves.K0.lift_unique (R : Type u_1) [Ring R] {G : Type u_2} [AddCommGroup G] (ψ₁ ψ₂ : K0 R →+ G) (h : ∀ (M : ModuleCat R), ψ₁ (classOf R M) = ψ₂ (classOf R M)) : ψ₁ = ψ₂

Uniqueness of the universal lift: two group homomorphisms from K_0(R) agreeing on all generators [M] are equal.

@[deprecated DegreeAdditivity.K0SESRelation (since := "2025-06-01")]

def CoherentSheavesCurves.SESRelation (R : Type u_1) [CommRing R] : Type (max (max (max u_1 (u_2 + 1)) (u_3 + 1)) (u_4 + 1))

Deprecated alias for DegreeAdditivity.K0SESRelation.

noncomputable def CoherentSheavesCurves.degree (R : Type u_3) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] : ℕ∞

The degree of a module M over R, defined as the R-module length of M (a value in ℕ∞). On curves this realizes the degree of a torsion coherent sheaf.

theorem CoherentSheavesCurves.degree_additive_ses {R : Type u_1} [Ring R] {A : Type u_3} {B : Type u_4} {C : Type u_5} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] (f : A →ₗ[R] B) (g : B →ₗ[R] C) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (H : Function.Exact ⇑f ⇑g) : degree R B = degree R A + degree R C

Degree is additive on short exact sequences.

theorem CoherentSheavesCurves.lemma34 {R : Type u_1} [Ring R] {E : Type u_3} {E' : Type u_4} {T : Type u_5} [AddCommGroup E] [AddCommGroup E'] [AddCommGroup T] [Module R E] [Module R E'] [Module R T] (f : E →ₗ[R] E') (g : E' →ₗ[R] T) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (H : Function.Exact ⇑f ⇑g) : degree R E' = degree R E + degree R T

Lemma 34: degree additivity on short exact sequences 0 → E → E' → T → 0.

theorem CoherentSheavesCurves.degree_le_of_injective {R : Type u_1} [Ring R] {A : Type u_3} {B : Type u_4} [AddCommGroup A] [AddCommGroup B] [Module R A] [Module R B] (f : A →ₗ[R] B) (hf : Function.Injective ⇑f) : degree R A ≤ degree R B

Degree is monotone under injective linear maps.

theorem CoherentSheavesCurves.degree_le_of_surjective {R : Type u_1} [Ring R] {A : Type u_3} {B : Type u_4} [AddCommGroup A] [AddCommGroup B] [Module R A] [Module R B] (f : A →ₗ[R] B) (hf : Function.Surjective ⇑f) : degree R B ≤ degree R A

A surjective linear map can only decrease degree.

theorem CoherentSheavesCurves.degree_eq_finrank (K : Type u_3) [DivisionRing K] (V : Type u_4) [AddCommGroup V] [Module K V] [Module.Finite K V] : degree K V = ↑(Module.finrank K V)

For finite-dimensional vector spaces over a division ring, the degree equals the dimension.

theorem CoherentSheavesCurves.degree_prod (R : Type u_3) [Ring R] (M : Type u_4) (N : Type u_5) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] : degree R (M × N) = degree R M + degree R N

Degree is additive on direct products of modules.

theorem CoherentSheavesCurves.sheafRank_of_torsion {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {M : Type u_3} [AddCommGroup M] [Module R M] (hM : Module.IsTorsion R M) : sheafRank R K M = 0

A torsion module has rank zero (its base-change to the fraction field vanishes).

theorem noZeroSMulDivisors_of_linearEquiv {R' : Type u_2} [CommRing R'] [IsDomain R'] {M₁ : Type u_3} {M₂ : Type u_4} [AddCommGroup M₁] [Module R' M₁] [AddCommGroup M₂] [Module R' M₂] [NoZeroSMulDivisors R' M₂] (e : M₁ ≃ₗ[R'] M₂) : NoZeroSMulDivisors R' M₁

A linear isomorphism transports the NoZeroSMulDivisors property along its inverse direction.

noncomputable def degTorsionFree (R : Type u_2) [CommRing R] [IsDomain R] [IsDedekindDomain R] (M : Type u_3) [AddCommGroup M] [Module R M] [Module.Finite R M] [NoZeroSMulDivisors R M] : ℤ

The degree of a finite torsion-free module over a Dedekind domain, defined via the determinant invertible-ideal construction.

theorem degTorsionFree_congr {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {M₁ : Type u_2} {M₂ : Type u_3} [AddCommGroup M₁] [Module R M₁] [Module.Finite R M₁] [NoZeroSMulDivisors R M₁] [AddCommGroup M₂] [Module R M₂] [Module.Finite R M₂] [NoZeroSMulDivisors R M₂] (e : M₁ ≃ₗ[R] M₂) : degTorsionFree R M₁ = degTorsionFree R M₂

The torsion-free degree is invariant under linear isomorphism.

theorem degTorsionFree_simple_ext {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {M' : Type u_2} [AddCommGroup M'] [Module R M'] [Module.Finite R M'] [NoZeroSMulDivisors R M'] (N : Submodule R M') [Module.Finite R ↥N] [NoZeroSMulDivisors R ↥N] (hlen : Module.length R (M' ⧸ N) = 1) : degTorsionFree R M' = degTorsionFree R ↥N + 1

If the quotient M'/N has length one (a simple extension), then deg(M') = deg(N) + 1.

theorem intermediate_submodule_exists {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {M' : Type u_2} [AddCommGroup M'] [Module R M'] [Module.Finite R M'] [NoZeroSMulDivisors R M'] (N : Submodule R M') [Module.Finite R ↥N] [NoZeroSMulDivisors R ↥N] (n : ℕ) (hn : 0 < n) (hlen : Module.length R (M' ⧸ N) = ↑(n + 1)) (htor : Module.IsTorsion R (M' ⧸ N)) : ∃ (N' : Submodule R M') (_ : Module.Finite R ↥N') (_ : NoZeroSMulDivisors R ↥N'), N ≤ N' ∧ Module.length R (↥N' ⧸ Submodule.comap N'.subtype N) = 1 ∧ Module.length R (M' ⧸ N') = ↑n ∧ Module.IsTorsion R (M' ⧸ N')

Given a torsion quotient M'/N of length n+1 > 1, there exists an intermediate torsion-free submodule N ≤ N' ≤ M' with N'/N simple and M'/N' of length n.

def P_lemma34 (R : Type u_2) [CommRing R] [IsDomain R] [IsDedekindDomain R] (M' : Type u_3) [AddCommGroup M'] [Module R M'] [Module.Finite R M'] [NoZeroSMulDivisors R M'] (k : ℕ) : Prop

Auxiliary inductive predicate used to prove Lemma 34: for a fixed M', the relation deg M' = deg N + k holds for every submodule N with M'/N torsion of length k.

theorem P_lemma34_holds {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {M' : Type u_2} [AddCommGroup M'] [Module R M'] [Module.Finite R M'] [NoZeroSMulDivisors R M'] (k : ℕ) : P_lemma34 R M' k

P_lemma34 holds for every k, proved by strong induction.

theorem lemma34_degTorsionFree {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {M' : Type u_2} [AddCommGroup M'] [Module R M'] [Module.Finite R M'] [NoZeroSMulDivisors R M'] (N : Submodule R M') [Module.Finite R ↥N] [NoZeroSMulDivisors R ↥N] (k : ℕ) (hk : 0 < k) (hlen : Module.length R (M' ⧸ N) = ↑k) (htor : Module.IsTorsion R (M' ⧸ N)) : degTorsionFree R M' = degTorsionFree R ↥N + ↑k

Lemma 34 (degree additivity for torsion-free modules): if M'/N is torsion of length k > 0, then deg M' = deg N + k.