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 ↥p)
:
@[simp]
theorem
FiniteDimensional.finrank_ulift
(R : Type u)
(M : Type v)
[Ring R]
[AddCommGroup M]
[Module R M]
:
theorem
FiniteDimensional.rank_lt_aleph0
(R : Type u)
(M : Type v)
[Ring R]
[StrongRankCondition R]
[AddCommGroup M]
[Module R M]
[Module.Finite R M]
:
The rank of a finite module is finite.
@[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.
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]
:
The finrank of a free module M over R is the cardinality of ChooseBasisIndex R M.
@[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 ι.
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 ι.
@[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 (DirectSum ι fun (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.
@[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).
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.
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).
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)
:
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}
{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.
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)
:
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
@[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).
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)
:
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)
:
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)
:
The dimension of a submodule is bounded by the dimension of the ambient space.
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.
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 ↥p]
:
FiniteDimensional.finrank R ↥(Submodule.map f p) ≤ FiniteDimensional.finrank R ↥p
Pushforwards of finite submodules have a smaller finrank.
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 ↥t]
(hst : s ≤ t)
: