Dimensions of submodules

Dimension-counting criteria for nontrivial submodule intersection: two subspaces of a finite-dimensional space whose dimensions sum to more than the ambient dimension meet nontrivially, as do three subspaces whose dimensions sum to more than twice the ambient dimension, and a subspace of rank greater than the rank of a linear map f meets ker f nontrivially. Dually, the preimage of a subspace W under a linear map out of an m-dimensional space has codimension at most the codimension of W. A set spans a subspace of dimension at least n exactly when it contains n linearly independent vectors. Two disjoint subspaces of a finite-dimensional subspace U have dimensions adding to at most that of U. A subspace of dimension at least three contains x outside 𝕜 ∙ a and z outside span 𝕜 {a, x}. A finite-dimensional subspace spanning the whole space together with V, of dimension at most the codimension of V, is a complement of V; here V itself may be infinite-dimensional.

The rank of a product V.prod W of free submodules is the sum of their ranks over any semiring satisfying the strong rank condition. Consequently, the rank of a product map f.prodMap g with free ranges is the sum of the ranks of f and g. The dimension of the range of a linear map is unchanged by composing on the left with an injective map and on the right with a surjective one, and composing on the left with a map that does not lower the dimension of the range does not enlarge the kernel. Conjugating an endomorphism by a linear equivalence preserves the dimension of its kernel. The kernel of a surjection from a finite-dimensional space has dimension the difference of the dimensions.

theorem Submodule.finrank_inf_add_finrank_inf_le {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] (U V H : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥H] : Module.finrank 𝕜 ↥(U ⊓ H) + Module.finrank 𝕜 ↥(V ⊓ H) ≤ Module.finrank 𝕜 ↥(U ⊓ V ⊓ H) + Module.finrank 𝕜 ↥((U ⊔ V) ⊓ H)

Intersecting with a fixed subspace gives a supermodular dimension function.

