Length of modules

Main results

• Module.length: Module.length R M is the length of M as an R-module.
• Module.length_pos: The length of a nontrivial module is positive
• Module.length_ne_top: The length of an Artinian and Noetherian module is finite.
• Module.length_eq_add_of_exact: Length is additive in exact sequences.

noncomputable def Module.length (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] : ℕ∞

The length of a module, defined as the krull dimension of its submodule lattice.

Equations

• Module.length R M = (Order.krullDim (Submodule R M)).unbot ⋯

theorem Module.coe_length (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] : ↑(length R M) = Order.krullDim (Submodule R M)

theorem Module.length_eq_height (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] : length R M = Order.height ⊤

theorem Module.length_eq_coheight (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] : length R M = Order.coheight ⊥

theorem Module.length_eq_zero_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : length R M = 0 ↔ Subsingleton M

@[simp]

theorem Module.length_eq_zero {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Subsingleton M] : length R M = 0

@[simp]

theorem Module.length_eq_zero_of_subsingleton_ring {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Subsingleton R] : length R M = 0

theorem Module.length_pos_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : 0 < length R M ↔ Nontrivial M

theorem Module.length_pos {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial M] : 0 < length R M

theorem Module.length_compositionSeries {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (s : CompositionSeries (Submodule R M)) (h₁ : RelSeries.head s = ⊥) (h₂ : RelSeries.last s = ⊤) : ↑s.length = length R M

theorem Module.length_eq_top_iff_infiniteDimensionalOrder {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : length R M = ⊤ ↔ InfiniteDimensionalOrder (Submodule R M)

theorem Module.length_ne_top_iff_finiteDimensionalOrder {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : length R M ≠ ⊤ ↔ FiniteDimensionalOrder (Submodule R M)

theorem Module.length_ne_top_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : length R M ≠ ⊤ ↔ IsFiniteLength R M

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

@[simp]

theorem Module.finiteDimensionalOrder_submodule_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : FiniteDimensionalOrder (Submodule R M) ↔ IsFiniteLength R M

instance instFiniteDimensionalOrderSubmoduleOfIsArtinianOfIsNoetherian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] : FiniteDimensionalOrder (Submodule R M)

theorem Module.length_submodule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} : length R ↥N = Order.height N

theorem Module.length_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} : length R (M ⧸ N) = Order.coheight N

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

theorem Module.length_eq_of_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M] (h : Function.Surjective ⇑(algebraMap S R)) : length S M = length R M

theorem Module.length_bot {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : length R ↥⊥ = 0

@[simp]

theorem Module.length_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : length R ↥⊤ = length R M

theorem Submodule.height_lt_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (N : Submodule R M) : Order.height N < ⊤

theorem Submodule.height_strictMono {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] : StrictMono Order.height

theorem Submodule.length_lt {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] {N : Submodule R M} (h : N ≠ ⊤) : Module.length R ↥N < Module.length R M

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

Length is additive in exact sequences.

theorem Module.length_le_of_injective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) (hf : Function.Injective ⇑f) : length R N ≤ length R M

theorem Module.length_le_of_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Type u_4} [AddCommGroup P] [Module R P] (g : M →ₗ[R] P) (hg : Function.Surjective ⇑g) : length R P ≤ length R M

@[simp]

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

@[simp]

theorem Module.length_pi_of_fintype (R : Type u_1) [Ring R] {ι : Type u_5} [Fintype ι] (M : ι → Type u_6) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] : length R ((i : ι) → M i) = ∑ i : ι, length R (M i)

@[simp]

theorem Module.length_finsupp {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_5} : length R (ι →₀ M) = ENat.card ι * length R M

@[simp]

theorem Module.length_pi {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_5} : length R (ι → M) = ENat.card ι * length R M

theorem Module.length_of_free (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [Free R M] : length R M = Cardinal.toENat (Module.rank R M) * length R R

theorem Module.length_of_free_of_finite (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Free R M] [Module.Finite R M] : length R M = ↑(finrank R M) * length R R

theorem Module.length_eq_one_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : length R M = 1 ↔ IsSimpleModule R M

@[simp]

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

theorem Module.length_eq_rank (K : Type u_5) (M : Type u_6) [DivisionRing K] [AddCommGroup M] [Module K M] : length K M = Cardinal.toENat (Module.rank K M)

theorem Module.length_eq_finrank (K : Type u_5) (M : Type u_6) [DivisionRing K] [AddCommGroup M] [Module K M] [Module.Finite K M] : length K M = ↑(finrank K M)

theorem Submodule.length_le_length_restrictScalars {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (A : Type u_5) [Ring A] [SMul A R] [Module A M] [IsScalarTower A R M] (p : Submodule R M) : Module.length R ↥p ≤ Module.length A ↥(restrictScalars A p)

theorem Submodule.length_quotient_lt {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (p : Submodule R M) (h : p ≠ ⊥) : Module.length R (M ⧸ p) < Module.length R M