doc-next-gen

Mathlib.LinearAlgebra.Dimension.RankNullity

Module docstring

{"# The rank nullity theorem

In this file we provide the rank nullity theorem as a typeclass, and prove various corollaries of the theorem. The main definition is HasRankNullity.{u} R, which states that 1. Every R-module M : Type u has a linear independent subset of cardinality Module.rank R M. 2. rank (M ⧸ N) + rank N = rank M for every R-module M : Type u and every N : Submodule R M.

The following instances are provided in mathlib: 1. DivisionRing.hasRankNullity for division rings in LinearAlgebra/Dimension/DivisionRing.lean. 2. IsDomain.hasRankNullity for commutative domains in LinearAlgebra/Dimension/Localization.lean.

TODO: prove the rank-nullity theorem for [Ring R] [IsDomain R] [StrongRankCondition R]. See nonempty_oreSet_of_strongRankCondition for a start. "}

HasRankNullity structure
(R : Type v) [inst : Ring R]
Full source 
/--
`HasRankNullity.{u}` is a class of rings satisfying
1. Every `R`-module `M : Type u` has a linear independent subset of cardinality `Module.rank R M`.
2. `rank (M ⧸ N) + rank N = rank M` for every `R`-module `M : Type u` and every `N : Submodule R M`.

Usually such a ring satisfies `HasRankNullity.{w}` for all universes `w`, and the universe
argument is there because of technical limitations to universe polymorphism.

See `DivisionRing.hasRankNullity` and `IsDomain.hasRankNullity`.
-/
@[pp_with_univ]
class HasRankNullity (R : Type v) [inst : Ring R] : Prop where
  exists_set_linearIndependent : ∀ (M : Type u) [AddCommGroup M] [Module R M],
    ∃ s : Set M, #s = Module.rank R M ∧ LinearIndepOn R id s
  rank_quotient_add_rank : ∀ {M : Type u} [AddCommGroup M] [Module R M] (N : Submodule R M),
    Module.rank R (M ⧸ N) + Module.rank R N = Module.rank R M
Rank-Nullity Theorem for Rings
Informal description
A ring \( R \) is said to satisfy the rank-nullity theorem if: 1. Every \( R \)-module \( M \) has a linearly independent subset whose cardinality equals the rank of \( M \). 2. For every \( R \)-module \( M \) and every submodule \( N \) of \( M \), the rank of the quotient module \( M / N \) plus the rank of \( N \) equals the rank of \( M \).
Submodule.rank_quotient_add_rank theorem
(N : Submodule R M) : Module.rank R (M ⧸ N) + Module.rank R N = Module.rank R M
Full source 
lemma Submodule.rank_quotient_add_rank (N : Submodule R M) :
    Module.rank R (M ⧸ N) + Module.rank R N = Module.rank R M :=
  HasRankNullity.rank_quotient_add_rank N
Rank-Nullity Theorem: $\text{rank}(M/N) + \text{rank}(N) = \text{rank}(M)$
Informal description
For any $R$-module $M$ and any submodule $N$ of $M$, the rank of the quotient module $M/N$ plus the rank of $N$ equals the rank of $M$, i.e., \[ \text{rank}(M/N) + \text{rank}(N) = \text{rank}(M). \]
exists_set_linearIndependent theorem
: ∃ s : Set M, #s = Module.rank R M ∧ LinearIndependent (ι := s) R Subtype.val
Full source 
lemma exists_set_linearIndependent :
    ∃ s : Set M, #s = Module.rank R M ∧ LinearIndependent (ι := s) R Subtype.val :=
  HasRankNullity.exists_set_linearIndependent M
Existence of Basis-Like Linear Independent Set in Modules Satisfying Rank-Nullity
Informal description
For any $R$-module $M$ where $R$ satisfies the rank-nullity theorem, there exists a subset $s \subseteq M$ such that: 1. The cardinality of $s$ equals the rank of $M$ as an $R$-module 2. The set $s$ is linearly independent over $R$ (when viewed through the inclusion map $\text{Subtype.val}: s \hookrightarrow M$)
LinearMap.lift_rank_range_add_rank_ker theorem
(f : M →ₗ[R] M') : lift.{u} (Module.rank R (LinearMap.range f)) + lift.{v} (Module.rank R (LinearMap.ker f)) = lift.{v} (Module.rank R M)
Full source 
theorem LinearMap.lift_rank_range_add_rank_ker (f : M →ₗ[R] M') :
    lift.{u} (Module.rank R (LinearMap.range f)) + lift.{v} (Module.rank R (LinearMap.ker f)) =
      lift.{v} (Module.rank R M) := by
  haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)
  rw [← f.quotKerEquivRange.lift_rank_eq, ← lift_add, rank_quotient_add_rank]
Rank-Nullity Theorem with Universe Lifting: $\text{rank}(\text{range } f) + \text{rank}(\ker f) = \text{rank}(M)$
Informal description
For any linear map $f \colon M \to M'$ between $R$-modules, the sum of the rank of the range of $f$ (lifted to universe $u$) and the rank of the kernel of $f$ (lifted to universe $v$) equals the rank of $M$ (lifted to universe $v$), i.e., \[ \text{rank}(\text{range } f) + \text{rank}(\ker f) = \text{rank}(M). \]
LinearMap.rank_range_add_rank_ker theorem
(f : M →ₗ[R] M₁) : Module.rank R (LinearMap.range f) + Module.rank R (LinearMap.ker f) = Module.rank R M
Full source 
/-- The **rank-nullity theorem** -/
theorem LinearMap.rank_range_add_rank_ker (f : M →ₗ[R] M₁) :
    Module.rank R (LinearMap.range f) + Module.rank R (LinearMap.ker f) = Module.rank R M := by
  haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)
  rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]
