Bases of modules and the Orzech property

It is shown in this file that any spanning set of a module over a ring satisfying the Orzech property of cardinality not exceeding the rank of the module must be linearly independent, and therefore is a basis.

theorem linearIndependent_of_top_le_span_of_card_le_finrank {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [Fintype ι] {b : ι → M} (spans : ⊤ ≤ Submodule.span R (Set.range b)) (card_le : Fintype.card ι ≤ Module.finrank R M) : LinearIndependent R b

theorem linearIndependent_of_top_le_span_of_card_eq_finrank {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [Fintype ι] {b : ι → M} (spans : ⊤ ≤ Submodule.span R (Set.range b)) (card_eq : Fintype.card ι = Module.finrank R M) : LinearIndependent R b

theorem linearIndependent_iff_card_eq_finrank_span {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] [Nontrivial R] {ι : Type u_3} [Fintype ι] {b : ι → M} : LinearIndependent R b ↔ Fintype.card ι = Set.finrank R (Set.range b)

A finite family of vectors is linearly independent if and only if its cardinality equals the dimension of its span.

theorem linearIndependent_iff_card_le_finrank_span {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] [Nontrivial R] {ι : Type u_3} [Fintype ι] {b : ι → M} : LinearIndependent R b ↔ Fintype.card ι ≤ Set.finrank R (Set.range b)

noncomputable def basisOfTopLeSpanOfCardEqFinrank {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [Fintype ι] (b : ι → M) (le_span : ⊤ ≤ Submodule.span R (Set.range b)) (card_eq : Fintype.card ι = Module.finrank R M) : Module.Basis ι R M

A family of finrank R M vectors forms a basis if they span the whole space, provided R satisfies the Orzech property.

@[simp]

theorem coe_basisOfTopLeSpanOfCardEqFinrank {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [Fintype ι] (b : ι → M) (le_span : ⊤ ≤ Submodule.span R (Set.range b)) (card_eq : Fintype.card ι = Module.finrank R M) : ⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b

noncomputable def finsetBasisOfTopLeSpanOfCardEqFinrank {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {s : Finset M} (le_span : ⊤ ≤ Submodule.span R ↑s) (card_eq : s.card = Module.finrank R M) : Module.Basis { x : M // x ∈ s } R M

A finset of finrank R M vectors forms a basis if they span the whole space, provided R satisfies the Orzech property.

@[simp]

theorem finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {s : Finset M} (le_span : ⊤ ≤ Submodule.span R ↑s) (card_eq : s.card = Module.finrank R M) (a✝ : M) : (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a✝ = ⋯.repr ((LinearMap.codRestrict (Submodule.span R (Set.range Subtype.val)) LinearMap.id ⋯) a✝)

noncomputable def setBasisOfTopLeSpanOfCardEqFinrank {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {s : Set M} [Fintype ↑s] (le_span : ⊤ ≤ Submodule.span R s) (card_eq : s.toFinset.card = Module.finrank R M) : Module.Basis (↑s) R M

A set of finrank R M vectors forms a basis if they span the whole space, provided R satisfies the Orzech property.

@[simp]

theorem setBasisOfTopLeSpanOfCardEqFinrank_repr_apply {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {s : Set M} [Fintype ↑s] (le_span : ⊤ ≤ Submodule.span R s) (card_eq : s.toFinset.card = Module.finrank R M) (a✝ : M) : (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a✝ = ⋯.repr ((LinearMap.codRestrict (Submodule.span R (Set.range Subtype.val)) LinearMap.id ⋯) a✝)