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?

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 (↥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