# 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 them 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} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] {ι : Type u_1} [IsEmpty ι] (hV : Module.rank K V = 0) :
Module.Basis ι K V

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

See also `Module.finBasis`.

Equations

- Basis.ofRankEqZero hV = Module.Basis.empty V

Instances For

source
@[simp]
theorem Basis.ofRankEqZero_apply {K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] {ι : Type u_1} [IsEmpty ι] (hV : Module.rank K V = 0) (i : ι) :
(ofRankEqZero hV) i = 0
source
theorem le_rank_iff_exists_linearIndependent {K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] {c : Cardinal.{v}} :
c ≤ Module.rank K V ↔ ∃ (s : Set V), Cardinal.mk ↑s = c ∧ LinearIndepOn K id s
source
theorem le_rank_iff_exists_linearIndependent_finset {K : Type u} {V : Type v} [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 K Subtype.val
source
theorem rank_le_one_iff {K : Type u} {V : Type v} [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} {V : Type v} [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} {V : Type v} [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} {V : Type v} [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} {V : Type v} [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} {V : Type v} [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} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Free K V] :
Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal
source
theorem finrank_eq_one_iff {K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] (ι : Type u_1) [Unique ι] :
Module.finrank K V = 1 ↔ Nonempty (Module.Basis ι K V)

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

See also `Module.Basis.nonempty_unique_index_of_finrank_eq_one`

source
theorem finrank_eq_one_iff' {K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] :
Module.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} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
Module.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} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] (W : Submodule K V) [Module.Free K ↥W] [Module.Finite K ↥W] :
Module.finrank K ↥W ≤ 1 ↔ W.IsPrincipal
source
theorem Module.finrank_le_one_iff_top_isPrincipal {K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Free K V] [Module.Finite K V] :
finrank K V ≤ 1 ↔ ⊤.IsPrincipal
source
theorem lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank (K : Type u) (V : Type v) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] :
Cardinal.lift.{u, v} (Cardinal.mk V) = Cardinal.lift.{v, u} (Cardinal.mk K) ^ Cardinal.lift.{u, v} (Module.rank K V)
source
theorem cardinalMk_eq_cardinalMk_field_pow_rank (K 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 v) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Finite K] [Module.Free K V] [Module.Finite K V] :
Cardinal.mk V < Cardinal.aleph0
source
theorem Subalgebra.eq_bot_of_rank_le_one {F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] {S : Subalgebra F E} (h : Module.rank F ↥S ≤ 1) [Module.Free F ↥S] :
S = ⊥
source
theorem Subalgebra.eq_bot_of_finrank_one {F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] {S : Subalgebra F E} (h : Module.finrank F ↥S = 1) [Module.Free F ↥S] :
S = ⊥
source
@[simp]
theorem Subalgebra.rank_eq_one_iff {F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] {S : Subalgebra F E} [Nontrivial E] [Module.Free F ↥S] :
Module.rank F ↥S = 1 ↔ S = ⊥
source
@[simp]
theorem Subalgebra.finrank_eq_one_iff {F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] {S : Subalgebra F E} [Nontrivial E] [Module.Free F ↥S] :
Module.finrank F ↥S = 1 ↔ S = ⊥
source
theorem Subalgebra.bot_eq_top_iff_rank_eq_one {F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] [Nontrivial E] [Module.Free F E] :
⊥ = ⊤ ↔ Module.rank F E = 1
source
theorem Subalgebra.bot_eq_top_iff_finrank_eq_one {F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] [Nontrivial E] [Module.Free F E] :
⊥ = ⊤ ↔ Module.finrank F E = 1
source
@[simp]
theorem Subalgebra.bot_eq_top_of_rank_eq_one {F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] [Nontrivial E] [Module.Free F E] :
Module.rank F E = 1 → ⊥ = ⊤

Alias of the reverse direction of `Subalgebra.bot_eq_top_iff_rank_eq_one`.

source
@[simp]
theorem Subalgebra.bot_eq_top_of_finrank_eq_one {F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] [Nontrivial E] [Module.Free F E] :
Module.finrank F E = 1 → ⊥ = ⊤

Alias of the reverse direction of `Subalgebra.bot_eq_top_iff_finrank_eq_one`.