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?

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_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'