Lemmas about rank and finrank in rings satisfying strong rank condition.

Main statements

For modules over rings satisfying the rank condition

• Basis.le_span: the cardinality of a basis is bounded by the cardinality of any spanning set

For modules over rings satisfying the strong rank condition

• linearIndependent_le_span: For any linearly independent family v : ι → M and any finite spanning set w : Set M, the cardinality of ι is bounded by the cardinality of w.
• linearIndependent_le_basis: If b is a basis for a module M, and s is a linearly independent set, then the cardinality of s is bounded by the cardinality of b.

For modules over rings with invariant basis number (including all commutative rings and all noetherian rings)

• mk_eq_mk_of_basis: the dimension theorem, any two bases of the same vector space have the same cardinality.

theorem mk_eq_mk_of_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} {ι' : Type w'} [InvariantBasisNumber R] (v : Basis ι R M) (v' : Basis ι' R M) : Cardinal.lift.{w', w} (Cardinal.mk ι) = Cardinal.lift.{w, w'} (Cardinal.mk ι')

The dimension theorem: if v and v' are two bases, their index types have the same cardinalities.

def Basis.indexEquiv {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} {ι' : Type w'} [InvariantBasisNumber R] (v : Basis ι R M) (v' : Basis ι' R M) : ι ≃ ι'

Given two bases indexed by ι and ι' of an R-module, where R satisfies the invariant basis number property, an equiv ι ≃ ι'.

Equations

• v.indexEquiv v' = ⋯.some

theorem mk_eq_mk_of_basis' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} [InvariantBasisNumber R] {ι' : Type w} (v : Basis ι R M) (v' : Basis ι' R M) : Cardinal.mk ι = Cardinal.mk ι'

theorem Basis.le_span'' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [RankCondition R] {ι : Type u_1} [Fintype ι] (b : Basis ι R M) {w : Set M} [Fintype ↑w] (s : Submodule.span R w = ⊤) : Fintype.card ι ≤ Fintype.card ↑w

An auxiliary lemma for Basis.le_span.

If R satisfies the rank condition, then for any finite basis b : Basis ι R M, and any finite spanning set w : Set M, the cardinality of ι is bounded by the cardinality of w.

theorem basis_le_span' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [RankCondition R] {ι : Type u_1} (b : Basis ι R M) {w : Set M} [Fintype ↑w] (s : Submodule.span R w = ⊤) : Cardinal.mk ι ≤ ↑(Fintype.card ↑w)

Another auxiliary lemma for Basis.le_span, which does not require assuming the basis is finite, but still assumes we have a finite spanning set.

theorem Basis.le_span {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} [RankCondition R] {J : Set M} (v : Basis ι R M) (hJ : Submodule.span R J = ⊤) : Cardinal.mk ↑(Set.range ⇑v) ≤ Cardinal.mk ↑J

If R satisfies the rank condition, then the cardinality of any basis is bounded by the cardinality of any spanning set.

theorem linearIndependent_le_span_aux' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} [Fintype ι] (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype ↑w] (s : Set.range v ≤ ↑(Submodule.span R w)) : Fintype.card ι ≤ Fintype.card ↑w

theorem LinearIndependent.finite_of_le_span_finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Finite ↑w] (s : Set.range v ≤ ↑(Submodule.span R w)) : Finite ι

If R satisfies the strong rank condition, then any linearly independent family v : ι → M contained in the span of some finite w : Set M, is itself finite.

theorem linearIndependent_le_span' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype ↑w] (s : Set.range v ≤ ↑(Submodule.span R w)) : Cardinal.mk ι ≤ ↑(Fintype.card ↑w)

If R satisfies the strong rank condition, then for any linearly independent family v : ι → M contained in the span of some finite w : Set M, the cardinality of ι is bounded by the cardinality of w.

theorem linearIndependent_le_span {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype ↑w] (s : Submodule.span R w = ⊤) : Cardinal.mk ι ≤ ↑(Fintype.card ↑w)

If R satisfies the strong rank condition, then for any linearly independent family v : ι → M and any finite spanning set w : Set M, the cardinality of ι is bounded by the cardinality of w.

theorem linearIndependent_le_span_finset {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} (v : ι → M) (i : LinearIndependent R v) (w : Finset M) (s : Submodule.span R ↑w = ⊤) : Cardinal.mk ι ≤ ↑w.card

