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.

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