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 them are generalized from the same result assuming the base ring being a division ring, and are moved from the files Mathlib/LinearAlgebra/Dimension/DivisionRing.lean and Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean.

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

@[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

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

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

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.

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.

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 ≤ 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.

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 ≤ 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.

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 ≤ 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.

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

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

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

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.

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.

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

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

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)

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

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

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

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

@[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 = ⊥

@[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 = ⊥

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

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

@[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.

@[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.