Rank of finite free modules #

This is a basic API for the rank of finite free modules.

@[simp]

theorem FiniteDimensional.Submodule.finrank_map_subtype_eq (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (q : Submodule R { x // x ∈ p }) :

FiniteDimensional.finrank R { x // x ∈ Submodule.map (Submodule.subtype p) q } = FiniteDimensional.finrank R { x // x ∈ q }

source

@[simp]

theorem FiniteDimensional.finrank_ulift (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] :

FiniteDimensional.finrank R (ULift.{u_1, v} M) = FiniteDimensional.finrank R M

source

theorem FiniteDimensional.rank_lt_aleph0 (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Finite R M] :

Module.rank R M < Cardinal.aleph0

The rank of a finite module is finite.

source

@[simp]

theorem FiniteDimensional.finrank_eq_rank (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Finite R M] :

↑(FiniteDimensional.finrank R M) = Module.rank R M

If M is finite, finrank M = rank M.

source

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.

source

@[simp]

theorem FiniteDimensional.finrank_finsupp (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] :

FiniteDimensional.finrank R (ι →₀ R) = Fintype.card ι

The finrank of (ι →₀ R) is Fintype.card ι.

source

theorem FiniteDimensional.finrank_pi (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] :

FiniteDimensional.finrank R (ι → R) = Fintype.card ι

The finrank of (ι → R) is Fintype.card ι.

source

@[simp]

theorem FiniteDimensional.finrank_directSum (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] (M : ι → Type w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] [∀ (i : ι), Module.Finite R (M i)] :

FiniteDimensional.finrank R (⨁ (i : ι), M i) = Finset.sum Finset.univ fun i => FiniteDimensional.finrank R (M i)

The finrank of the direct sum is the sum of the finranks.

source

@[simp]

theorem FiniteDimensional.finrank_prod (R : Type u) (M : Type v) (N : Type w) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module.Free R N] [Module.Finite R N] :

FiniteDimensional.finrank R (M × N) = FiniteDimensional.finrank R M + FiniteDimensional.finrank R N

The finrank of M × N is (finrank R M) + (finrank R N).

source

theorem FiniteDimensional.finrank_pi_fintype (R : Type u) [Ring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] {M : ι → Type w} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] [∀ (i : ι), Module.Finite R (M i)] :

FiniteDimensional.finrank R ((i : ι) → M i) = Finset.sum Finset.univ fun i => FiniteDimensional.finrank R (M i)

The finrank of a finite product is the sum of the finranks.

source

theorem FiniteDimensional.finrank_matrix (R : Type u) [Ring R] [StrongRankCondition R] (m : Type u_1) (n : Type u_2) [Fintype m] [Fintype n] :

FiniteDimensional.finrank R (Matrix m n R) = Fintype.card m * Fintype.card n

If m and n are Fintype, the finrank of m × n matrices is (Fintype.card m) * (Fintype.card n).

source

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

Nonempty (M ≃ₗ[R] N)

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

source

theorem FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq {R : Type u} {M : Type v} {N : Type w} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module.Free R N] [Module.Finite R N] :

Nonempty (M ≃ₗ[R] N) ↔ FiniteDimensional.finrank R M = FiniteDimensional.finrank R N

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

source

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

M ≃ₗ[R] N

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

Equations

LinearEquiv.ofFinrankEq M N cond = Classical.choice (_ : Nonempty (M ≃ₗ[R] N))

Instances For

source

@[simp]

theorem FiniteDimensional.finrank_tensorProduct (R : Type u) [CommRing R] [StrongRankCondition R] (M : Type v) (N : Type w) [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup N] [Module R N] [Module.Free R N] :

FiniteDimensional.finrank R (TensorProduct R M N) = FiniteDimensional.finrank R M * FiniteDimensional.finrank R N

The finrank of M ⊗[R] N is (finrank R M) * (finrank R N).

source

theorem LinearMap.finrank_le_finrank_of_injective {R : Type u} {M : Type v} {N : Type w} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R N] {f : M →ₗ[R] N} (hf : Function.Injective ↑f) :

FiniteDimensional.finrank R M ≤ FiniteDimensional.finrank R N

source

theorem LinearMap.finrank_range_le {R : Type u} {M : Type v} {N : Type w} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] (f : M →ₗ[R] N) :

FiniteDimensional.finrank R { x // x ∈ LinearMap.range f } ≤ FiniteDimensional.finrank R M

source

theorem Submodule.finrank_le {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Finite R M] (s : Submodule R M) :

FiniteDimensional.finrank R { x // x ∈ s } ≤ FiniteDimensional.finrank R M

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

source

theorem Submodule.finrank_quotient_le {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [Module.Finite R M] (s : Submodule R M) :

FiniteDimensional.finrank R (M ⧸ s) ≤ FiniteDimensional.finrank R M

The dimension of a quotient is bounded by the dimension of the ambient space.

source

theorem Submodule.finrank_map_le {R : Type u} {M : Type v} {N : Type w} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (p : Submodule R M) [Module.Finite R { x // x ∈ p }] :

FiniteDimensional.finrank R { x // x ∈ Submodule.map f p } ≤ FiniteDimensional.finrank R { x // x ∈ p }

Pushforwards of finite submodules have a smaller finrank.

source

theorem Submodule.finrank_le_finrank_of_le {R : Type u} {M : Type v} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] {s : Submodule R M} {t : Submodule R M} [Module.Finite R { x // x ∈ t }] (hst : s ≤ t) :

FiniteDimensional.finrank R { x // x ∈ s } ≤ FiniteDimensional.finrank R { x // x ∈ t }