Length of modules #
Main results #
Module.length
:Module.length R M
is the length ofM
as anR
-module.Module.length_pos
: The length of a nontrivial module is positiveModule.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 ⋯
Instances For
theorem
Module.length_eq_height
(R : Type u_1)
(M : Type u_2)
[Ring R]
[AddCommGroup M]
[Module R M]
:
theorem
Module.length_eq_coheight
(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]
:
@[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]
:
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]
:
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 = ⊤)
:
theorem
Module.length_eq_top_iff_infiniteDimensionalOrder
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
:
theorem
Module.length_ne_top_iff_finiteDimensionalOrder
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module 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
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.height_strictMono
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
[IsArtinian R M]
[IsNoetherian 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 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)
:
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)
:
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]
:
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]
:
theorem
Module.length_eq_rank
(K : Type u_5)
(M : Type u_6)
[DivisionRing K]
[AddCommGroup M]
[Module 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]
: