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.

class HasRankNullity (R : Type v) [inst : Ring R] : Prop

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.

• exists_set_linearIndependent : ∀ (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M], ∃ (s : Set M), Cardinal.mk ↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val
• rank_quotient_add_rank : ∀ {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M), Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

theorem HasRankNullity.exists_set_linearIndependent {R : Type v} {inst : Ring R} [self : HasRankNullity.{u, v} R] (M : Type u) [AddCommGroup M] [Module R M] : ∃ (s : Set M), Cardinal.mk ↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val

theorem HasRankNullity.rank_quotient_add_rank {R : Type v} {inst : Ring R} [self : HasRankNullity.{u, v} R] {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

theorem Submodule.rank_quotient_add_rank {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] (N : Submodule R M) : Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

theorem exists_set_linearIndependent (R : Type u_1) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] : ∃ (s : Set M), Cardinal.mk ↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val

theorem nontrivial_of_hasRankNullity (R : Type u_1) [Ring R] [HasRankNullity.{u, u_1} R] : Nontrivial R

theorem LinearMap.lift_rank_range_add_rank_ker {R : Type u_1} {M : Type u} {M' : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] [HasRankNullity.{u, u_1} R] (f : M →ₗ[R] M') : Cardinal.lift.{u, v} (Module.rank R ↥(LinearMap.range f)) + Cardinal.lift.{v, u} (Module.rank R ↥(LinearMap.ker f)) = Cardinal.lift.{v, u} (Module.rank R M)

theorem LinearMap.rank_range_add_rank_ker {R : Type u_1} {M : Type u} {M₁ : Type u} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] [HasRankNullity.{u, u_1} R] (f : M →ₗ[R] M₁) : Module.rank R ↥(LinearMap.range f) + Module.rank R ↥(LinearMap.ker f) = Module.rank R M

The rank-nullity theorem

theorem LinearMap.lift_rank_eq_of_surjective {R : Type u_1} {M : Type u} {M' : Type v} [Ring R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] [HasRankNullity.{u, u_1} R] {f : M →ₗ[R] M'} (h : Function.Surjective ⇑f) : Cardinal.lift.{v, u} (Module.rank R M) = Cardinal.lift.{u, v} (Module.rank R M') + Cardinal.lift.{v, u} (Module.rank R ↥(LinearMap.ker f))

theorem LinearMap.rank_eq_of_surjective {R : Type u_1} {M : Type u} {M₁ : Type u} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] [HasRankNullity.{u, u_1} R] {f : M →ₗ[R] M₁} (h : Function.Surjective ⇑f) : Module.rank R M = Module.rank R M₁ + Module.rank R ↥(LinearMap.ker f)

theorem exists_linearIndependent_of_lt_rank {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] {s : Set M} (hs : LinearIndependent (ι := ↑s) R Subtype.val) : ∃ (t : Set M), s ⊆ t ∧ Cardinal.mk ↑t = Module.rank R M ∧ LinearIndependent (ι := ↑t) R Subtype.val

theorem exists_linearIndependent_cons_of_lt_rank {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [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)

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 {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [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)

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_pair_of_one_lt_rank {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [NoZeroSMulDivisors R M] (h : 1 < Module.rank R M) {x : M} (hx : x ≠ 0) : ∃ (y : M), LinearIndependent R ![x, y]

Given a nonzero vector in a space of dimension > 1, one may find another vector linearly independent of the first one.

theorem Submodule.exists_smul_not_mem_of_rank_lt {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] {N : Submodule R M} (h : Module.rank R ↥N < Module.rank R M) : ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N

theorem Submodule.rank_sup_add_rank_inf_eq {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] (s : Submodule R M) (t : Submodule R M) : Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥t

theorem Submodule.rank_add_le_rank_add_rank {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] (s : Submodule R M) (t : Submodule R M) : Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t

theorem exists_linearIndependent_snoc_of_lt_finrank {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] {n : ℕ} {v : Fin n → M} (hv : LinearIndependent R v) (h : n < Module.finrank R M) : ∃ (x : M), LinearIndependent R (Fin.snoc v x)

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 {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] {n : ℕ} {v : Fin n → M} (hv : LinearIndependent R v) (h : n < Module.finrank R M) : ∃ (x : M), LinearIndependent R (Fin.cons x v)

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_pair_of_one_lt_finrank {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [NoZeroSMulDivisors R M] (h : 1 < Module.finrank R M) {x : M} (hx : x ≠ 0) : ∃ (y : M), LinearIndependent R ![x, y]

Given a nonzero vector in a finite-dimensional space of dimension > 1, one may find another vector linearly independent of the first one.

theorem Submodule.finrank_quotient_add_finrank {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M) : Module.finrank R (M ⧸ N) + Module.finrank R ↥N = Module.finrank R M

Rank-nullity theorem using finrank.

theorem Submodule.finrank_quotient {R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_2} R] [StrongRankCondition R] [Module.Finite R M] {S : Type u_1} [Ring S] [SMul R S] [Module S M] [IsScalarTower R S M] (N : Submodule S M) : Module.finrank R (M ⧸ N) = Module.finrank R M - Module.finrank R ↥N

Rank-nullity theorem using finrank and subtraction.

theorem Submodule.exists_of_finrank_lt {R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M) (h : Module.finrank R ↥N < Module.finrank R M) : ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N