Documentation

Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Some results on free modules over rings satisfying strong rank condition #

This file contains some results on free modules over rings satisfying strong rank condition. Most of then are generalized from the same result assuming the base ring being division ring, and are moved from the files Mathlib/LinearAlgebra/Dimension/DivisionRing.lean and Mathlib/LinearAlgebra/FiniteDimensional.lean.

source
noncomputable def Basis.ofRankEqZero {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] {ι : Type u_3} [IsEmpty ι] (hV : Module.rank K V = 0) :
Basis ι K V

The ι indexed basis on V, where ι is an empty type and V is zero-dimensional.

See also FiniteDimensional.finBasis.

Equations
Instances For
    source
    @[simp]
    theorem Basis.ofRankEqZero_apply {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] {ι : Type u_3} [IsEmpty ι] (hV : Module.rank K V = 0) (i : ι) :
    (Basis.ofRankEqZero hV) i = 0
    source
    theorem le_rank_iff_exists_linearIndependent {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] {c : Cardinal.{u_2}} :
    c ≤ Module.rank K V ↔ ∃ (s : Set V), Cardinal.mk ↑s = c ∧ LinearIndependent (ι := { x : V // x ∈ s }) K Subtype.val
    source
    theorem le_rank_iff_exists_linearIndependent_finset {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] {n : ℕ} :
    ↑n ≤ Module.rank K V ↔ ∃ (s : Finset V), s.card = n ∧ LinearIndependent (ι := { x : V // x ∈ ↑s }) K Subtype.val
    source
    theorem rank_le_one_iff {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] :
    Module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v

    A vector space has dimension at most 1 if and only if there is a single vector of which all vectors are multiples.

    source
    theorem rank_eq_one_iff {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] :
    Module.rank K V = 1 ↔ ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v

    A vector space has dimension 1 if and only if there is a single non-zero vector of which all vectors are multiples.

    source
    theorem rank_submodule_le_one_iff {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] (s : Submodule K V) [Module.Free K ↥s] :
    Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ Submodule.span K {v₀}

    A submodule has dimension at most 1 if and only if there is a single vector in the submodule such that the submodule is contained in its span.

    source
    theorem rank_submodule_eq_one_iff {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] (s : Submodule K V) [Module.Free K ↥s] :
    Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ Submodule.span K {v₀}

    A submodule has dimension 1 if and only if there is a single non-zero vector in the submodule such that the submodule is contained in its span.

    source
    theorem rank_submodule_le_one_iff' {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] (s : Submodule K V) [Module.Free K ↥s] :
    Module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ Submodule.span K {v₀}

    A submodule has dimension at most 1 if and only if there is a single vector, not necessarily in the submodule, such that the submodule is contained in its span.

    source
    theorem Submodule.rank_le_one_iff_isPrincipal {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] (W : Submodule K V) [Module.Free K ↥W] :
    Module.rank K ↥W ≤ 1 ↔ W.IsPrincipal
    source
    theorem Module.rank_le_one_iff_top_isPrincipal {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] :
    Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal
    source
    theorem finrank_eq_one_iff {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] (ι : Type u_3) [Unique ι] :
    FiniteDimensional.finrank K V = 1 ↔ Nonempty (Basis ι K V)

    A module has dimension 1 iff there is some v : V so {v} is a basis.

    source
    theorem finrank_eq_one_iff' {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] :
    FiniteDimensional.finrank K V = 1 ↔ ∃ (v : V), v ≠ 0 ∧ ∀ (w : V), ∃ (c : K), c • v = w

    A module has dimension 1 iff there is some nonzero v : V so every vector is a multiple of v.

    source
    theorem finrank_le_one_iff {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
    FiniteDimensional.finrank K V ≤ 1 ↔ ∃ (v : V), ∀ (w : V), ∃ (c : K), c • v = w

    A finite dimensional module has dimension at most 1 iff there is some v : V so every vector is a multiple of v.

    source
    theorem Submodule.finrank_le_one_iff_isPrincipal {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] (W : Submodule K V) [Module.Free K ↥W] [Module.Finite K ↥W] :
    FiniteDimensional.finrank K ↥W ≤ 1 ↔ W.IsPrincipal
    source
    theorem Module.finrank_le_one_iff_top_isPrincipal {K : Type u_1} {V : Type u_2} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
    FiniteDimensional.finrank K V ≤ 1 ↔ ⊤.IsPrincipal
    source
    theorem cardinal_mk_eq_cardinal_mk_field_pow_rank (K : Type u) (V : Type u) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
    Cardinal.mk V = Cardinal.mk K ^ Module.rank K V
    source
    theorem cardinal_lt_aleph0_of_finiteDimensional (K : Type u) (V : Type u) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Finite K] [Module.Free K V] [Module.Finite K V] :
    Cardinal.mk V < Cardinal.aleph0