Rank-Nullity Theorem: $\text{rank}(\text{range } f) + \text{rank}(\ker f) = \text{rank}(M)$
Informal description
For any linear map $f \colon M \to M₁$ between $R$-modules, the rank of the range of $f$ plus the rank of the kernel of $f$ equals the rank of $M$, i.e., \[ \text{rank}(\text{range } f) + \text{rank}(\ker f) = \text{rank}(M). \]
LinearMap.lift_rank_eq_of_surjective theorem
{f : M →ₗ[R] M'} (h : Surjective f) : lift.{v} (Module.rank R M) = lift.{u} (Module.rank R M') + lift.{v} (Module.rank R (LinearMap.ker f))
Full source 
theorem LinearMap.lift_rank_eq_of_surjective {f : M →ₗ[R] M'} (h : Surjective f) :
    lift.{v} (Module.rank R M) =
      lift.{u} (Module.rank R M') + lift.{v} (Module.rank R (LinearMap.ker f)) := by
  rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
Rank-Nullity Theorem for Surjective Linear Maps with Universe Lifting: $\text{rank}(M) = \text{rank}(M') + \text{rank}(\ker f)$
Informal description
For any surjective linear map $f \colon M \to M'$ between $R$-modules, the rank of $M$ (lifted to universe $v$) is equal to the sum of the rank of $M'$ (lifted to universe $u$) and the rank of the kernel of $f$ (lifted to universe $v$), i.e., \[ \text{rank}(M) = \text{rank}(M') + \text{rank}(\ker f). \]
LinearMap.rank_eq_of_surjective theorem
{f : M →ₗ[R] M₁} (h : Surjective f) : Module.rank R M = Module.rank R M₁ + Module.rank R (LinearMap.ker f)
Full source 
theorem LinearMap.rank_eq_of_surjective {f : M →ₗ[R] M₁} (h : Surjective f) :
    Module.rank R M = Module.rank R M₁ + Module.rank R (LinearMap.ker f) := by
  rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
Rank-Nullity Theorem for Surjective Linear Maps: $\text{rank}(M) = \text{rank}(M₁) + \text{rank}(\ker f)$
Informal description
For any surjective linear map $f \colon M \to M₁$ between $R$-modules, the rank of $M$ is equal to the sum of the rank of $M₁$ and the rank of the kernel of $f$, i.e., \[ \text{rank}(M) = \text{rank}(M₁) + \text{rank}(\ker f). \]
exists_linearIndepOn_of_lt_rank theorem
[StrongRankCondition R] {s : Set M} (hs : LinearIndepOn R id s) : ∃ t, s ⊆ t ∧ #t = Module.rank R M ∧ LinearIndepOn R id t
Full source 
theorem exists_linearIndepOn_of_lt_rank [StrongRankCondition R]
    {s : Set M} (hs : LinearIndepOn R id s) :
    ∃ t, s ⊆ t ∧ #t = Module.rank R M ∧ LinearIndepOn R id t := by
  obtain ⟨t, ht, ht'⟩ := exists_set_linearIndependent R (M ⧸ Submodule.span R s)
  choose sec hsec using Submodule.mkQ_surjective (Submodule.span R s)
  have hsec' : (Submodule.mkQ _) ∘ sec = _root_.id := funext hsec
  have hst : Disjoint s (sec '' t) := by
    rw [Set.disjoint_iff]
    rintro _ ⟨hxs, ⟨x, hxt, rfl⟩⟩
    apply ht'.ne_zero ⟨x, hxt⟩
    rw [Subtype.coe_mk, ← hsec x,mkQ_apply, Quotient.mk_eq_zero]
    exact Submodule.subset_span hxs
  refine ⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩
  · rw [Cardinal.mk_union_of_disjoint hst, Cardinal.mk_image_eq, ht,
      ← rank_quotient_add_rank (Submodule.span R s), add_comm, rank_span_set hs]
    exact HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩
  · apply LinearIndepOn.union_id_of_quotient Submodule.subset_span hs
    rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,
      ← image_comp, hsec', image_id]
Extension of Linear Independent Set to Basis-Like Set in Modules Satisfying Strong Rank Condition
Informal description
Let $R$ be a ring satisfying the strong rank condition, $M$ an $R$-module, and $s \subseteq M$ a linearly independent subset. Then there exists a subset $t \subseteq M$ such that: 1. $s \subseteq t$, 2. The cardinality of $t$ equals the rank of $M$ as an $R$-module, and 3. $t$ is linearly independent over $R$.
exists_linearIndependent_cons_of_lt_rank theorem
[StrongRankCondition R] {n : ℕ} {v : Fin n → M} (hv : LinearIndependent R v) (h : n < Module.rank R M) : ∃ (x : M), LinearIndependent R (Fin.cons x v)
Full source 
/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
the family by another vector while retaining linear independence. -/
theorem exists_linearIndependent_cons_of_lt_rank [StrongRankCondition R] {n : ℕ} {v : Fin n → M}
    (hv : LinearIndependent R v) (h : n < Module.rank R M) :
    ∃ (x : M), LinearIndependent R (Fin.cons x v) := by
  obtain ⟨t, h₁, h₂, h₃⟩ := exists_linearIndepOn_of_lt_rank hv.linearIndepOn_id
  have : rangerange v ≠ t := by
    refine fun e ↦ h.ne ?_
    rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂
    simpa only [mk_fintype, Fintype.card_fin, lift_natCast, lift_id'] using h₂
  obtain ⟨x, hx, hx'⟩ := nonempty_of_ssubset (h₁.ssubset_of_ne this)
  exact ⟨x, (linearIndepOn_id_range_iff (Fin.cons_injective_iff.mpr ⟨hx', hv.injective⟩)).mp
    (h₃.mono (Fin.range_cons x v ▸ insert_subset hx h₁))⟩
Extension of Linearly Independent Family by One Vector in High-Rank Modules
Informal description
Let $R$ be a ring satisfying the strong rank condition, $M$ an $R$-module, and $v \colon \text{Fin } n \to M$ a linearly independent family of vectors in $M$. If $n < \text{rank}_R M$, then there exists a vector $x \in M$ such that the extended family $\text{Fin.cons } x \ v$ (i.e., $x$ prepended to $v$) is linearly independent over $R$.
exists_linearIndependent_snoc_of_lt_rank theorem
[StrongRankCondition R] {n : ℕ} {v : Fin n → M} (hv : LinearIndependent R v) (h : n < Module.rank R M) : ∃ (x : M), LinearIndependent R (Fin.snoc v x)
Full source 
/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
the family by another vector while retaining linear independence. -/
theorem exists_linearIndependent_snoc_of_lt_rank [StrongRankCondition R] {n : ℕ} {v : Fin n → M}
    (hv : LinearIndependent R v) (h : n < Module.rank R M) :
    ∃ (x : M), LinearIndependent R (Fin.snoc v x) := by
  simp only [Fin.snoc_eq_cons_rotate]
  have ⟨x, hx⟩ := exists_linearIndependent_cons_of_lt_rank hv h
  exact ⟨x, hx.comp _ (finRotate _).injective⟩
Extension of Linearly Independent Family by One Vector (Appended) in High-Rank Modules
Informal description
Let $R$ be a ring satisfying the strong rank condition, $M$ an $R$-module, and $v \colon \text{Fin } n \to M$ a linearly independent family of vectors in $M$. If $n < \text{rank}_R M$, then there exists a vector $x \in M$ such that the extended family $\text{Fin.snoc } v \ x$ (i.e., $x$ appended to $v$) is linearly independent over $R$.
exists_linearIndependent_pair_of_one_lt_rank theorem
[StrongRankCondition R] [NoZeroSMulDivisors R M] (h : 1 < Module.rank R M) {x : M} (hx : x ≠ 0) : ∃ y, LinearIndependent R ![x, y]
Full source 
/-- Given a nonzero vector in a space of dimension `> 1`, one may find another vector linearly
independent of the first one. -/
theorem exists_linearIndependent_pair_of_one_lt_rank [StrongRankCondition R]
    [NoZeroSMulDivisors R M] (h : 1 < Module.rank R M) {x : M} (hx : x ≠ 0) :
    ∃ y, LinearIndependent R ![x, y] := by
  obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (linearIndependent_unique ![x] hx) h
  have : Fin.snoc ![x] y = ![x, y] := by simp [Fin.snoc, ← List.ofFn_inj]
  rw [this] at hy
  exact ⟨y, hy⟩
Existence of Linearly Independent Pair in High-Rank Modules
Informal description
Let $R$ be a ring satisfying the strong rank condition, and let $M$ be an $R$-module with no zero smul divisors. If the rank of $M$ is greater than $1$ and $x \in M$ is a nonzero vector, then there exists a vector $y \in M$ such that the pair $(x, y)$ is linearly independent over $R$.
Submodule.exists_smul_not_mem_of_rank_lt theorem
{N : Submodule R M} (h : Module.rank R N < Module.rank R M) : ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N
Full source 
theorem Submodule.exists_smul_not_mem_of_rank_lt {N : Submodule R M}
    (h : Module.rank R N < Module.rank R M) : ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N := by
  have : Module.rankModule.rank R (M ⧸ N) ≠ 0 := by
    intro e
    rw [← rank_quotient_add_rank N, e, zero_add] at h
    exact h.ne rfl
  rw [ne_eq, rank_eq_zero_iff, (Submodule.Quotient.mk_surjective N).forall] at this
  push_neg at this
  simp_rw [← N.mkQ_apply, ← map_smul, N.mkQ_apply, ne_eq, Submodule.Quotient.mk_eq_zero] at this
  exact this
Existence of Non-Membership Element in Submodule of Lower Rank
Informal description
For any submodule $N$ of an $R$-module $M$ with $\text{rank}(N) < \text{rank}(M)$, there exists an element $m \in M$ such that for all nonzero $r \in R$, the scalar multiple $r \cdot m$ does not belong to $N$.
Submodule.rank_sup_add_rank_inf_eq theorem
(s t : Submodule R M) : Module.rank R (s ⊔ t : Submodule R M) + Module.rank R (s ⊓ t : Submodule R M) = Module.rank R s + Module.rank R t
Full source 
theorem Submodule.rank_sup_add_rank_inf_eq (s t : Submodule R M) :
    Module.rank R (s ⊔ t : Submodule R M) + Module.rank R (s ⊓ t : Submodule R M) =
    Module.rank R s + Module.rank R t := by
  conv_rhs => enter [2]; rw [show t = (s ⊔ t) ⊓ t by simp]
  rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
Rank Additivity Formula for Submodule Supremum and Infimum
Informal description
For any two submodules $s$ and $t$ of an $R$-module $M$, the sum of the ranks of their supremum $s \sqcup t$ and their infimum $s \sqcap t$ equals the sum of their individual ranks, i.e., \[ \text{rank}(s \sqcup t) + \text{rank}(s \sqcap t) = \text{rank}(s) + \text{rank}(t). \]
Submodule.rank_add_le_rank_add_rank theorem
(s t : Submodule R M) : Module.rank R (s ⊔ t : Submodule R M) ≤ Module.rank R s + Module.rank R t
Full source 
theorem Submodule.rank_add_le_rank_add_rank (s t : Submodule R M) :
    Module.rank R (s ⊔ t : Submodule R M) ≤ Module.rank R s + Module.rank R t := by
  rw [← Submodule.rank_sup_add_rank_inf_eq]
  exact self_le_add_right _ _
Subadditivity of Rank for Submodule Supremum
Informal description
For any two submodules $s$ and $t$ of an $R$-module $M$, the rank of their supremum $s \sqcup t$ is less than or equal to the sum of their individual ranks, i.e., \[ \text{rank}(s \sqcup t) \leq \text{rank}(s) + \text{rank}(t). \]
exists_linearIndependent_snoc_of_lt_finrank theorem
{n : ℕ} {v : Fin n → M} (hv : LinearIndependent R v) (h : n < finrank R M) : ∃ (x : M), LinearIndependent R (Fin.snoc v x)
Full source 
/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
theorem exists_linearIndependent_snoc_of_lt_finrank {n : ℕ} {v : Fin n → M}
    (hv : LinearIndependent R v) (h : n < finrank R M) :
    ∃ (x : M), LinearIndependent R (Fin.snoc v x) :=
  exists_linearIndependent_snoc_of_lt_rank hv (lt_rank_of_lt_finrank h)
Extension of Linearly Independent Family by One Vector in Finite-Dimensional Modules (Appended Version)
Informal description
Let $R$ be a ring, $M$ a finite-dimensional $R$-module, and $v \colon \{0,\dots,n-1\} \to M$ a linearly independent family of vectors in $M$. If $n < \operatorname{finrank}_R M$, then there exists a vector $x \in M$ such that the extended family $(v(0),\dots,v(n-1),x)$ is linearly independent over $R$.
exists_linearIndependent_cons_of_lt_finrank theorem
{n : ℕ} {v : Fin n → M} (hv : LinearIndependent R v) (h : n < finrank R M) : ∃ (x : M), LinearIndependent R (Fin.cons x v)
Full source 
/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
theorem exists_linearIndependent_cons_of_lt_finrank {n : ℕ} {v : Fin n → M}
    (hv : LinearIndependent R v) (h : n < finrank R M) :
    ∃ (x : M), LinearIndependent R (Fin.cons x v) :=
  exists_linearIndependent_cons_of_lt_rank hv (lt_rank_of_lt_finrank h)
Extension of Linearly Independent Family by One Vector in Finite-Dimensional Modules
Informal description
Let $R$ be a ring, $M$ a finite-dimensional $R$-module, and $v \colon \text{Fin } n \to M$ a linearly independent family of vectors in $M$. If $n < \operatorname{finrank}_R M$, then there exists a vector $x \in M$ such that the extended family $\text{Fin.cons } x \ v$ (i.e., $x$ prepended to $v$) is linearly independent over $R$.
exists_linearIndependent_pair_of_one_lt_finrank theorem
[NoZeroSMulDivisors R M] (h : 1 < finrank R M) {x : M} (hx : x ≠ 0) : ∃ y, LinearIndependent R ![x, y]
Full source 
/-- Given a nonzero vector in a finite-dimensional space of dimension `> 1`, one may find another
vector linearly independent of the first one. -/
theorem exists_linearIndependent_pair_of_one_lt_finrank [NoZeroSMulDivisors R M]
    (h : 1 < finrank R M) {x : M} (hx : x ≠ 0) :
    ∃ y, LinearIndependent R ![x, y] :=
  exists_linearIndependent_pair_of_one_lt_rank (one_lt_rank_of_one_lt_finrank h) hx
Existence of Linearly Independent Pair in Finite-Dimensional Modules of Dimension > 1
Informal description
Let $R$ be a ring and $M$ a finite-dimensional $R$-module with no zero smul divisors. If the dimension of $M$ is greater than $1$ and $x \in M$ is a nonzero vector, then there exists a vector $y \in M$ such that the pair $(x, y)$ is linearly independent over $R$.
Submodule.finrank_quotient_add_finrank theorem
[Module.Finite R M] (N : Submodule R M) : finrank R (M ⧸ N) + finrank R N = finrank R M
Full source 
/-- Rank-nullity theorem using `finrank`. -/
lemma Submodule.finrank_quotient_add_finrank [Module.Finite R M] (N : Submodule R M) :
    finrank R (M ⧸ N) + finrank R N = finrank R M := by
  rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
    Submodule.finrank_eq_rank]
  exact HasRankNullity.rank_quotient_add_rank _
Rank-Nullity Theorem for Finite-Dimensional Modules
Informal description
Let $R$ be a ring and $M$ a finite-dimensional $R$-module. For any submodule $N$ of $M$, the sum of the dimensions of the quotient module $M/N$ and the submodule $N$ equals the dimension of $M$, i.e., \[ \operatorname{finrank}_R(M/N) + \operatorname{finrank}_R(N) = \operatorname{finrank}_R(M). \]
Submodule.finrank_quotient theorem
[Module.Finite R M] {S : Type*} [Ring S] [SMul R S] [Module S M] [IsScalarTower R S M] (N : Submodule S M) : finrank R (M ⧸ N) = finrank R M - finrank R N
Full source 
/-- Rank-nullity theorem using `finrank` and subtraction. -/
lemma Submodule.finrank_quotient [Module.Finite R M] {S : Type*} [Ring S] [SMul R S] [Module S M]
    [IsScalarTower R S M] (N : Submodule S M) : finrank R (M ⧸ N) = finrank R M - finrank R N := by
  rw [← (N.restrictScalars R).finrank_quotient_add_finrank]
  exact Nat.eq_sub_of_add_eq rfl
Rank-Nullity Theorem for Quotient Modules in Scalar Tower Context
Informal description
Let $R$ be a ring and $M$ a finite-dimensional $R$-module. Suppose $S$ is another ring with a scalar multiplication action on $M$ such that $R$ and $S$ form a scalar tower. For any $S$-submodule $N$ of $M$, the dimension of the quotient module $M/N$ over $R$ is equal to the dimension of $M$ over $R$ minus the dimension of $N$ over $R$, i.e., \[ \operatorname{finrank}_R(M/N) = \operatorname{finrank}_R(M) - \operatorname{finrank}_R(N). \]
Submodule.disjoint_ker_of_finrank_le theorem
[NoZeroSMulDivisors R M] {N : Type*} [AddCommGroup N] [Module R N] {L : Submodule R M} [Module.Finite R L] (f : M →ₗ[R] N) (h : finrank R L ≤ finrank R (L.map f)) : Disjoint L (LinearMap.ker f)
Full source 
lemma Submodule.disjoint_ker_of_finrank_le [NoZeroSMulDivisors R M] {N : Type*} [AddCommGroup N]
    [Module R N] {L : Submodule R M} [Module.Finite R L] (f : M →ₗ[R] N)
    (h : finrank R L ≤ finrank R (L.map f)) :
    Disjoint L (LinearMap.ker f) := by
  refine disjoint_iff.mpr <| LinearMap.injective_domRestrict_iff.mp <| LinearMap.ker_eq_bot.mp <|
    Submodule.rank_eq_zero.mp ?_
  rw [← Submodule.finrank_eq_rank, Nat.cast_eq_zero]
  rw [← LinearMap.range_domRestrict] at h
  have := (LinearMap.ker (f.domRestrict L)).finrank_quotient_add_finrank
  rw [LinearEquiv.finrank_eq (f.domRestrict L).quotKerEquivRange] at this
  omega
Disjointness of Kernel and Submodule under Dimension Constraint
Informal description
Let $R$ be a ring with no zero divisors acting on an $R$-module $M$, and let $N$ be another $R$-module. Consider a finite-dimensional submodule $L$ of $M$ and a linear map $f \colon M \to N$. If the dimension of $L$ is less than or equal to the dimension of the image of $L$ under $f$, then $L$ is disjoint from the kernel of $f$, i.e., $L \cap \ker f = \{0\}$.
Submodule.exists_of_finrank_lt theorem
(N : Submodule R M) (h : finrank R N < finrank R M) : ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N
Full source 
lemma Submodule.exists_of_finrank_lt (N : Submodule R M) (h : finrank R N < finrank R M) :
    ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N := by
  obtain ⟨s, hs, hs'⟩ :=
    exists_finset_linearIndependent_of_le_finrank (R := R) (M := M ⧸ N) le_rfl
  obtain ⟨v, hv⟩ : s.Nonempty := by rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
  obtain ⟨v, rfl⟩ := N.mkQ_surjective v
  refine ⟨v, fun r hr ↦ mt ?_ hr⟩
  have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)
  rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← LinearMap.map_smul,
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
Existence of Non-Scalar Multiple Outside Submodule of Lower Rank
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $N$ a submodule of $M$. If the rank of $N$ is strictly less than the rank of $M$, then there exists an element $m \in M$ such that for all nonzero $r \in R$, the scalar multiple $r \cdot m$ does not belong to $N$.