noncomputable def 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] : ℤ

Degree of a finitely generated torsion-free module over a Dedekind domain (Lec 22, Lemma 34 setting).

theorem Lemma34.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 degree of a torsion-free module is an isomorphism invariant.

theorem Lemma34.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

Base case of degree additivity: if M'/N has length one (a simple extension), then deg M' = deg N + 1.

theorem Lemma34.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')

Inductive step ingredient: given N ⊆ M' with quotient of torsion length n + 1, there exists an intermediate N ≤ N' ⊆ M' such that N'/N has length one and M'/N' has torsion length n.

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

Helper: NoZeroSMulDivisors transfers along a linear equivalence.

theorem Lemma34.Module.IsTorsion.of_linearEquiv {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (h : Module.IsTorsion R N) : Module.IsTorsion R M

Helper: the torsion property transfers along a linear equivalence.

def Lemma34.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

Induction predicate for Lemma 34: for any submodule N ⊆ M' with torsion quotient of length k, the degrees differ by k.

theorem Lemma34.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

Induction on length: the predicate P_lemma34 holds for every k.

theorem Lemma34.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

Submodule version of Lemma 34: for N ⊆ M' torsion-free with M'/N torsion of length k, the degrees satisfy deg M' = deg N + k.

theorem lemma34_degree_additivity (R : Type u) [CommRing R] [IsDomain R] [IsDedekindDomain R] {E E' T : Type v} [AddCommGroup E] [Module R E] [Module.Finite R E] [NoZeroSMulDivisors R E] [AddCommGroup E'] [Module R E'] [Module.Finite R E'] [NoZeroSMulDivisors R E'] [AddCommGroup T] [Module R T] (hT : Module.IsTorsion R T) (hTfin : IsFiniteLength R T) (f : E →ₗ[R] E') (g : E' →ₗ[R] T) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hex : Function.Exact ⇑f ⇑g) : Lemma34.degTorsionFree R E' = Lemma34.degTorsionFree R E + ↑(Module.length R T).toNat

Lec 22, Lemma 34 (degree additivity): for a short exact sequence 0 → E → E' → T → 0 of finite modules over a Dedekind domain R, with E, E' torsion-free and T torsion of finite length, deg E' = deg E + length(T).