Rank of free modules

Main result

• LinearEquiv.nonempty_equiv_iff_lift_rank_eq: Two free modules are isomorphic iff they have the same dimension.
• FiniteDimensional.finBasis: An arbitrary basis of a finite free module indexed by Fin n given finrank R M = n.

theorem lift_rank_mul_lift_rank (F : Type u) (K : Type v) (A : Type w) [Ring F] [Ring K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] [Module.Free K A] : Cardinal.lift.{w, v} (Module.rank F K) * Cardinal.lift.{v, w} (Module.rank K A) = Cardinal.lift.{v, w} (Module.rank F A)

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

The universe polymorphic version of rank_mul_rank below.

theorem rank_mul_rank (F : Type u) (K : Type v) [Ring F] [Ring K] [Module F K] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] (A : Type v) [AddCommGroup A] [Module K A] [Module F A] [IsScalarTower F K A] [Module.Free K A] : Module.rank F K * Module.rank K A = Module.rank F A

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

This is a simpler version of lift_rank_mul_lift_rank with K and A in the same universe.

theorem FiniteDimensional.finrank_mul_finrank (F : Type u) (K : Type v) (A : Type w) [Ring F] [Ring K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] [Module.Free K A] : FiniteDimensional.finrank F K * FiniteDimensional.finrank K A = FiniteDimensional.finrank F A

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

theorem Module.Free.rank_eq_card_chooseBasisIndex (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] : Module.rank R M = Cardinal.mk (Module.Free.ChooseBasisIndex R M)

The rank of a free module M over R is the cardinality of ChooseBasisIndex R M.

theorem FiniteDimensional.finrank_eq_card_chooseBasisIndex (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : FiniteDimensional.finrank R M = Fintype.card (Module.Free.ChooseBasisIndex R M)

The finrank of a free module M over R is the cardinality of ChooseBasisIndex R M.

theorem Module.Free.rank_eq_mk_of_infinite_lt (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [Infinite R] (h_lt : Cardinal.lift.{v, u} (Cardinal.mk R) < Cardinal.lift.{u, v} (Cardinal.mk M)) : Module.rank R M = Cardinal.mk M

The rank of a free module M over an infinite scalar ring R is the cardinality of M whenever #R < #M.

theorem nonempty_linearEquiv_of_lift_rank_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M'] [Module.Free R M'] (cnd : Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')) : Nonempty (M ≃ₗ[R] M')

Two vector spaces are isomorphic if they have the same dimension.

theorem nonempty_linearEquiv_of_rank_eq {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M₁] [Module R M₁] [Module.Free R M₁] (cond : Module.rank R M = Module.rank R M₁) : Nonempty (M ≃ₗ[R] M₁)

Two vector spaces are isomorphic if they have the same dimension.

def LinearEquiv.ofLiftRankEq {R : Type u} (M : Type v) (M' : Type v') [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M'] [Module.Free R M'] (cond : Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')) : M ≃ₗ[R] M'

Two vector spaces are isomorphic if they have the same dimension.

Equations

• LinearEquiv.ofLiftRankEq M M' cond = Classical.choice ⋯

def LinearEquiv.ofRankEq {R : Type u} (M : Type v) (M₁ : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M₁] [Module R M₁] [Module.Free R M₁] (cond : Module.rank R M = Module.rank R M₁) : M ≃ₗ[R] M₁

Two vector spaces are isomorphic if they have the same dimension.

Equations

• LinearEquiv.ofRankEq M M₁ cond = Classical.choice ⋯

theorem LinearEquiv.nonempty_equiv_iff_lift_rank_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M'] [Module.Free R M'] : Nonempty (M ≃ₗ[R] M') ↔ Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')

Two vector spaces are isomorphic if and only if they have the same dimension.

theorem LinearEquiv.nonempty_equiv_iff_rank_eq {R : Type u} {M : Type v} {M₁ : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M₁] [Module R M₁] [Module.Free R M₁] : Nonempty (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁

Two vector spaces are isomorphic if and only if they have the same dimension.

theorem FiniteDimensional.nonempty_linearEquiv_of_finrank_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M'] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] (cond : FiniteDimensional.finrank R M = FiniteDimensional.finrank R M') : Nonempty (M ≃ₗ[R] M')

Two finite and free modules are isomorphic if they have the same (finite) rank.

theorem FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq {R : Type u} {M : Type v} {M' : Type v'} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M'] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] : Nonempty (M ≃ₗ[R] M') ↔ FiniteDimensional.finrank R M = FiniteDimensional.finrank R M'

Two finite and free modules are isomorphic if and only if they have the same (finite) rank.

noncomputable def LinearEquiv.ofFinrankEq {R : Type u} (M : Type v) (M' : Type v') [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup M'] [Module R M'] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] (cond : FiniteDimensional.finrank R M = FiniteDimensional.finrank R M') : M ≃ₗ[R] M'

Two finite and free modules are isomorphic if they have the same (finite) rank.

Equations

• LinearEquiv.ofFinrankEq M M' cond = Classical.choice ⋯

theorem Module.rank_lt_alpeh0_iff {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] : Module.rank R M < Cardinal.aleph0 ↔ Module.Finite R M

See rank_lt_aleph0 for the inverse direction without Module.Free R M.

theorem FiniteDimensional.finrank_of_not_finite {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : ¬Module.Finite R M) : FiniteDimensional.finrank R M = 0

theorem Module.finite_of_finrank_pos {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : 0 < FiniteDimensional.finrank R M) : Module.Finite R M

theorem Module.finite_of_finrank_eq_succ {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] {n : ℕ} (hn : FiniteDimensional.finrank R M = Nat.succ n) : Module.Finite R M

theorem Module.finite_iff_of_rank_eq_nsmul {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] {W : Type v} [AddCommGroup W] [Module R W] [Module.Free R W] {n : ℕ} (hn : n ≠ 0) (hVW : Module.rank R M = n • Module.rank R W) : Module.Finite R M ↔ Module.Finite R W

noncomputable def FiniteDimensional.finBasis (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : Basis (Fin (FiniteDimensional.finrank R M)) R M

A finite rank free module has a basis indexed by Fin (finrank R M).

Equations

• FiniteDimensional.finBasis R M = Basis.reindex (Module.Free.chooseBasis R M) (Fintype.equivFinOfCardEq ⋯)

noncomputable def FiniteDimensional.finBasisOfFinrankEq (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {n : ℕ} (hn : FiniteDimensional.finrank R M = n) : Basis (Fin n) R M

A rank n free module has a basis indexed by Fin n.

Equations

• FiniteDimensional.finBasisOfFinrankEq R M hn = Basis.reindex (FiniteDimensional.finBasis R M) (Fin.castIso hn).toEquiv

noncomputable def FiniteDimensional.basisUnique {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] (ι : Type u_1) [Unique ι] (h : FiniteDimensional.finrank R M = 1) : Basis ι R M

A free module with rank 1 has a basis with one element.

Equations

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

@[simp]

theorem FiniteDimensional.basisUnique_repr_eq_zero_iff {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] {ι : Type u_1} [Unique ι] {h : FiniteDimensional.finrank R M = 1} {v : M} {i : ι} : ((FiniteDimensional.basisUnique ι h).repr v) i = 0 ↔ v = 0