A version of linearIndependent_le_span for Finset.

theorem linearIndependent_le_infinite_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v) : Cardinal.mk κ ≤ Cardinal.mk ι

An auxiliary lemma for linearIndependent_le_basis: we handle the case where the basis b is infinite.

theorem linearIndependent_le_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type w} (b : Basis ι R M) {κ : Type w} (v : κ → M) (i : LinearIndependent R v) : Cardinal.mk κ ≤ Cardinal.mk ι

Over any ring R satisfying the strong rank condition, if b is a basis for a module M, and s is a linearly independent set, then the cardinality of s is bounded by the cardinality of b.

theorem Basis.card_le_card_of_linearIndependent_aux {R : Type u_1} [Ring R] [StrongRankCondition R] (n : ℕ) {m : ℕ} (v : Fin m → Fin n → R) : LinearIndependent R v → m ≤ n

Let R satisfy the strong rank condition. If m elements of a free rank n R-module are linearly independent, then m ≤ n.

theorem maximal_linearIndependent_eq_infinite_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v) (m : i.Maximal) : Cardinal.mk κ = Cardinal.mk ι

Over any ring R satisfying the strong rank condition, if b is an infinite basis for a module M, then every maximal linearly independent set has the same cardinality as b.

This proof (along with some of the lemmas above) comes from [Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973]

theorem Basis.mk_eq_rank'' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type v} (v : Basis ι R M) : Cardinal.mk ι = Module.rank R M

theorem Basis.mk_range_eq_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} [StrongRankCondition R] (v : Basis ι R M) : Cardinal.mk ↑(Set.range ⇑v) = Module.rank R M

theorem rank_eq_card_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type w} [Fintype ι] (h : Basis ι R M) : Module.rank R M = ↑(Fintype.card ι)

If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the cardinality of the basis.

theorem Basis.card_le_card_of_linearIndependent {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} [Fintype ι] (b : Basis ι R M) {ι' : Type u_2} [Fintype ι'] {v : ι' → M} (hv : LinearIndependent R v) : Fintype.card ι' ≤ Fintype.card ι

theorem Basis.card_le_card_of_submodule {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} {ι' : Type w'} [StrongRankCondition R] (N : Submodule R M) [Fintype ι] (b : Basis ι R M) [Fintype ι'] (b' : Basis ι' R ↥N) : Fintype.card ι' ≤ Fintype.card ι

theorem Basis.card_le_card_of_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} {ι' : Type w'} [StrongRankCondition R] {N O : Submodule R M} (hNO : N ≤ O) [Fintype ι] (b : Basis ι R ↥O) [Fintype ι'] (b' : Basis ι' R ↥N) : Fintype.card ι' ≤ Fintype.card ι

theorem Basis.mk_eq_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} [StrongRankCondition R] (v : Basis ι R M) : Cardinal.lift.{v, w} (Cardinal.mk ι) = Cardinal.lift.{w, v} (Module.rank R M)

theorem Basis.mk_eq_rank' {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} [StrongRankCondition R] (v : Basis ι R M) : Cardinal.lift.{max v m, w} (Cardinal.mk ι) = Cardinal.lift.{max w m, v} (Module.rank R M)

theorem rank_span {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} [StrongRankCondition R] {v : ι → M} (hv : LinearIndependent R v) : Module.rank R ↥(Submodule.span R (Set.range v)) = Cardinal.mk ↑(Set.range v)

theorem rank_span_set {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {s : Set M} (hs : LinearIndependent R fun (x : ↑s) => ↑x) : Module.rank R ↥(Submodule.span R s) = Cardinal.mk ↑s

def Submodule.inductionOnRank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} [StrongRankCondition R] [IsDomain R] [Finite ι] (b : Basis ι R M) (P : Submodule R M → Sort u_1) (ih : (N : Submodule R M) → ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N) (N : Submodule R M) : P N

An induction (and recursion) principle for proving results about all submodules of a fixed finite free module M. A property is true for all submodules of M if it satisfies the following "inductive step": the property is true for a submodule N if it's true for all submodules N' of N with the property that there exists 0 ≠ x ∈ N such that the sum N' + Rx is direct.

Equations

• Submodule.inductionOnRank b P ih N = Submodule.inductionOnRankAux b P ih (Fintype.card ι) N ⋯

theorem Ideal.rank_eq {R : Type u_1} {S : Type u_2} [CommRing R] [StrongRankCondition R] [Ring S] [IsDomain S] [Algebra R S] {n : Type u_3} {m : Type u_4} [Fintype n] [Fintype m] (b : Basis n R S) {I : Ideal S} (hI : I ≠ ⊥) (c : Basis m R ↥I) : Fintype.card m = Fintype.card n

If S a module-finite free R-algebra, then the R-rank of a nonzero R-free ideal I of S is the same as the rank of S.

theorem Module.finrank_eq_nat_card_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type w} [StrongRankCondition R] (h : Basis ι R M) : Module.finrank R M = Nat.card ι

