Documentation

Mathlib.LinearAlgebra.Dimension.Finite

Conditions for rank to be finite #

Also contains characterization for when rank equals zero or rank equals one.

theorem rank_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : } (H : ∀ (s : Finset M), (LinearIndependent R fun (i : { x : M // x s }) => i)s.card n) :
Module.rank R M n
theorem rank_eq_zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :
Module.rank R M = 0 ∀ (x : M), ∃ (a : R), a 0 a x = 0

See rank_zero_iff for a stronger version with NoZeroSMulDivisor R M.

theorem rank_zero_iff_forall_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] :
Module.rank R M = 0 ∀ (x : M), x = 0
theorem rank_zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] :

See rank_subsingleton for the reason that Nontrivial R is needed. Also see rank_eq_zero_iff for the version without NoZeroSMulDivisor R M.

theorem rank_pos_iff_exists_ne_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] :
0 < Module.rank R M ∃ (x : M), x 0
theorem rank_pos {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] [Nontrivial M] :
theorem rank_subsingleton' (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [Subsingleton M] :

See rank_subsingleton that assumes Subsingleton R instead.

@[simp]
@[simp]
theorem rank_bot (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] :
theorem exists_mem_ne_zero_of_rank_pos {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] {s : Submodule R M} (h : 0 < Module.rank R s) :
bs, b 0
theorem Module.finite_of_rank_eq_nat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] {n : } (h : Module.rank R M = n) :
theorem Module.finite_of_rank_eq_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : Module.rank R M = 1) :

If a module has a finite dimension, all bases are indexed by a finite type.

noncomputable def Basis.fintypeIndexOfRankLtAleph0 {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} (b : Basis ι R M) (h : Module.rank R M < Cardinal.aleph0) :

If a module has a finite dimension, all bases are indexed by a finite type.

