Documentation

Mathlib.RingTheory.Length

Length of modules #

Main results #

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
Instances For
    theorem Module.coe_length (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] :
    theorem Module.length_eq_height (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] :
    theorem Module.length_eq_zero_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R 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] :
    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_ne_top_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module 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] :
    theorem Module.length_submodule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} :
    theorem Module.length_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} :
    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) :
    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) :
    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 ) :
    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] :
    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] :
    @[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_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)