Finite dimensional vector spaces

Definition and basic properties of finite dimensional vector spaces, of their dimensions, and of linear maps on such spaces.

Main definitions

Assume V is a vector space over a division ring K. There are (at least) three equivalent definitions of finite-dimensionality of V:

• it admits a finite basis.
• it is finitely generated.
• it is noetherian, i.e., every subspace is finitely generated.

We introduce a typeclass FiniteDimensional K V capturing this property. For ease of transfer of proof, it is defined using the second point of view, i.e., as Finite. However, we prove that all these points of view are equivalent, with the following lemmas (in the namespace FiniteDimensional):

• fintypeBasisIndex states that a finite-dimensional vector space has a finite basis
• FiniteDimensional.finBasis and FiniteDimensional.finBasisOfFinrankEq are bases for finite dimensional vector spaces, where the index type is Fin
• of_fintype_basis states that the existence of a basis indexed by a finite type implies finite-dimensionality
• of_finite_basis states that the existence of a basis indexed by a finite set implies finite-dimensionality
• IsNoetherian.iff_fg states that the space is finite-dimensional if and only if it is noetherian

We make use of finrank, the dimension of a finite dimensional space, returning a Nat, as opposed to Module.rank, which returns a Cardinal. When the space has infinite dimension, its finrank is by convention set to 0. finrank is not defined using FiniteDimensional. For basic results that do not need the FiniteDimensional class, import Mathlib.LinearAlgebra.Finrank.

Preservation of finite-dimensionality and formulas for the dimension are given for

• submodules
• quotients (for the dimension of a quotient, see finrank_quotient_add_finrank)
• linear equivs, in LinearEquiv.finiteDimensional
• image under a linear map (the rank-nullity formula is in finrank_range_add_finrank_ker)

Basic properties of linear maps of a finite-dimensional vector space are given. Notably, the equivalence of injectivity and surjectivity is proved in LinearMap.injective_iff_surjective, and the equivalence between left-inverse and right-inverse in LinearMap.mul_eq_one_comm and LinearMap.comp_eq_id_comm.

Implementation notes

Most results are deduced from the corresponding results for the general dimension (as a cardinal), in Mathlib.LinearAlgebra.Dimension. Not all results have been ported yet.

You should not assume that there has been any effort to state lemmas as generally as possible.

One of the characterizations of finite-dimensionality is in terms of finite generation. This property is currently defined only for submodules, so we express it through the fact that the maximal submodule (which, as a set, coincides with the whole space) is finitely generated. This is not very convenient to use, although there are some helper functions. However, this becomes very convenient when speaking of submodules which are finite-dimensional, as this notion coincides with the fact that the submodule is finitely generated (as a submodule of the whole space). This equivalence is proved in Submodule.fg_iff_finiteDimensional.

@[reducible]