Equations
Instances For
    theorem Basis.finite_index_of_rank_lt_aleph0 {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_1} {s : Set ι} (b : Basis (s) R M) (h : Module.rank R M < Cardinal.aleph0) :
    s.Finite

    If a module has a finite dimension, all bases are indexed by a finite set.

    theorem LinearIndependent.finset_card_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {b : Finset M} (h : LinearIndependent R fun (x : { x : M // x b }) => x) :
    theorem LinearIndependent.finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type u_1} {f : ιM} (h : LinearIndependent R f) :
    theorem LinearIndependent.setFinite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {b : Set M} (h : LinearIndependent R fun (x : b) => x) :
    b.Finite
    @[deprecated LinearIndependent.cardinal_mk_le_finrank]

    Alias of LinearIndependent.cardinal_mk_le_finrank.

    @[deprecated LinearIndependent.fintype_card_le_finrank]

    Alias of LinearIndependent.fintype_card_le_finrank.

    @[deprecated LinearIndependent.finset_card_le_finrank]
    theorem finset_card_le_finrank_of_linearIndependent {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {b : Finset M} (h : LinearIndependent R fun (x : { x : M // x b }) => x) :

    Alias of LinearIndependent.finset_card_le_finrank.

    @[deprecated LinearIndependent.lt_aleph0_of_finite]

    Alias of LinearIndependent.lt_aleph0_of_finite.

    theorem exists_set_linearIndependent_of_lt_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : Cardinal.{v}} (hn : n < Module.rank R M) :
    ∃ (s : Set M), Cardinal.mk s = n LinearIndependent (ι := { x : M // x s }) R Subtype.val
    theorem exists_finset_linearIndependent_of_le_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : } (hn : n Module.rank R M) :
    ∃ (s : Finset M), s.card = n LinearIndependent R Subtype.val
    theorem exists_linearIndependent_of_le_rank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : } (hn : n Module.rank R M) :
    ∃ (f : Fin nM), LinearIndependent R f
    theorem natCast_le_rank_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {n : } :
    n Module.rank R M ∃ (f : Fin nM), LinearIndependent R f
    theorem natCast_le_rank_iff_finset {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {n : } :
    n Module.rank R M ∃ (s : Finset M), s.card = n LinearIndependent R Subtype.val
    theorem exists_finset_linearIndependent_of_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : } (hn : n FiniteDimensional.finrank R M) :
    ∃ (s : Finset M), s.card = n LinearIndependent R Subtype.val
    theorem exists_linearIndependent_of_le_finrank {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {n : } (hn : n FiniteDimensional.finrank R M) :
    ∃ (f : Fin nM), LinearIndependent R f
    noncomputable def CompleteLattice.Independent.fintypeNeBotOfFiniteDimensional {R : Type u} {M : Type v} {ι : Type w} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [NoZeroSMulDivisors R M] {p : ιSubmodule R M} (hp : CompleteLattice.Independent p) :
    Fintype { i : ι // p i }

    If p is an independent family of submodules of a R-finite module M, then the number of nontrivial subspaces in the family p is finite.

    Equations
    • hp.fintypeNeBotOfFiniteDimensional = let_fun this := ; .some
    Instances For

      If p is an independent family of submodules of a R-finite module M, then the number of nontrivial subspaces in the family p is bounded above by the dimension of M.

      Note that the Fintype hypothesis required here can be provided by CompleteLattice.Independent.fintypeNeBotOfFiniteDimensional.

      theorem Module.exists_nontrivial_relation_of_finrank_lt_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {t : Finset M} (h : FiniteDimensional.finrank R M < t.card) :
      ∃ (f : MR), et, f e e = 0 xt, f x 0

      If a finset has cardinality larger than the rank of a module, then there is a nontrivial linear relation amongst its elements.

      theorem Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {t : Finset M} (h : FiniteDimensional.finrank R M + 1 < t.card) :
      ∃ (f : MR), et, f e e = 0 et, f e = 0 xt, f x 0

      If a finset has cardinality larger than finrank + 1, then there is a nontrivial linear relation amongst its elements, such that the coefficients of the relation sum to zero.

      A finite dimensional space is nontrivial if it has positive finrank.

      A finite dimensional space is nontrivial if it has finrank equal to the successor of a natural number.

      A (finite dimensional) space that is a subsingleton has zero finrank.

      theorem LinearIndependent.finrank_eq_zero_of_infinite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_1} [Nontrivial R] [Infinite ι] {v : ιM} (hv : LinearIndependent R v) :
      @[simp]
      theorem finrank_bot (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] :

      A finite rank torsion-free module has positive finrank iff it has a nonzero element.

      An R-finite torsion-free module has positive finrank iff it is nontrivial.

      A nontrivial finite dimensional space has positive finrank.

      theorem FiniteDimensional.finrank_eq_zero_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] :
      FiniteDimensional.finrank R M = 0 ∀ (x : M), ∃ (a : R), a 0 a x = 0

      See FiniteDimensional.finrank_zero_iff for the stronger version with NoZeroSMulDivisors R M.

      The StrongRankCondition is automatic. See commRing_strongRankCondition.

      A finite dimensional space has zero finrank iff it is a subsingleton. This is the finrank version of rank_zero_iff.

      @[simp]
      theorem Submodule.rank_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M] {S : Submodule R M} :
      Module.rank R S = 0 S =

      See rank_subsingleton for the reason that Nontrivial R is needed.

      theorem finrank_eq_zero_of_basis_imp_not_finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ∀ (s : Set M), Basis (s) R M¬s.Finite) :
      theorem finrank_eq_zero_of_basis_imp_false {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ∀ (s : Finset M), Basis (s) R MFalse) :
      theorem finrank_eq_zero_of_not_exists_basis {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ¬∃ (s : Finset M), Nonempty (Basis (s) R M)) :
      theorem finrank_eq_zero_of_not_exists_basis_finite {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ¬∃ (s : Set M) (x : Basis (s) R M), s.Finite) :
      theorem finrank_eq_zero_of_not_exists_basis_finset {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ¬∃ (s : Finset M), Nonempty (Basis { x : M // x s } R M)) :
      theorem rank_eq_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [StrongRankCondition R] (v : M) (n : v 0) (h : ∀ (w : M), ∃ (c : R), c v = w) :

      If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.

      theorem finrank_eq_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [StrongRankCondition R] (v : M) (n : v 0) (h : ∀ (w : M), ∃ (c : R), c v = w) :

      If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.

      theorem finrank_le_one {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [StrongRankCondition R] (v : M) (h : ∀ (w : M), ∃ (c : R), c v = w) :

      If every vector is a multiple of some v : M, then M has dimension at most one.