Documentation

Mathlib.LinearAlgebra.Dimension.RankNullity

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] :

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.

Instances
    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) :
    theorem 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) :
    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 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₁) :

    The rank-nullity theorem

    theorem 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) :
    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 nM} (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 nM} (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 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 0r mN
    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 nM} (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 nM} (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.