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.

Additional definition

• Algebra.IsQuadraticExtension: An extension of rings R ⊆ S is quadratic if S is a free R-algebra of rank 2.

theorem mk_eq_mk_of_basis {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type w} {ι' : Type w'} [InvariantBasisNumber R] (v : Module.Basis ι R M) (v' : Module.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 Module.Basis.indexEquiv {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type w} [InvariantBasisNumber R] {ι' : Type w} (v : Module.Basis ι R M) (v' : Module.Basis ι' R M) : Cardinal.mk ι = Cardinal.mk ι'

theorem Basis.le_span'' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [RankCondition R] {ι : Type u_2} [Fintype ι] (b : Module.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} [Semiring R] [AddCommMonoid M] [Module R M] [RankCondition R] {ι : Type u_2} (b : Module.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 Module.Basis.le_span {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type u_2} [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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type u_2} (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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type u_2} (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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type u_2} (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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type u_2} (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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type w} (b : Module.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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type w} (b : Module.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 card_le_of_injective'' {R : Type u} [Semiring R] [StrongRankCondition R] {α β : Type v} (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Function.Injective ⇑f) : Cardinal.mk α ≤ Cardinal.mk β

StrongRankCondition implies that if there is an injective linear map (α →₀ R) →ₗ[R] β →₀ R, then the cardinal of α is smaller than or equal to the cardinal of β.

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

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

theorem Basis.card_le_card_of_linearIndependent_aux {R : Type u_2} [Semiring 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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type w} (b : Module.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 Module.Basis.mk_eq_rank'' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type v} (v : Basis ι R M) : Cardinal.mk ι = Module.rank R M

theorem Module.Basis.mk_range_eq_rank {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type w} [Fintype ι] (h : Module.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 Module.Basis.card_le_card_of_linearIndependent {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type u_2} [Fintype ι] (b : Basis ι R M) {ι' : Type u_3} [Fintype ι'] {v : ι' → M} (hv : LinearIndependent R v) : Fintype.card ι' ≤ Fintype.card ι

theorem Module.Basis.card_le_card_of_submodule {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid 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 Module.Basis.card_le_card_of_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid 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 Module.Basis.mk_eq_rank {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid 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 Module.Basis.mk_eq_rank' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {s : Set M} (hs : LinearIndepOn R id s) : Module.rank R ↥(Submodule.span R s) = Cardinal.mk ↑s

theorem toENat_rank_span_set {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type w} [StrongRankCondition R] {v : ι → M} {s : Set ι} (hs : LinearIndepOn R v s) : Cardinal.toENat (Module.rank R ↥(Submodule.span R (v '' s))) = s.encard

def Submodule.inductionOnRank {ι : Type w} {R : Type u_3} {M : Type u_4} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [IsDomain R] [Finite ι] (b : Module.Basis ι R M) (P : Submodule R M → Sort u_2) (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_2} {S : Type u_3} [CommRing R] [StrongRankCondition R] [Ring S] [IsDomain S] [Algebra R S] {n : Type u_4} {m : Type u_5} [Fintype n] [Fintype m] (b : Module.Basis n R S) {I : Ideal S} (hI : I ≠ ⊥) (c : Module.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} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type w} [StrongRankCondition R] (h : Basis ι R M) : finrank R M = Nat.card ι

theorem Module.finrank_eq_card_basis {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type w} [Fintype ι] (h : Basis ι R M) : 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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type w} (h : Basis ι R M) : ↑(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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type w} {b : Finset ι} (h : Basis { x : ι // x ∈ b } R M) : 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) [Semiring R] [StrongRankCondition R] : Module.rank R R = 1

@[simp]

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

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

noncomputable def Module.Basis.unique (R : Type u) [Semiring R] [StrongRankCondition R] {ι : Type u_2} (b : Basis ι R R) : Unique ι

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

Equations

• Module.Basis.unique R b = ⋯.some

theorem Module.rank_lt_aleph0 (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid 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_2} {M : Type u_3} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set M} [Module.Finite R ↥(Submodule.span R t)] (hs : LinearIndepOn R id s) (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) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] : ↑(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) [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {M' : Type u_2} [AddCommMonoid 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} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {M' : Type u_2} [AddCommMonoid M'] [Module R M'] [Module.Finite R M] (f : M →ₗ[R] M') : Module.finrank R ↥(range f) ≤ Module.finrank R M

theorem LinearMap.finrank_le_of_isSMulRegular {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {S : Type u_2} [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'

theorem Module.finrank_top_le_finrank_of_isScalarTower (R : Type u) (S : Type u_1) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [Semiring S] [Module S M] [Module R S] [IsScalarTower R S S] [FaithfulSMul R S] [IsScalarTower R S M] : finrank S M ≤ finrank R M

Also see Module.finrank_top_le_finrank_of_isScalarTower_of_free for a version with different typeclass constraints.

theorem Module.finrank_bot_le_finrank_of_isScalarTower (R : Type u) [Semiring R] [StrongRankCondition R] (S : Type u_2) (T : Type u_3) [Semiring S] [Semiring T] [Module R T] [Module S T] [Module R S] [IsScalarTower R S T] [IsScalarTower S T T] [FaithfulSMul S T] [Module.Finite R T] : finrank R S ≤ finrank R T

Also see Module.finrank_bot_le_finrank_of_isScalarTower_of_free for a version with different typeclass constraints.

theorem Submodule.exists_finset_span_eq_linearIndepOn (K : Type u_2) {M : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] (s : Set M) [Module.Finite K ↥(span K s)] : ∃ (t : Finset M), ↑t ⊆ s ∧ t.card = Module.finrank K ↥(span K s) ∧ span K ↑t = span K s ∧ LinearIndepOn K id ↑t

This is a version of exists_linearIndependent with an upper estimate on the size of the finite set we choose.

theorem Submodule.exists_fun_fin_finrank_span_eq (K : Type u_2) {M : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] (s : Set M) [Module.Finite K ↥(span K s)] : ∃ (f : Fin (Module.finrank K ↥(span K s)) → M), (∀ (i : Fin (Module.finrank K ↥(span K s))), f i ∈ s) ∧ span K (Set.range f) = span K s ∧ LinearIndependent K f

theorem Submodule.mem_span_set_iff_exists_finsupp_le_finrank {K : Type u_2} {M : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] {s : Set M} {x : M} [Module.Finite K ↥(span K s)] : x ∈ span K s ↔ ∃ (c : M →₀ K), c.support.card ≤ Module.finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun (mi : M) (r : K) => r • mi) = x

This is a version of mem_span_set with an estimate on the number of terms in the sum.

class Algebra.IsQuadraticExtension (R : Type u_2) (S : Type u_3) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S] extends Module.Free R S : Prop

An extension of rings R ⊆ S is quadratic if S is a free R-algebra of rank 2.

• exists_basis : Nonempty ((I : Type u_3) × Basis I R S)
• finrank_eq_two' : Module.finrank R S = 2

theorem Algebra.IsQuadraticExtension.finrank_eq_two (R : Type u_2) (S : Type u_3) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S] [IsQuadraticExtension R S] : Module.finrank R S = 2