noncomputable def DegreeAdditivity.torsionDegree (R : Type u_1) (M : Type u_2) [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] : ℕ∞

The "torsion degree" of a module M over a domain R, defined as the length of its torsion submodule. Plays the role of ℓ(𝒯) in the degree additivity statement.

theorem DegreeAdditivity.length_eq_torsionDegree_add {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] : Module.length R M = torsionDegree R M + Module.length R (M ⧸ Submodule.torsion R M)

The length of a module decomposes as the sum of its torsion length and the length of the torsion-free quotient, via the short exact sequence 0 → 𝒯 → M → M/𝒯 → 0.

theorem DegreeAdditivity.torsionDegree_of_torsion {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] (htor : Module.IsTorsion R M) : torsionDegree R M = Module.length R M

For a torsion module, the torsion degree equals the full length.

theorem DegreeAdditivity.torsionDegree_of_torsionFree {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] (htf : Module.IsTorsionFree R M) : torsionDegree R M = 0

A torsion-free module has torsion degree zero.

theorem DegreeAdditivity.torsionDegree_zero (R : Type u_1) [CommRing R] [IsDomain R] : torsionDegree R PUnit.{u_2 + 1} = 0

The trivial module PUnit has torsion degree zero.

theorem DegreeAdditivity.LinearMap.map_torsion_mem {R : Type u_1} {N : Type u_2} {M : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup N] [Module R N] [AddCommGroup M] [Module R M] (f : N →ₗ[R] M) {x : N} (hx : x ∈ Submodule.torsion R N) : f x ∈ Submodule.torsion R M

A linear map sends torsion elements to torsion elements.

theorem DegreeAdditivity.lemma34_ses_length_additive {R : Type u_1} [Ring R] {N : Type u_2} {M : Type u_3} {P : Type u_4} [AddCommGroup N] [AddCommGroup M] [AddCommGroup P] [Module R N] [Module R M] [Module R P] (f : N →ₗ[R] M) (g : M →ₗ[R] P) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hex : Function.Exact ⇑f ⇑g) : Module.length R M = Module.length R N + Module.length R P

Lemma 34 (Lecture 22): Length is additive on short exact sequences: for 0 → N → M → P → 0, we have ℓ(M) = ℓ(N) + ℓ(P).

theorem DegreeAdditivity.lemma34_submodule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) : Module.length R M = Module.length R ↥N + Module.length R (M ⧸ N)

Instantiation of Lemma 34 to a submodule: ℓ(M) = ℓ(N) + ℓ(M/N).

theorem DegreeAdditivity.length_le_of_submodule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) : Module.length R ↥N ≤ Module.length R M

Length is monotone with respect to submodule inclusion.

theorem DegreeAdditivity.dvr_ord_uniformizer (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {π : R} (hπ : Irreducible π) : Ring.ord R π = 1

A uniformizer of a DVR has order one.

theorem DegreeAdditivity.dvr_ord_uniformizer_pow (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {π : R} (hπ : Irreducible π) (n : ℕ) : Ring.ord R (π ^ n) = ↑n

A power of a uniformizer has order equal to the exponent.

theorem DegreeAdditivity.dvr_determinant_length (R : Type u_1) [CommRing R] [IsDomain R] {a b : R} (hb : b ∈ nonZeroDivisors R) : Ring.ord R (a * b) = Ring.ord R a + Ring.ord R b

Multiplicativity of the order/length on non-zero-divisor products.

theorem DegreeAdditivity.top_exterior_power_rank_one (R : Type u_1) [CommRing R] [Nontrivial R] [StrongRankCondition R] (n : ℕ) : Module.finrank R ↥(⋀[R]^n (Fin n → R)) = 1

The top exterior power Λⁿ Rⁿ is free of rank one.

theorem DegreeAdditivity.exterior_power_vanishes_above_rank (R : Type u_1) [CommRing R] [Nontrivial R] [StrongRankCondition R] {n p : ℕ} (hp : n < p) : Module.finrank R ↥(⋀[R]^p (Fin n → R)) = 0

The p-th exterior power of Rⁿ vanishes when p > n.

structure DegreeAdditivity.K0SESRelation (R : Type u_1) [Ring R] : Type (max (max (max u_1 (u_2 + 1)) (u_3 + 1)) (u_4 + 1))

Data of a short exact sequence of R-modules 0 → N → M → P → 0, suitable as a defining relation in K₀(R).

• N : Type u_2
• M : Type u_3
• P : Type u_4
• instN : AddCommGroup self.N
• modN : Module R self.N
• instM : AddCommGroup self.M
• modM : Module R self.M
• instP : AddCommGroup self.P
• modP : Module R self.P
• f : self.N →ₗ[R] self.M
• g : self.M →ₗ[R] self.P
• f_inj : Function.Injective ⇑self.f
• g_surj : Function.Surjective ⇑self.g
• exact : Function.Exact ⇑self.f ⇑self.g

theorem DegreeAdditivity.degree_respects_K0 {R : Type u_1} [Ring R] (rel : K0SESRelation R) : Module.length R rel.M = Module.length R rel.N + Module.length R rel.P

Module length respects the K₀ short-exact-sequence relations: it is additive on sequences 0 → N → M → P → 0.

theorem DegreeAdditivity.degree_respects_iso {R : Type u_1} [Ring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : Module.length R M = Module.length R N

Module length is an isomorphism invariant.

theorem DegreeAdditivity.degree_additive_prod (R : Type u_1) [Ring R] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : Module.length R (M × N) = Module.length R M + Module.length R N

Length is additive on direct products.

theorem DegreeAdditivity.degree_zero (R : Type u_1) [Ring R] : Module.length R PUnit.{u_2 + 1} = 0

The trivial module has length zero.

theorem DegreeAdditivity.degree_simple (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsSimpleModule R M] : Module.length R M = 1

A simple module has length one.

theorem DegreeAdditivity.degree_finite {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] : Module.length R M ≠ ⊤

Modules that are both Artinian and Noetherian have finite length.

theorem DegreeAdditivity.dedekind_localization_is_dvr (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] {P : Ideal R} [P.IsPrime] (hP : P ≠ ⊥) : IsDiscreteValuationRing (Localization.AtPrime P)

The localization of a Dedekind domain at a nonzero prime is a DVR.

theorem DegreeAdditivity.dvr_torsionFree_is_free (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.IsTorsionFree R M] : Module.Free R M

Over a DVR, every finitely generated torsion-free module is free.