theorem Submodule.inf_ne_bot_of_finrank_lt {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {V W : Submodule 𝕜 E} (h : Module.finrank 𝕜 E < Module.finrank 𝕜 ↥V + Module.finrank 𝕜 ↥W) : V ⊓ W ≠ ⊥

Two subspaces whose dimensions sum to more than the dimension of the ambient space have nontrivial intersection.

theorem Submodule.finrank_add_finrank_le_of_disjoint_of_le {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {S T U : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥U] (h : Disjoint S T) (hS : S ≤ U) (hT : T ≤ U) : Module.finrank 𝕜 ↥S + Module.finrank 𝕜 ↥T ≤ Module.finrank 𝕜 ↥U

Two disjoint subspaces of a finite-dimensional subspace U have dimensions adding to at most that of U. This is the relative form of Submodule.finrank_add_finrank_le_of_disjoint, which bounds them by the dimension of the ambient space.

theorem Submodule.inf_inf_ne_bot_of_finrank_lt {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {U V W : Submodule 𝕜 E} (h : 2 * Module.finrank 𝕜 E < Module.finrank 𝕜 ↥U + Module.finrank 𝕜 ↥V + Module.finrank 𝕜 ↥W) : U ⊓ V ⊓ W ≠ ⊥

Three subspaces whose dimensions sum to more than twice the dimension of the ambient space have nontrivial common intersection.

theorem Submodule.finrank_add_finrank_le_finrank_comap_add_finrank {𝕜 : Type u_1} [DivisionRing 𝕜] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module 𝕜 M] [AddCommGroup N] [Module 𝕜 N] [FiniteDimensional 𝕜 M] [FiniteDimensional 𝕜 N] (f : M →ₗ[𝕜] N) (W : Submodule 𝕜 N) : Module.finrank 𝕜 M + Module.finrank 𝕜 ↥W ≤ Module.finrank 𝕜 ↥(comap f W) + Module.finrank 𝕜 N

The preimage of a subspace W under a linear map f : M → N of finite-dimensional spaces has codimension at most the codimension of W: dim M + dim W ≤ dim (f⁻¹ W) + dim N.

theorem Submodule.le_finrank_span_iff_exists_linearIndependent {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {s : Set E} [Module.Finite 𝕜 ↥(span 𝕜 s)] {n : ℕ} : n ≤ Module.finrank 𝕜 ↥(span 𝕜 s) ↔ ∃ (v : Fin n → E), LinearIndependent 𝕜 v ∧ ∀ (i : Fin n), v i ∈ s

A set spans a subspace of dimension at least n exactly when it contains n linearly independent vectors.

theorem Submodule.isCompl_of_codisjoint_of_finrank_le {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {V S : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥S] (h : Codisjoint V S) (hrank : Module.finrank 𝕜 ↥S ≤ Module.finrank 𝕜 (E ⧸ V)) : IsCompl V S

A finite-dimensional subspace S which spans the whole space together with V, and whose dimension is at most the codimension of V, is a complement of V. Indeed S maps onto E ⧸ V, so the two dimensions agree and the map is injective.

theorem Submodule.exists_mem_notMem_span_of_ncard_lt {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {V : Submodule 𝕜 E} {s : Set E} (hs : s.Finite) (h : s.ncard < Module.finrank 𝕜 ↥V) : ∃ z ∈ V, z ∉ span 𝕜 s

A subspace with more dimensions than a finite set has elements contains a vector outside the span of the set.

theorem Submodule.exists_mem_notMem_span_pair {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {V : Submodule 𝕜 E} (a : E) (h : 3 ≤ Module.finrank 𝕜 ↥V) : ∃ x ∈ V, x ∉ 𝕜 ∙ a ∧ ∃ z ∈ V, z ∉ span 𝕜 {a, x}

A subspace of dimension at least three contains a vector x outside 𝕜 ∙ a and a vector z outside span {a, x}.

theorem Submodule.lift_rank_le_of_disjoint_ker {𝕜 : Type u_1} [Ring 𝕜] {M : Type u} {N : Type v} [AddCommGroup M] [Module 𝕜 M] [AddCommGroup N] [Module 𝕜 N] {V : Submodule 𝕜 M} {f : M →ₗ[𝕜] N} (h : Disjoint V f.ker) : Cardinal.lift.{v, u} (Module.rank 𝕜 ↥V) ≤ Cardinal.lift.{u, v} f.rank

A submodule meeting the kernel of f trivially has rank at most the rank of f, since f maps it injectively into its range.

theorem Submodule.rank_prod {𝕜 : Type u_1} [Semiring 𝕜] [StrongRankCondition 𝕜] {M : Type u} {N : Type v} [AddCommMonoid M] [Module 𝕜 M] [AddCommMonoid N] [Module 𝕜 N] (V : Submodule 𝕜 M) (W : Submodule 𝕜 N) [Module.Free 𝕜 ↥V] [Module.Free 𝕜 ↥W] : Module.rank 𝕜 ↥(V.prod W) = Cardinal.lift.{v, u} (Module.rank 𝕜 ↥V) + Cardinal.lift.{u, v} (Module.rank 𝕜 ↥W)

The rank of a product of free submodules is the sum of their ranks.

theorem LinearMap.rank_prodMap {𝕜 : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u} {N' : Type v} [Semiring 𝕜] [StrongRankCondition 𝕜] [AddCommMonoid M] [Module 𝕜 M] [AddCommMonoid N] [Module 𝕜 N] [AddCommMonoid M'] [Module 𝕜 M'] [AddCommMonoid N'] [Module 𝕜 N'] (f : M →ₗ[𝕜] M') (g : N →ₗ[𝕜] N') [Module.Free 𝕜 ↥f.range] [Module.Free 𝕜 ↥g.range] : (f.prodMap g).rank = Cardinal.lift.{v, u} f.rank + Cardinal.lift.{u, v} g.rank

The rank of a product map with free ranges is the sum of the ranks of its components.

theorem LinearMap.finrank_range_comp_comp {𝕜 : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type v} [Semiring 𝕜] [AddCommMonoid M] [Module 𝕜 M] [AddCommMonoid N] [Module 𝕜 N] [AddCommMonoid N'] [Module 𝕜 N'] {V : Type u_4} [AddCommMonoid V] [Module 𝕜 V] (A : N →ₗ[𝕜] N') (L : M →ₗ[𝕜] N) (B : V →ₗ[𝕜] M) (hA : Function.Injective ⇑A) (hB : Function.Surjective ⇑B) : Module.finrank 𝕜 ↥(A ∘ₗ L ∘ₗ B).range = Module.finrank 𝕜 ↥L.range

The dimension of the range of a linear map is unchanged by composing on the left with an injective map and on the right with a surjective one.

theorem LinearMap.ker_comp_eq_of_finrank_range_le {K : Type u_4} {V : Type u_5} {V₂ : Type u_6} {V₃ : Type u_7} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] (A : V →ₗ[K] V₂) (P : V₂ →ₗ[K] V₃) [FiniteDimensional K ↥A.range] (h : Module.finrank K ↥A.range ≤ Module.finrank K ↥(P ∘ₗ A).range) : (P ∘ₗ A).ker = A.ker

If composing a map A of finite rank on the left with P does not lower the dimension of its range, then it does not enlarge its kernel: ker (P ∘ A) = ker A. Indeed P is then injective on the range of A.

theorem LinearMap.finrank_ker_eq_sub_of_surjective {K : Type u_1} {M : Type v} {N : Type u_2} [Ring K] [HasRankNullity.{v, u_1} K] [StrongRankCondition K] [AddCommGroup M] [Module K M] [Module.Finite K M] [AddCommGroup N] [Module K N] (f : M →ₗ[K] N) (hf : Function.Surjective ⇑f) : Module.finrank K ↥f.ker = Module.finrank K M - Module.finrank K N

Rank–nullity for a surjection: the kernel of a surjective linear map from a finite module has dimension the difference of the dimensions.

@[simp]

theorem LinearEquiv.finrank_ker_conj {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (f : Module.End R M) : Module.finrank R ↥(LinearMap.ker (e.conj f)) = Module.finrank R ↥(LinearMap.ker f)

Conjugate endomorphisms have kernels of the same dimension.