def FiniteDimensional (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop

FiniteDimensional vector spaces are defined to be finite modules. Use FiniteDimensional.of_fintype_basis to prove finite dimension from another definition.

Equations

• FiniteDimensional K V = Module.Finite K V

theorem FiniteDimensional.of_injective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (w : Function.Injective ↑f) [FiniteDimensional K V₂] : FiniteDimensional K V

If the codomain of an injective linear map is finite dimensional, the domain must be as well.

theorem FiniteDimensional.of_surjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (w : Function.Surjective ↑f) [FiniteDimensional K V] : FiniteDimensional K V₂

If the domain of a surjective linear map is finite dimensional, the codomain must be as well.

instance FiniteDimensional.finiteDimensional_pi (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] : FiniteDimensional K (ι → K)

Equations

• FiniteDimensional.finiteDimensional_pi = FiniteDimensional.finiteDimensional_pi.proof_1

instance FiniteDimensional.finiteDimensional_pi' (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] (M : ι → Type u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module K (M i)] [I : ∀ (i : ι), FiniteDimensional K (M i)] : FiniteDimensional K ((i : ι) → M i)

Equations

• FiniteDimensional.finiteDimensional_pi' = FiniteDimensional.finiteDimensional_pi'.proof_1

noncomputable def FiniteDimensional.fintypeOfFintype (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [Fintype K] [FiniteDimensional K V] : Fintype V

A finite dimensional vector space over a finite field is finite

Equations

• FiniteDimensional.fintypeOfFintype K V = Module.fintypeOfFintype (IsNoetherian.finsetBasis K V)

theorem FiniteDimensional.finite_of_finite (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [Finite K] [FiniteDimensional K V] : Finite V

theorem FiniteDimensional.of_fintype_basis {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} [Finite ι] (h : Basis ι K V) : FiniteDimensional K V

If a vector space has a finite basis, then it is finite-dimensional.

noncomputable def FiniteDimensional.fintypeBasisIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [FiniteDimensional K V] (b : Basis ι K V) : Fintype ι

If a vector space is FiniteDimensional, all bases are indexed by a finite type

Equations

• FiniteDimensional.fintypeBasisIndex b = IsNoetherian.fintypeBasisIndex b

noncomputable instance FiniteDimensional.instFintypeElemOfVectorSpaceIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Fintype ↑(Basis.ofVectorSpaceIndex K V)

If a vector space is FiniteDimensional, Basis.ofVectorSpace is indexed by a finite type.

Equations

• FiniteDimensional.instFintypeElemOfVectorSpaceIndex = inferInstance

theorem FiniteDimensional.of_finite_basis {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} {s : Set ι} (h : Basis (↑s) K V) (hs : Set.Finite s) : FiniteDimensional K V

If a vector space has a basis indexed by elements of a finite set, then it is finite-dimensional.

instance FiniteDimensional.finiteDimensional_submodule {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K { x // x ∈ S }

A subspace of a finite-dimensional space is also finite-dimensional.

Equations

• @FiniteDimensional.finiteDimensional_submodule = @FiniteDimensional.finiteDimensional_submodule.proof_1

instance FiniteDimensional.finiteDimensional_quotient {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K (V ⧸ S)

A quotient of a finite-dimensional space is also finite-dimensional.

Equations

• @FiniteDimensional.finiteDimensional_quotient = @FiniteDimensional.finiteDimensional_quotient.proof_1

theorem FiniteDimensional.finrank_eq_rank' (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : ↑(FiniteDimensional.finrank K V) = Module.rank K V

In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its finrank. This is a copy of finrank_eq_rank _ _ which creates easier typeclass searches.

theorem FiniteDimensional.finrank_of_infinite_dimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : ¬FiniteDimensional K V) : FiniteDimensional.finrank K V = 0

theorem FiniteDimensional.finiteDimensional_of_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : 0 < FiniteDimensional.finrank K V) : FiniteDimensional K V

theorem FiniteDimensional.finiteDimensional_of_finrank_eq_succ {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (hn : FiniteDimensional.finrank K V = Nat.succ n) : FiniteDimensional K V

theorem FiniteDimensional.fact_finiteDimensional_of_finrank_eq_succ {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (n : ℕ) [Fact (FiniteDimensional.finrank K V = n + 1)] : FiniteDimensional K V

We can infer FiniteDimensional K V in the presence of [Fact (finrank K V = n + 1)]. Declare this as a local instance where needed.

theorem FiniteDimensional.finiteDimensional_iff_of_rank_eq_nsmul {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {W : Type v} [AddCommGroup W] [Module K W] {n : ℕ} (hn : n ≠ 0) (hVW : Module.rank K V = n • Module.rank K W) : FiniteDimensional K V ↔ FiniteDimensional K W

theorem FiniteDimensional.finrank_eq_card_basis' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type w} (h : Basis ι K V) : ↑(FiniteDimensional.finrank K V) = Cardinal.mk ι

If a vector space is finite-dimensional, then the cardinality of any basis is equal to its finrank.

noncomputable def Basis.unique {K : Type u} [DivisionRing K] {ι : Type u_1} (b : Basis ι K K) : Unique ι

Given a basis of a division ring over itself indexed by a type ι, then ι is Unique.

Equations

• Basis.unique b = let_fun A := (_ : Cardinal.mk ι = ↑(FiniteDimensional.finrank K K)); Nonempty.some (_ : Nonempty (Unique ι))

noncomputable def FiniteDimensional.finBasis (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Basis (Fin (FiniteDimensional.finrank K V)) K V

A finite dimensional vector space has a basis indexed by Fin (finrank K V).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FiniteDimensional.finBasisOfFinrankEq (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {n : ℕ} (hn : FiniteDimensional.finrank K V = n) : Basis (Fin n) K V

An n-dimensional vector space has a basis indexed by Fin n.

Equations

• FiniteDimensional.finBasisOfFinrankEq K V hn = Basis.reindex (FiniteDimensional.finBasis K V) (Fin.castIso hn).toEquiv

noncomputable def FiniteDimensional.basisUnique {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : FiniteDimensional.finrank K V = 1) : Basis ι K V

A module with dimension 1 has a basis with one element.

Equations

• FiniteDimensional.basisUnique ι h = Basis.reindex (FiniteDimensional.finBasisOfFinrankEq K V h) (Equiv.equivOfUnique (Fin 1) ι)

@[simp]

theorem FiniteDimensional.basisUnique.repr_eq_zero_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Unique ι] {h : FiniteDimensional.finrank K V = 1} {v : V} {i : ι} : ↑(↑(FiniteDimensional.basisUnique ι h).repr v) i = 0 ↔ v = 0

theorem FiniteDimensional.cardinal_mk_le_finrank_of_linearIndependent {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type w} {b : ι → V} (h : LinearIndependent K b) : Cardinal.mk ι ≤ ↑(FiniteDimensional.finrank K V)

theorem FiniteDimensional.fintype_card_le_finrank_of_linearIndependent {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} [Fintype ι] {b : ι → V} (h : LinearIndependent K b) : Fintype.card ι ≤ FiniteDimensional.finrank K V

theorem FiniteDimensional.finset_card_le_finrank_of_linearIndependent {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {b : Finset V} (h : LinearIndependent K fun x => ↑x) : Finset.card b ≤ FiniteDimensional.finrank K V

theorem FiniteDimensional.lt_aleph0_of_linearIndependent {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} [FiniteDimensional K V] {v : ι → V} (h : LinearIndependent K v) : Cardinal.mk ι < Cardinal.aleph0

theorem LinearIndependent.finite {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {b : Set V} (h : LinearIndependent K fun x => ↑x) : Set.Finite b

theorem FiniteDimensional.not_linearIndependent_of_infinite {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} [inf : Infinite ι] [FiniteDimensional K V] (v : ι → V) : ¬LinearIndependent K v

theorem FiniteDimensional.finrank_pos_iff_exists_ne_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : 0 < FiniteDimensional.finrank K V ↔ ∃ x, x ≠ 0

A finite dimensional space has positive finrank iff it has a nonzero element.

theorem FiniteDimensional.finrank_pos_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : 0 < FiniteDimensional.finrank K V ↔ Nontrivial V

A finite dimensional space has positive finrank iff it is nontrivial.

theorem FiniteDimensional.finrank_pos {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [h : Nontrivial V] : 0 < FiniteDimensional.finrank K V

A nontrivial finite dimensional space has positive finrank.

theorem FiniteDimensional.finrank_zero_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : FiniteDimensional.finrank K V = 0 ↔ Subsingleton V

A finite dimensional space has zero finrank iff it is a subsingleton. This is the finrank version of rank_zero_iff.

theorem Submodule.eq_top_of_finrank_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {S : Submodule K V} (h : FiniteDimensional.finrank K { x // x ∈ S } = FiniteDimensional.finrank K V) : S = ⊤

If a submodule has maximal dimension in a finite dimensional space, then it is equal to the whole space.

instance FiniteDimensional.finiteDimensional_self (K : Type u) [DivisionRing K] : FiniteDimensional K K

Equations

• FiniteDimensional.finiteDimensional_self = FiniteDimensional.finiteDimensional_self.proof_1

theorem FiniteDimensional.span_of_finite (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {A : Set V} (hA : Set.Finite A) : FiniteDimensional K { x // x ∈ Submodule.span K A }

The submodule generated by a finite set is finite-dimensional.

instance FiniteDimensional.span_singleton (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (x : V) : FiniteDimensional K { x // x ∈ Submodule.span K {x} }

The submodule generated by a single element is finite-dimensional.

Equations

• FiniteDimensional.span_singleton = FiniteDimensional.span_singleton.proof_1

instance FiniteDimensional.span_finset (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Finset V) : FiniteDimensional K { x // x ∈ Submodule.span K ↑s }

The submodule generated by a finset is finite-dimensional.

Equations

• FiniteDimensional.span_finset = FiniteDimensional.span_finset.proof_1

instance FiniteDimensional.instFiniteDimensionalSubtypeMemSubmoduleToSemiringToDivisionSemiringToAddCommMonoidInstMembershipSetLikeMapToAddCommMonoidIdToNonAssocSemiringIdsLinearMapSemilinearMapClassAddCommGroupToRingModule (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) [FiniteDimensional K { x // x ∈ p }] : FiniteDimensional K { x // x ∈ Submodule.map f p }

Pushforwards of finite-dimensional submodules are finite-dimensional.

Equations

• One or more equations did not get rendered due to their size.

theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank_aux {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type w} {p : ι → Submodule K V} (hp : CompleteLattice.Independent p) : Cardinal.mk { i // p i ≠ ⊥ } ≤ ↑(FiniteDimensional.finrank K V)

noncomputable def CompleteLattice.Independent.fintypeNeBotOfFiniteDimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type w} {p : ι → Submodule K V} (hp : CompleteLattice.Independent p) : Fintype { i // p i ≠ ⊥ }

If p is an independent family of subspaces of a finite-dimensional space V, then the number of nontrivial subspaces in the family p is finite.

Equations

• CompleteLattice.Independent.fintypeNeBotOfFiniteDimensional hp = let_fun this := (_ : Cardinal.mk { i // p i ≠ ⊥ } < Cardinal.aleph0); Nonempty.some (_ : Nonempty (Fintype { i // p i ≠ ⊥ }))

theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type w} {p : ι → Submodule K V} (hp : CompleteLattice.Independent p) [Fintype { i // p i ≠ ⊥ }] : Fintype.card { i // p i ≠ ⊥ } ≤ FiniteDimensional.finrank K V

If p is an independent family of subspaces of a finite-dimensional space V, then the number of nontrivial subspaces in the family p is bounded above by the dimension of V.

Note that the Fintype hypothesis required here can be provided by CompleteLattice.Independent.fintypeNeBotOfFiniteDimensional.

theorem FiniteDimensional.exists_nontrivial_relation_of_rank_lt_card {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {t : Finset V} (h : FiniteDimensional.finrank K V < Finset.card t) : ∃ f, (Finset.sum t fun e => f e • e) = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0

If a finset has cardinality larger than the dimension of the space, then there is a nontrivial linear relation amongst its elements.

theorem FiniteDimensional.exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {t : Finset V} (h : FiniteDimensional.finrank K V + 1 < Finset.card t) : ∃ f, (Finset.sum t fun e => f e • e) = 0 ∧ (Finset.sum t fun e => f e) = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0

If a finset has cardinality larger than finrank + 1, then there is a nontrivial linear relation amongst its elements, such that the coefficients of the relation sum to zero.

theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_rank_succ_lt_card {L : Type u_1} [LinearOrderedField L] {W : Type v} [AddCommGroup W] [Module L W] [FiniteDimensional L W] {t : Finset W} (h : FiniteDimensional.finrank L W + 1 < Finset.card t) : ∃ f, (Finset.sum t fun e => f e • e) = 0 ∧ (Finset.sum t fun e => f e) = 0 ∧ ∃ x, x ∈ t ∧ 0 < f x

A slight strengthening of exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card available when working over an ordered field: we can ensure a positive coefficient, not just a nonzero coefficient.

@[simp]

theorem FiniteDimensional.basisSingleton_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : FiniteDimensional.finrank K V = 1) (v : V) (hv : v ≠ 0) (w : V) : ↑(FiniteDimensional.basisSingleton ι h v hv).repr w = fun₀ | default => ↑(↑(FiniteDimensional.basisUnique ι h).repr w) default / ↑(↑(FiniteDimensional.basisUnique ι h).repr v) default

noncomputable def FiniteDimensional.basisSingleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : FiniteDimensional.finrank K V = 1) (v : V) (hv : v ≠ 0) : Basis ι K V

In a vector space with dimension 1, each set {v} is a basis for v ≠ 0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FiniteDimensional.basisSingleton_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : FiniteDimensional.finrank K V = 1) (v : V) (hv : v ≠ 0) (i : ι) : ↑(FiniteDimensional.basisSingleton ι h v hv) i = v

@[simp]

theorem FiniteDimensional.range_basisSingleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : FiniteDimensional.finrank K V = 1) (v : V) (hv : v ≠ 0) : Set.range ↑(FiniteDimensional.basisSingleton ι h v hv) = {v}

theorem finiteDimensional_of_rank_eq_nat {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (h : Module.rank K V = ↑n) : FiniteDimensional K V

theorem finiteDimensional_of_rank_eq_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V = 0) : FiniteDimensional K V

theorem finiteDimensional_of_rank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V = 1) : FiniteDimensional K V

theorem finrank_eq_zero_of_rank_eq_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (h : Module.rank K V = 0) : FiniteDimensional.finrank K V = 0

instance finiteDimensional_bot (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] : FiniteDimensional K { x // x ∈ ⊥ }

Equations

• finiteDimensional_bot = finiteDimensional_bot.proof_1

theorem bot_eq_top_of_rank_eq_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V = 0) : ⊥ = ⊤

@[simp]

theorem rank_eq_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S : Submodule K V} : Module.rank K { x // x ∈ S } = 0 ↔ S = ⊥

@[simp]

theorem finrank_eq_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S : Submodule K V} [FiniteDimensional K { x // x ∈ S }] : FiniteDimensional.finrank K { x // x ∈ S } = 0 ↔ S = ⊥

theorem Submodule.fg_iff_finiteDimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) : Submodule.FG s ↔ FiniteDimensional K { x // x ∈ s }

A submodule is finitely generated if and only if it is finite-dimensional

theorem Submodule.finiteDimensional_of_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ : Submodule K V} {S₂ : Submodule K V} [FiniteDimensional K { x // x ∈ S₂ }] (h : S₁ ≤ S₂) : FiniteDimensional K { x // x ∈ S₁ }

A submodule contained in a finite-dimensional submodule is finite-dimensional.

instance Submodule.finiteDimensional_inf_left {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ : Submodule K V) (S₂ : Submodule K V) [FiniteDimensional K { x // x ∈ S₁ }] : FiniteDimensional K { x // x ∈ S₁ ⊓ S₂ }

The inf of two submodules, the first finite-dimensional, is finite-dimensional.

Equations

• @Submodule.finiteDimensional_inf_left = @Submodule.finiteDimensional_inf_left.proof_1

instance Submodule.finiteDimensional_inf_right {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ : Submodule K V) (S₂ : Submodule K V) [FiniteDimensional K { x // x ∈ S₂ }] : FiniteDimensional K { x // x ∈ S₁ ⊓ S₂ }

The inf of two submodules, the second finite-dimensional, is finite-dimensional.

Equations

• @Submodule.finiteDimensional_inf_right = @Submodule.finiteDimensional_inf_right.proof_1

instance Submodule.finiteDimensional_sup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ : Submodule K V) (S₂ : Submodule K V) [h₁ : FiniteDimensional K { x // x ∈ S₁ }] [h₂ : FiniteDimensional K { x // x ∈ S₂ }] : FiniteDimensional K { x // x ∈ S₁ ⊔ S₂ }

The sup of two finite-dimensional submodules is finite-dimensional.

Equations

• @Submodule.finiteDimensional_sup = @Submodule.finiteDimensional_sup.proof_1

instance Submodule.finiteDimensional_finset_sup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} (s : Finset ι) (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K { x // x ∈ S i }] : FiniteDimensional K { x // x ∈ Finset.sup s S }

The submodule generated by a finite supremum of finite dimensional submodules is finite-dimensional.

Note that strictly this only needs ∀ i ∈ s, FiniteDimensional K (S i), but that doesn't work well with typeclass search.

Equations

• @Submodule.finiteDimensional_finset_sup = @Submodule.finiteDimensional_finset_sup.proof_1

instance Submodule.finiteDimensional_iSup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Sort u_1} [Finite ι] (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K { x // x ∈ S i }] : FiniteDimensional K { x // x ∈ ⨆ (i : ι), S i }

The submodule generated by a supremum of finite dimensional submodules, indexed by a finite sort is finite-dimensional.

Equations

• @Submodule.finiteDimensional_iSup = @Submodule.finiteDimensional_iSup.proof_1

theorem Submodule.finrank_quotient_add_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (s : Submodule K V) : FiniteDimensional.finrank K (V ⧸ s) + FiniteDimensional.finrank K { x // x ∈ s } = FiniteDimensional.finrank K V

In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding quotient add up to the dimension of the space.

theorem Submodule.finrank_lt {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s : Submodule K V} (h : s < ⊤) : FiniteDimensional.finrank K { x // x ∈ s } < FiniteDimensional.finrank K V

The dimension of a strict submodule is strictly bounded by the dimension of the ambient space.

theorem Submodule.finrank_sup_add_finrank_inf_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) (t : Submodule K V) [FiniteDimensional K { x // x ∈ s }] [FiniteDimensional K { x // x ∈ t }] : FiniteDimensional.finrank K { x // x ∈ s ⊔ t } + FiniteDimensional.finrank K { x // x ∈ s ⊓ t } = FiniteDimensional.finrank K { x // x ∈ s } + FiniteDimensional.finrank K { x // x ∈ t }

The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t

theorem Submodule.finrank_add_le_finrank_add_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) (t : Submodule K V) [FiniteDimensional K { x // x ∈ s }] [FiniteDimensional K { x // x ∈ t }] : FiniteDimensional.finrank K { x // x ∈ s ⊔ t } ≤ FiniteDimensional.finrank K { x // x ∈ s } + FiniteDimensional.finrank K { x // x ∈ t }

theorem Submodule.eq_top_of_disjoint {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (s : Submodule K V) (t : Submodule K V) (hdim : FiniteDimensional.finrank K { x // x ∈ s } + FiniteDimensional.finrank K { x // x ∈ t } = FiniteDimensional.finrank K V) (hdisjoint : Disjoint s t) : s ⊔ t = ⊤

theorem LinearEquiv.finiteDimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V ≃ₗ[K] V₂) [FiniteDimensional K V] : FiniteDimensional K V₂

Finite dimensionality is preserved under linear equivalence.

instance finiteDimensional_finsupp {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Finite ι] [FiniteDimensional K V] : FiniteDimensional K (ι →₀ V)

Equations

• @finiteDimensional_finsupp = @finiteDimensional_finsupp.proof_1

theorem FiniteDimensional.eq_of_le_of_finrank_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ : Submodule K V} {S₂ : Submodule K V} [FiniteDimensional K { x // x ∈ S₂ }] (hle : S₁ ≤ S₂) (hd : FiniteDimensional.finrank K { x // x ∈ S₂ } ≤ FiniteDimensional.finrank K { x // x ∈ S₁ }) : S₁ = S₂

theorem FiniteDimensional.eq_of_le_of_finrank_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ : Submodule K V} {S₂ : Submodule K V} [FiniteDimensional K { x // x ∈ S₂ }] (hle : S₁ ≤ S₂) (hd : FiniteDimensional.finrank K { x // x ∈ S₁ } = FiniteDimensional.finrank K { x // x ∈ S₂ }) : S₁ = S₂

If a submodule is less than or equal to a finite-dimensional submodule with the same dimension, they are equal.

noncomputable def FiniteDimensional.LinearEquiv.quotEquivOfEquiv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {p : Subspace K V} {q : Subspace K V₂} (f₁ : { x // x ∈ p } ≃ₗ[K] { x // x ∈ q }) (f₂ : V ≃ₗ[K] V₂) : (V ⧸ p) ≃ₗ[K] V₂ ⧸ q

Given isomorphic subspaces p q of vector spaces V and V₁ respectively, p.quotient is isomorphic to q.quotient.

Equations

• FiniteDimensional.LinearEquiv.quotEquivOfEquiv f₁ f₂ = LinearEquiv.ofFinrankEq (V ⧸ p) (V₂ ⧸ q) (_ : FiniteDimensional.finrank K (V ⧸ p) = FiniteDimensional.finrank K (V₂ ⧸ q))

noncomputable def FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {p : Subspace K V} {q : Subspace K V} (f : (V ⧸ p) ≃ₗ[K] { x // x ∈ q }) : (V ⧸ q) ≃ₗ[K] { x // x ∈ p }

Given the subspaces p q, if p.quotient ≃ₗ[K] q, then q.quotient ≃ₗ[K] p

Equations

• FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv f = LinearEquiv.ofFinrankEq (V ⧸ q) { x // x ∈ p } (_ : FiniteDimensional.finrank K (V ⧸ q) = FiniteDimensional.finrank K { x // x ∈ p })

theorem LinearMap.surjective_of_injective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} (hinj : Function.Injective ↑f) : Function.Surjective ↑f

On a finite-dimensional space, an injective linear map is surjective.

theorem LinearMap.finiteDimensional_of_surjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) (hf : LinearMap.range f = ⊤) : FiniteDimensional K V₂

The image under an onto linear map of a finite-dimensional space is also finite-dimensional.

instance LinearMap.finiteDimensional_range {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) : FiniteDimensional K { x // x ∈ LinearMap.range f }

The range of a linear map defined on a finite-dimensional space is also finite-dimensional.

Equations

• @LinearMap.finiteDimensional_range = @LinearMap.finiteDimensional_range.proof_1

theorem LinearMap.injective_iff_surjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} : Function.Injective ↑f ↔ Function.Surjective ↑f

On a finite-dimensional space, a linear map is injective if and only if it is surjective.

theorem LinearMap.ker_eq_bot_iff_range_eq_top {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} : LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤

theorem LinearMap.mul_eq_one_of_mul_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} {g : V →ₗ[K] V} (hfg : f * g = 1) : g * f = 1

In a finite-dimensional space, if linear maps are inverse to each other on one side then they are also inverse to each other on the other side.

theorem LinearMap.mul_eq_one_comm {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} {g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1

In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

theorem LinearMap.comp_eq_id_comm {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} {g : V →ₗ[K] V} : LinearMap.comp f g = LinearMap.id ↔ LinearMap.comp g f = LinearMap.id

In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

theorem LinearMap.finrank_range_add_finrank_ker {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) : FiniteDimensional.finrank K { x // x ∈ LinearMap.range f } + FiniteDimensional.finrank K { x // x ∈ LinearMap.ker f } = FiniteDimensional.finrank K V

rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to the dimension of the source space.

noncomputable def LinearEquiv.ofInjectiveEndo {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ↑f) : V ≃ₗ[K] V

The linear equivalence corresponding to an injective endomorphism.

Equations

• LinearEquiv.ofInjectiveEndo f h_inj = LinearEquiv.ofBijective f (_ : Function.Injective ↑f ∧ Function.Surjective ↑f)

@[simp]

theorem LinearEquiv.coe_ofInjectiveEndo {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ↑f) : ↑(LinearEquiv.ofInjectiveEndo f h_inj) = ↑f

@[simp]

theorem LinearEquiv.ofInjectiveEndo_right_inv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ↑f) : f * ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo f h_inj)) = 1

@[simp]

theorem LinearEquiv.ofInjectiveEndo_left_inv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ↑f) : ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo f h_inj)) * f = 1

theorem LinearMap.isUnit_iff_ker_eq_bot {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ LinearMap.ker f = ⊥

theorem LinearMap.isUnit_iff_range_eq_top {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ LinearMap.range f = ⊤

theorem finrank_zero_iff_forall_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : FiniteDimensional.finrank K V = 0 ↔ ∀ (x : V), x = 0

noncomputable def basisOfFinrankZero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} [IsEmpty ι] (hV : FiniteDimensional.finrank K V = 0) : Basis ι K V

If ι is an empty type and V is zero-dimensional, there is a unique ι-indexed basis.

Equations

• basisOfFinrankZero hV = Basis.empty V

theorem LinearMap.injective_iff_surjective_of_finrank_eq_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (H : FiniteDimensional.finrank K V = FiniteDimensional.finrank K V₂) {f : V →ₗ[K] V₂} : Function.Injective ↑f ↔ Function.Surjective ↑f

theorem LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (H : FiniteDimensional.finrank K V = FiniteDimensional.finrank K V₂) {f : V →ₗ[K] V₂} : LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤

noncomputable def LinearMap.linearEquivOfInjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (f : V →ₗ[K] V₂) (hf : Function.Injective ↑f) (hdim : FiniteDimensional.finrank K V = FiniteDimensional.finrank K V₂) : V ≃ₗ[K] V₂

Given a linear map f between two vector spaces with the same dimension, if ker f = ⊥ then linearEquivOfInjective is the induced isomorphism between the two vector spaces.

Equations

• LinearMap.linearEquivOfInjective f hf hdim = LinearEquiv.ofBijective f (_ : Function.Injective ↑f ∧ Function.Surjective ↑f)

@[simp]

theorem LinearMap.linearEquivOfInjective_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (hf : Function.Injective ↑f) (hdim : FiniteDimensional.finrank K V = FiniteDimensional.finrank K V₂) (x : V) : ↑(LinearMap.linearEquivOfInjective f hf hdim) x = ↑f x

theorem FiniteDimensional.exists_mul_eq_one (F : Type u_1) {K : Type u_2} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : ∃ y, x * y = 1

noncomputable def divisionRingOfFiniteDimensional (F : Type u_1) (K : Type u_2) [Field F] [h : Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] : DivisionRing K

A domain that is module-finite as an algebra over a field is a division ring.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def fieldOfFiniteDimensional (F : Type u_1) (K : Type u_2) [Field F] [h : CommRing K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] : Field K

An integral domain that is module-finite as an algebra over a field is a field.

Equations

• fieldOfFiniteDimensional F K = let src := divisionRingOfFiniteDimensional F K; Field.mk DivisionRing.zpow (_ : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) DivisionRing.qsmul

theorem Submodule.finrank_mono {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Monotone fun s => FiniteDimensional.finrank K { x // x ∈ s }

theorem Submodule.finrank_lt_finrank_of_lt {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Submodule K V} {t : Submodule K V} [FiniteDimensional K { x // x ∈ t }] (hst : s < t) : FiniteDimensional.finrank K { x // x ∈ s } < FiniteDimensional.finrank K { x // x ∈ t }

theorem Submodule.finrank_strictMono {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : StrictMono fun s => FiniteDimensional.finrank K { x // x ∈ s }

theorem Submodule.finrank_add_eq_of_isCompl {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U : Submodule K V} {W : Submodule K V} (h : IsCompl U W) : FiniteDimensional.finrank K { x // x ∈ U } + FiniteDimensional.finrank K { x // x ∈ W } = FiniteDimensional.finrank K V

theorem finrank_span_singleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {v : V} (hv : v ≠ 0) : FiniteDimensional.finrank K { x // x ∈ Submodule.span K {v} } = 1

theorem exists_smul_eq_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : FiniteDimensional.finrank K V = 1) {x : V} (hx : x ≠ 0) (y : V) : ∃ c, c • x = y

In a one-dimensional space, any vector is a multiple of any nonzero vector

theorem Set.finrank_mono {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s : Set V} {t : Set V} (h : s ⊆ t) : Set.finrank K s ≤ Set.finrank K t

theorem span_eq_top_of_linearIndependent_of_card_eq_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [hι : Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = FiniteDimensional.finrank K V) : Submodule.span K (Set.range b) = ⊤

@[simp]

theorem basisOfLinearIndependentOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = FiniteDimensional.finrank K V) : ∀ (a : V), ↑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a = ↑(LinearIndependent.repr lin_ind) (↑(LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id (_ : ∀ (x : V), ↑LinearMap.id x ∈ Submodule.span K (Set.range b))) a)

noncomputable def basisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = FiniteDimensional.finrank K V) : Basis ι K V

A linear independent family of finrank K V vectors forms a basis.

Equations

• basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq = Basis.mk lin_ind (_ : ⊤ ≤ Submodule.span K (Set.range b))

@[simp]

theorem coe_basisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = FiniteDimensional.finrank K V) : ↑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = b

@[simp]

theorem finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : Finset.Nonempty s) (lin_ind : LinearIndependent K Subtype.val) (card_eq : Finset.card s = FiniteDimensional.finrank K V) : ∀ (a : V), ↑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq).repr a = ↑(LinearIndependent.repr lin_ind) (↑(LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id (_ : ∀ (x : V), ↑LinearMap.id x ∈ Submodule.span K (Set.range Subtype.val))) a)

noncomputable def finsetBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : Finset.Nonempty s) (lin_ind : LinearIndependent K Subtype.val) (card_eq : Finset.card s = FiniteDimensional.finrank K V) : Basis { x // x ∈ s } K V

A linear independent finset of finrank K V vectors forms a basis.

Equations

• finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank lin_ind (_ : Fintype.card { x // x ∈ s } = FiniteDimensional.finrank K V)

@[simp]

theorem coe_finsetBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : Finset.Nonempty s) (lin_ind : LinearIndependent K Subtype.val) (card_eq : Finset.card s = FiniteDimensional.finrank K V) : ↑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = Subtype.val

@[simp]

theorem setBasisOfLinearIndependentOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty ↑s] [Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : Finset.card (Set.toFinset s) = FiniteDimensional.finrank K V) : ∀ (a : V), ↑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a = ↑(LinearIndependent.repr lin_ind) (↑(LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id (_ : ∀ (x : V), ↑LinearMap.id x ∈ Submodule.span K (Set.range Subtype.val))) a)

noncomputable def setBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty ↑s] [Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : Finset.card (Set.toFinset s) = FiniteDimensional.finrank K V) : Basis (↑s) K V

A linear independent set of finrank K V vectors forms a basis.

Equations

• setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank lin_ind (_ : Fintype.card ↑s = FiniteDimensional.finrank K V)

@[simp]

theorem coe_setBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty ↑s] [Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : Finset.card (Set.toFinset s) = FiniteDimensional.finrank K V) : ↑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = Subtype.val

We now give characterisations of finrank K V = 1 and finrank K V ≤ 1.

theorem finrank_eq_one_iff_of_nonzero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (nz : v ≠ 0) : FiniteDimensional.finrank K V = 1 ↔ Submodule.span K {v} = ⊤

A vector space with a nonzero vector v has dimension 1 iff v spans.

theorem finrank_eq_one_iff_of_nonzero' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (nz : v ≠ 0) : FiniteDimensional.finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w

A module with a nonzero vector v has dimension 1 iff every vector is a multiple of v.

theorem finrank_eq_one_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [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.

theorem finrank_eq_one_iff' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] : FiniteDimensional.finrank K V = 1 ↔ ∃ v _n, ∀ (w : V), ∃ c, 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} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : FiniteDimensional.finrank K V ≤ 1 ↔ ∃ v, ∀ (w : V), ∃ c, 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} [DivisionRing K] [AddCommGroup V] [Module K V] (W : Submodule K V) [FiniteDimensional K { x // x ∈ W }] : FiniteDimensional.finrank K { x // x ∈ W } ≤ 1 ↔ Submodule.IsPrincipal W

theorem Module.finrank_le_one_iff_top_isPrincipal {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : FiniteDimensional.finrank K V ≤ 1 ↔ Submodule.IsPrincipal ⊤

theorem surjective_of_nonzero_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {W : Type u_1} {A : Type u_2} [Semiring A] [Module A V] [AddCommGroup W] [Module K W] [Module A W] [LinearMap.CompatibleSMul V W K A] (h : FiniteDimensional.finrank K W = 1) {f : V →ₗ[A] W} (w : f ≠ 0) : Function.Surjective ↑f

theorem is_simple_module_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {A : Type u_1} [Semiring A] [Module A V] [SMul K A] [IsScalarTower K A V] (h : FiniteDimensional.finrank K V = 1) : IsSimpleOrder (Submodule A V)

Any K-algebra module that is 1-dimensional over K is simple.

theorem Subalgebra.finiteDimensional_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F { x // x ∈ ↑Subalgebra.toSubmodule S } ↔ FiniteDimensional F { x // x ∈ S }

A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

theorem FiniteDimensional.of_subalgebra_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F { x // x ∈ ↑Subalgebra.toSubmodule S } → FiniteDimensional F { x // x ∈ S }

Alias of the forward direction of Subalgebra.finiteDimensional_toSubmodule.

---

A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

theorem FiniteDimensional.subalgebra_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F { x // x ∈ S } → FiniteDimensional F { x // x ∈ ↑Subalgebra.toSubmodule S }

Alias of the reverse direction of Subalgebra.finiteDimensional_toSubmodule.

---

A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

instance FiniteDimensional.finiteDimensional_subalgebra {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] [FiniteDimensional F E] (S : Subalgebra F E) : FiniteDimensional F { x // x ∈ S }

Equations

• @FiniteDimensional.finiteDimensional_subalgebra = @FiniteDimensional.finiteDimensional_subalgebra.proof_1

instance Subalgebra.finiteDimensional_bot {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] : FiniteDimensional F { x // x ∈ ⊥ }

Equations

• @Subalgebra.finiteDimensional_bot = @Subalgebra.finiteDimensional_bot.proof_1

theorem Subalgebra.eq_bot_of_rank_le_one {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} (h : Module.rank F { x // x ∈ S } ≤ 1) : S = ⊥

theorem Subalgebra.eq_bot_of_finrank_one {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} (h : FiniteDimensional.finrank F { x // x ∈ S } = 1) : S = ⊥

@[simp]

theorem Subalgebra.rank_eq_one_iff {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] [Nontrivial E] {S : Subalgebra F E} : Module.rank F { x // x ∈ S } = 1 ↔ S = ⊥

@[simp]

theorem Subalgebra.finrank_eq_one_iff {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] [Nontrivial E] {S : Subalgebra F E} : FiniteDimensional.finrank F { x // x ∈ S } = 1 ↔ S = ⊥

theorem Subalgebra.bot_eq_top_iff_rank_eq_one {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] [Nontrivial E] : ⊥ = ⊤ ↔ Module.rank F E = 1

theorem Subalgebra.bot_eq_top_iff_finrank_eq_one {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] [Nontrivial E] : ⊥ = ⊤ ↔ FiniteDimensional.finrank F E = 1

@[simp]

theorem Subalgebra.bot_eq_top_of_rank_eq_one {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] [Nontrivial 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} [Field F] [Ring E] [Algebra F E] [Nontrivial E] : FiniteDimensional.finrank F E = 1 → ⊥ = ⊤

Alias of the reverse direction of Subalgebra.bot_eq_top_iff_finrank_eq_one.

theorem Subalgebra.isSimpleOrder_of_finrank {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] (hr : FiniteDimensional.finrank F E = 2) : IsSimpleOrder (Subalgebra F E)

theorem Module.End.exists_ker_pow_eq_ker_pow_succ {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : ∃ k, k ≤ FiniteDimensional.finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)

theorem Module.End.ker_pow_constant {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {f : Module.End K V} {k : ℕ} (h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)) (m : ℕ) : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))

theorem Module.End.ker_pow_eq_ker_pow_finrank_of_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {m : ℕ} (hm : FiniteDimensional.finrank K V ≤ m) : LinearMap.ker (f ^ m) = LinearMap.ker (f ^ FiniteDimensional.finrank K V)

theorem Module.End.ker_pow_le_ker_pow_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (m : ℕ) : LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ FiniteDimensional.finrank K V)

theorem cardinal_mk_eq_cardinal_mk_field_pow_rank (K : Type u) (V : Type u) [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Cardinal.mk V = Cardinal.mk K ^ Module.rank K V

theorem cardinal_lt_aleph0_of_finiteDimensional (K : Type u) (V : Type u) [DivisionRing K] [AddCommGroup V] [Module K V] [Finite K] [FiniteDimensional K V] : Cardinal.mk V < Cardinal.aleph0