theorem Module.finrank_eq_card_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type w} [Fintype ι] (h : Basis ι R M) : Module.finrank R M = Fintype.card ι

If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the cardinality of the basis.

theorem Module.mk_finrank_eq_card_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type w} (h : Basis ι R M) : ↑(Module.finrank R M) = Cardinal.mk ι

If a free module is of finite rank, then the cardinality of any basis is equal to its finrank.

theorem Module.finrank_eq_card_finset_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type w} {b : Finset ι} (h : Basis { x : ι // x ∈ b } R M) : Module.finrank R M = b.card

If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the cardinality of the basis. This lemma uses a Finset instead of indexed types.

@[simp]

theorem Module.rank_self (R : Type u) [Ring R] [StrongRankCondition R] : Module.rank R R = 1

@[simp]

theorem Module.finrank_self (R : Type u) [Ring R] [StrongRankCondition R] : Module.finrank R R = 1

A ring satisfying StrongRankCondition (such as a DivisionRing) is one-dimensional as a module over itself.

noncomputable def Basis.unique (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type u_1} (b : Basis ι R R) : Unique ι

Given a basis of a ring over itself indexed by a type ι, then ι is Unique.

Equations

• Basis.unique R b = ⋯.some

theorem Module.rank_lt_aleph0 (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] : Module.rank R M < Cardinal.aleph0

The rank of a finite module is finite.

noncomputable instance Module.instFintypeElemExtendOfFiniteSubtypeMemSubmoduleSpan {R : Type u_1} {M : Type u_2} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set M} [Module.Finite R ↥(Submodule.span R t)] (hs : LinearIndependent R Subtype.val) (hst : s ⊆ t) : Fintype ↑(hs.extend hst)

Equations

• Module.instFintypeElemExtendOfFiniteSubtypeMemSubmoduleSpan hs hst = Classical.choice ⋯

@[simp]

theorem Module.finrank_eq_rank (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] : ↑(Module.finrank R M) = Module.rank R M

If M is finite, finrank M = rank M.

theorem Submodule.finrank_eq_rank (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M) : ↑(Module.finrank R ↥N) = Module.rank R ↥N

If M is finite, then finrank N = rank N for all N : Submodule M. Note that such an N need not be finitely generated.

theorem LinearMap.finrank_le_finrank_of_injective {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {M' : Type u_1} [AddCommGroup M'] [Module R M'] [Module.Finite R M'] {f : M →ₗ[R] M'} (hf : Function.Injective ⇑f) : Module.finrank R M ≤ Module.finrank R M'

theorem LinearMap.finrank_range_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {M' : Type u_1} [AddCommGroup M'] [Module R M'] [Module.Finite R M] (f : M →ₗ[R] M') : Module.finrank R ↥(LinearMap.range f) ≤ Module.finrank R M

theorem LinearMap.finrank_le_of_isSMulRegular {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {S : Type u_1} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (L L' : Submodule R M) [Module.Finite R ↥L'] {s : S} (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') : Module.finrank R ↥L ≤ Module.finrank R ↥L'

@[deprecated LinearMap.finrank_le_of_isSMulRegular]

theorem LinearMap.finrank_le_of_smul_regular {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {S : Type u_1} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (L L' : Submodule R M) [Module.Finite R ↥L'] {s : S} (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') : Module.finrank R ↥L ≤ Module.finrank R ↥L'

Alias of LinearMap.finrank_le_of_isSMulRegular.