Extra results about Module.rank #
This file contains some extra results not in LinearAlgebra.Dimension.
@[simp]
theorem
rank_finsupp
(R : Type u)
(M : Type v)
[Ring R]
[StrongRankCondition R]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
(ι : Type w)
:
Module.rank R (ι →₀ M) = Cardinal.lift.{v, w} (Cardinal.mk ι) * Cardinal.lift.{w, v} (Module.rank R M)
theorem
rank_finsupp'
(R : Type u)
(M : Type v)
[Ring R]
[StrongRankCondition R]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
(ι : Type v)
:
Module.rank R (ι →₀ M) = Cardinal.mk ι * Module.rank R M
theorem
rank_finsupp_self
(R : Type u)
[Ring R]
[StrongRankCondition R]
(ι : Type w)
:
Module.rank R (ι →₀ R) = Cardinal.lift.{u, w} (Cardinal.mk ι)
The rank of (ι →₀ R) is (#ι).lift.
theorem
rank_finsupp_self'
(R : Type u)
[Ring R]
[StrongRankCondition R]
{ι : Type u}
:
Module.rank R (ι →₀ R) = Cardinal.mk ι
If R and ι lie in the same universe, the rank of (ι →₀ R) is # ι.
@[simp]
theorem
rank_directSum
(R : Type u)
[Ring R]
[StrongRankCondition R]
{ι : Type v}
(M : ι → Type w)
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.Free R (M i)]
:
Module.rank R (⨁ (i : ι), M i) = Cardinal.sum fun i => Module.rank R (M i)
The rank of the direct sum is the sum of the ranks.
@[simp]
theorem
rank_matrix
(R : Type u)
[Ring R]
[StrongRankCondition R]
(m : Type v)
(n : Type w)
[Finite m]
[Finite n]
:
Module.rank R (Matrix m n R) = Cardinal.lift.{max v w u, v} (Cardinal.mk m) * Cardinal.lift.{max v w u, w} (Cardinal.mk n)
If m and n are Fintype, the rank of m × n matrices is (#m).lift * (#n).lift.
@[simp]
theorem
rank_matrix'
(R : Type u)
[Ring R]
[StrongRankCondition R]
(m : Type v)
(n : Type v)
[Finite m]
[Finite n]
:
Module.rank R (Matrix m n R) = Cardinal.lift.{u, v} (Cardinal.mk m * Cardinal.mk n)
If m and n are Fintype that lie in the same universe, the rank of m × n matrices is
(#n * #m).lift.
theorem
rank_matrix''
(R : Type u)
[Ring R]
[StrongRankCondition R]
(m : Type u)
(n : Type u)
[Finite m]
[Finite n]
:
Module.rank R (Matrix m n R) = Cardinal.mk m * Cardinal.mk n
If m and n are Fintype that lie in the same universe as R, the rank of m × n matrices
is # m * # n.
@[simp]
theorem
rank_tensorProduct
(R : Type u)
(M : Type v)
(N : Type w)
[CommRing R]
[StrongRankCondition R]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
[AddCommGroup N]
[Module R N]
[Module.Free R N]
:
Module.rank R (TensorProduct R M N) = Cardinal.lift.{w, v} (Module.rank R M) * Cardinal.lift.{v, w} (Module.rank R N)
The rank of M ⊗[R] N is (Module.rank R M).lift * (Module.rank R N).lift.
theorem
rank_tensorProduct'
(R : Type u)
(M : Type v)
[CommRing R]
[StrongRankCondition R]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
(N : Type v)
[AddCommGroup N]
[Module R N]
[Module.Free R N]
:
Module.rank R (TensorProduct R M N) = Module.rank R M * Module.rank R N
If M and N lie in the same universe, the rank of M ⊗[R] N is
(Module.rank R M) * (Module.rank R N).