Mathlib.LinearAlgebra.Dimension.Free

lift_rank_mul_lift_rank theorem

: Cardinal.lift.{w} (Module.rank F K) * Cardinal.lift.{v} (Module.rank K A) = Cardinal.lift.{v} (Module.rank F A)

Full source

/-- 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 lift_rank_mul_lift_rank :
    Cardinal.lift.{w} (Module.rank F K) * Cardinal.lift.{v} (Module.rank K A) =
      Cardinal.lift.{v} (Module.rank F A) := by
  let b := Module.Free.chooseBasis F K
  let c := Module.Free.chooseBasis K A
  rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank,
    ← lift_umaxlift_umax.{w, v}, ← (b.smulTower c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift,
    lift_lift, lift_lift, lift_umaxlift_umax.{v, w}]

Tower Law for Module Ranks: $\operatorname{rank}_F(K) \cdot \operatorname{rank}_K(A) = \operatorname{rank}_F(A)$

Informal description

Let $F$ be a field, $K$ be a field extension of $F$, and $A$ be a $K$-module. Then the rank of $A$ as an $F$-module satisfies: \[ \operatorname{rank}_F(K) \cdot \operatorname{rank}_K(A) = \operatorname{rank}_F(A) \] where the ranks are considered with appropriate universe lifting to handle type parameters.

rank_mul_rank theorem

 (A : Type v) [AddCommMonoid 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

Full source

/-- 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. -/
@[stacks 09G9]
theorem rank_mul_rank (A : Type v) [AddCommMonoid 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 := by
  convert lift_rank_mul_lift_rank F K A <;> rw [lift_id]

Tower Law for Module Ranks: $\operatorname{rank}_F(K) \cdot \operatorname{rank}_K(A) = \operatorname{rank}_F(A)$

Informal description

Let $F$ be a field, $K$ a field extension of $F$, and $A$ a $K$-module that is free over $K$. Then the rank of $A$ as an $F$-module satisfies: \[ \operatorname{rank}_F(K) \cdot \operatorname{rank}_K(A) = \operatorname{rank}_F(A) \]

Module.finrank_mul_finrank theorem

: finrank F K * finrank K A = finrank F A

Full source

/-- 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.finrank_mul_finrank : finrank F K * finrank K A = finrank F A := by
  simp_rw [finrank]
  rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]

Tower Law for Finite Ranks: $\operatorname{finrank}_F(K) \cdot \operatorname{finrank}_K(A) = \operatorname{finrank}_F(A)$

Informal description

Let $F$ be a field, $K$ a field extension of $F$, and $A$ a finite-dimensional $K$-module. Then the finite rank of $A$ as an $F$-module satisfies: \[ \operatorname{finrank}_F(K) \cdot \operatorname{finrank}_K(A) = \operatorname{finrank}_F(A) \]

Module.Free.rank_eq_card_chooseBasisIndex theorem

: Module.rank R M = #(ChooseBasisIndex R M)

Full source

/-- The rank of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`. -/
theorem rank_eq_card_chooseBasisIndex : Module.rank R M = #(ChooseBasisIndex R M) :=
  (chooseBasis R M).mk_eq_rank''.symm

Rank of Free Module Equals Cardinality of Basis Index Set

Informal description

For a free module $M$ over a ring $R$, the rank of $M$ is equal to the cardinality of the index set used to choose a basis for $M$ over $R$, i.e., $\text{rank}_R M = |\text{ChooseBasisIndex } R M|$.

Module.finrank_eq_card_chooseBasisIndex theorem

[Module.Finite R M] : finrank R M = Fintype.card (ChooseBasisIndex R M)

Full source

/-- The finrank of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`. -/
theorem _root_.Module.finrank_eq_card_chooseBasisIndex [Module.Finite R M] :
    finrank R M = Fintype.card (ChooseBasisIndex R M) := by
  simp [finrank, rank_eq_card_chooseBasisIndex]

Finite Rank Equals Basis Index Cardinality for Free Modules

Informal description

For a finite free module $M$ over a ring $R$, the finite rank of $M$ is equal to the cardinality of the index set $\text{ChooseBasisIndex } R M$ used to choose a basis for $M$ over $R$, i.e., $\text{finrank}_R M = |\text{ChooseBasisIndex } R M|$.

Module.Free.rank_eq_mk_of_infinite_lt theorem

[Infinite R] (h_lt : lift.{v} #R < lift.{u} #M) : Module.rank R M = #M

Full source

/-- The rank of a free module `M` over an infinite scalar ring `R` is the cardinality of `M`
whenever `#R < #M`. -/
lemma rank_eq_mk_of_infinite_lt [Infinite R] (h_lt : lift.{v} #R < lift.{u} #M) :
    Module.rank R M = #M := by
  have : Infinite M := infinite_iff.mpr <| lift_le.mp <| le_trans (by simp) h_lt.le
  have h : lift #M = lift #(ChooseBasisIndex R M →₀ R) := lift_mk_eq'.mpr ⟨(chooseBasis R M).repr⟩
  simp only [mk_finsupp_lift_of_infinite', lift_id', ← rank_eq_card_chooseBasisIndex, lift_max,
    lift_lift] at h
  refine lift_inj.mp ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ ?_).left
  exact (lift_umax.{v, u}.symm ▸ h_lt).ne

Rank of Free Module Equals Cardinality under Infinite Scalar Ring Condition

Informal description

Let $R$ be an infinite ring and $M$ a free $R$-module. If the cardinality of $R$ is strictly less than the cardinality of $M$ (after lifting to a common universe), then the rank of $M$ over $R$ equals the cardinality of $M$, i.e., $\text{rank}_R M = |M|$.

nonempty_linearEquiv_of_lift_rank_eq theorem

(cnd : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')) : Nonempty (M ≃ₗ[R] M')

Full source

/-- Two vector spaces are isomorphic if they have the same dimension. -/
theorem nonempty_linearEquiv_of_lift_rank_eq
    (cnd : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')) :
    Nonempty (M ≃ₗ[R] M') := by
  obtain ⟨⟨α, B⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  obtain ⟨⟨β, B'⟩⟩ := Module.Free.exists_basis (R := R) (M := M')
  have : Cardinal.lift.{v', v} #α = Cardinal.lift.{v, v'} #β := by
    rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']
  exact (Cardinal.lift_mk_eq.{v, v', 0}.1 this).map (B.equiv B')

Existence of Linear Isomorphism for Modules with Equal Rank

Informal description

Let $R$ be a ring and $M$, $M'$ be two $R$-modules. If the (lifted) dimensions of $M$ and $M'$ are equal, i.e., $\text{rank}_R M = \text{rank}_R M'$, then there exists a linear isomorphism between $M$ and $M'$ as $R$-modules.

nonempty_linearEquiv_of_rank_eq theorem

(cond : Module.rank R M = Module.rank R M₁) : Nonempty (M ≃ₗ[R] M₁)

Full source

/-- Two vector spaces are isomorphic if they have the same dimension. -/
theorem nonempty_linearEquiv_of_rank_eq (cond : Module.rank R M = Module.rank R M₁) :
    Nonempty (M ≃ₗ[R] M₁) :=
  nonempty_linearEquiv_of_lift_rank_eq <| congr_arg _ cond

Existence of Linear Isomorphism for Modules with Equal Rank

Informal description

Let $R$ be a ring and let $M$ and $M_1$ be two $R$-modules. If the dimensions of $M$ and $M_1$ over $R$ are equal, i.e., $\text{rank}_R M = \text{rank}_R M_1$, then there exists a linear isomorphism between $M$ and $M_1$ as $R$-modules.

LinearEquiv.ofLiftRankEq definition

(cond : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')) : M ≃ₗ[R] M'

Full source

/-- Two vector spaces are isomorphic if they have the same dimension. -/
def LinearEquiv.ofLiftRankEq
    (cond : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')) :
    M ≃ₗ[R] M' :=
  Classical.choice (nonempty_linearEquiv_of_lift_rank_eq cond)

Linear isomorphism from equal lifted ranks

Informal description

Given a ring $R$ and two $R$-modules $M$ and $M'$, if the lifted dimensions of $M$ and $M'$ are equal, i.e., $\text{rank}_R M = \text{rank}_R M'$, then there exists a linear isomorphism between $M$ and $M'$ as $R$-modules. This isomorphism is constructed by choosing a representative from the nonempty set of linear isomorphisms guaranteed by the equality of ranks.

LinearEquiv.ofRankEq definition

(cond : Module.rank R M = Module.rank R M₁) : M ≃ₗ[R] M₁

Full source

/-- Two vector spaces are isomorphic if they have the same dimension. -/
def LinearEquiv.ofRankEq (cond : Module.rank R M = Module.rank R M₁) : M ≃ₗ[R] M₁ :=
  Classical.choice (nonempty_linearEquiv_of_rank_eq cond)

Linear isomorphism from equal ranks

Informal description

Given a ring $R$ and two $R$-modules $M$ and $M_1$ with equal rank ($\text{rank}_R M = \text{rank}_R M_1$), this definition constructs a linear isomorphism between $M$ and $M_1$ by choosing a representative from the nonempty set of linear isomorphisms guaranteed by the equality of ranks.

LinearEquiv.nonempty_equiv_iff_lift_rank_eq theorem

: Nonempty (M ≃ₗ[R] M') ↔ Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')

Full source

/-- Two vector spaces are isomorphic if and only if they have the same dimension. -/
theorem LinearEquiv.nonempty_equiv_iff_lift_rank_eq : NonemptyNonempty (M ≃ₗ[R] M') ↔
    Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M') :=
  ⟨fun ⟨h⟩ => LinearEquiv.lift_rank_eq h, fun h => nonempty_linearEquiv_of_lift_rank_eq h⟩

Linear isomorphism exists if and only if modules have equal rank

Informal description

Let $R$ be a ring and $M$, $M'$ be two $R$-modules. Then there exists a linear isomorphism between $M$ and $M'$ if and only if their (lifted) dimensions are equal, i.e., $\text{rank}_R M = \text{rank}_R M'$.

LinearEquiv.nonempty_equiv_iff_rank_eq theorem

: Nonempty (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁

Full source

/-- Two vector spaces are isomorphic if and only if they have the same dimension. -/
theorem LinearEquiv.nonempty_equiv_iff_rank_eq :
    NonemptyNonempty (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁ :=
  ⟨fun ⟨h⟩ => LinearEquiv.rank_eq h, fun h => nonempty_linearEquiv_of_rank_eq h⟩

Linear isomorphism exists if and only if modules have equal rank

Informal description

Let $R$ be a ring and let $M$ and $M_1$ be two $R$-modules. There exists a linear isomorphism between $M$ and $M_1$ if and only if their dimensions over $R$ are equal, i.e., $\text{rank}_R M = \text{rank}_R M_1$.

FiniteDimensional.nonempty_linearEquiv_of_finrank_eq theorem

[Module.Finite R M] [Module.Finite R M'] (cond : finrank R M = finrank R M') : Nonempty (M ≃ₗ[R] M')

Full source

/-- Two finite and free modules are isomorphic if they have the same (finite) rank. -/
theorem FiniteDimensional.nonempty_linearEquiv_of_finrank_eq
    [Module.Finite R M] [Module.Finite R M'] (cond : finrank R M = finrank R M') :
    Nonempty (M ≃ₗ[R] M') :=
  nonempty_linearEquiv_of_lift_rank_eq <| by simp only [← finrank_eq_rank, cond, lift_natCast]

Finite free modules are isomorphic if and only if they have the same rank

Informal description

Let $R$ be a ring and $M$, $M'$ be two finite-dimensional free $R$-modules. If $M$ and $M'$ have the same finite rank, i.e., $\text{finrank}_R M = \text{finrank}_R M'$, then there exists a linear isomorphism between $M$ and $M'$ as $R$-modules.

FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq theorem

[Module.Finite R M] [Module.Finite R M'] : Nonempty (M ≃ₗ[R] M') ↔ finrank R M = finrank R M'

Full source

/-- Two finite and free modules are isomorphic if and only if they have the same (finite) rank. -/
theorem FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq [Module.Finite R M]
    [Module.Finite R M'] : NonemptyNonempty (M ≃ₗ[R] M') ↔ finrank R M = finrank R M' :=
  ⟨fun ⟨h⟩ => h.finrank_eq, fun h => nonempty_linearEquiv_of_finrank_eq h⟩

Finite free modules are isomorphic if and only if they have the same rank

Informal description

Let $R$ be a ring and $M$, $M'$ be two finite-dimensional free $R$-modules. There exists a linear isomorphism between $M$ and $M'$ if and only if they have the same finite rank, i.e., $\text{finrank}_R M = \text{finrank}_R M'$.

LinearEquiv.ofFinrankEq definition

[Module.Finite R M] [Module.Finite R M'] (cond : finrank R M = finrank R M') : M ≃ₗ[R] M'

Full source

/-- Two finite and free modules are isomorphic if they have the same (finite) rank. -/
noncomputable def LinearEquiv.ofFinrankEq [Module.Finite R M] [Module.Finite R M']
    (cond : finrank R M = finrank R M') : M ≃ₗ[R] M' :=
  Classical.choice <| FiniteDimensional.nonempty_linearEquiv_of_finrank_eq cond

Linear isomorphism between finite free modules of equal rank

Informal description

Given two finite-dimensional free modules $ M $ and $ M' $ over a ring $ R $, if they have the same finite rank (i.e., $\text{finrank}_R M = \text{finrank}_R M'$), then there exists a linear isomorphism between $ M $ and $ M' $ as $ R $-modules.

Module.subsingleton_of_rank_zero theorem

(h : Module.rank R M = 0) : Subsingleton M

Full source

/-- A free module of rank zero is trivial. -/
lemma subsingleton_of_rank_zero (h : Module.rank R M = 0) : Subsingleton M := by
  rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h
  exact (Module.Free.repr R M).subsingleton

Zero Rank Implies Subsingleton Module

Informal description

If a module $M$ over a ring $R$ has rank zero, then $M$ is a subsingleton (i.e., all elements of $M$ are equal).

Module.rank_lt_aleph0_iff theorem

: Module.rank R M < ℵ₀ ↔ Module.Finite R M

Full source

/-- See `rank_lt_aleph0` for the inverse direction without `Module.Free R M`. -/
lemma rank_lt_aleph0_iff : Module.rankModule.rank R M < ℵ₀ ↔ Module.Finite R M := by
  rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]
  exact ⟨fun h ↦ Finite.of_basis (Free.chooseBasis R M),
    fun I ↦ Finite.of_fintype (Free.ChooseBasisIndex R M)⟩

Finite Rank Characterization for Modules: $\text{rank}_R M < \aleph_0 \leftrightarrow M$ is finitely generated

Informal description

For a module $M$ over a ring $R$, the rank of $M$ is less than $\aleph_0$ if and only if $M$ is finitely generated as an $R$-module.

Module.finrank_of_not_finite theorem

(h : ¬Module.Finite R M) : finrank R M = 0

Full source

theorem finrank_of_not_finite (h : ¬Module.Finite R M) : finrank R M = 0 := by
  rw [finrank, toNat_eq_zero, ← not_lt, Module.rank_lt_aleph0_iff]
  exact .inr h

Finrank of Non-Finitely Generated Modules is Zero

Informal description

For a module $M$ over a ring $R$, if $M$ is not finitely generated, then its finrank (finite dimension) is zero.

Module.finite_of_finrank_pos theorem

(h : 0 < finrank R M) : Module.Finite R M

Full source

theorem finite_of_finrank_pos (h : 0 < finrank R M) : Module.Finite R M := by
  contrapose h
  simp [finrank_of_not_finite h]

Positive Finrank Implies Finite Generation of Modules

Informal description

For a module $M$ over a ring $R$, if the finite dimension (finrank) of $M$ is positive, then $M$ is finitely generated as an $R$-module.

Module.finite_of_finrank_eq_succ theorem

{n : ℕ} (hn : finrank R M = n.succ) : Module.Finite R M

Full source

theorem finite_of_finrank_eq_succ {n : ℕ} (hn : finrank R M = n.succ) : Module.Finite R M :=
  finite_of_finrank_pos <| by rw [hn]; exact n.succ_pos

Finite Generation of Modules with Finrank Equal to Successor of a Natural Number

Informal description

For a module $M$ over a ring $R$, if the finite dimension (finrank) of $M$ is equal to $n + 1$ for some natural number $n$, then $M$ is finitely generated as an $R$-module.

Module.finite_iff_of_rank_eq_nsmul theorem

 {W} [AddCommMonoid 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

Full source

theorem finite_iff_of_rank_eq_nsmul {W} [AddCommMonoid W] [Module R W] [Module.Free R W] {n : ℕ}
    (hn : n ≠ 0) (hVW : Module.rank R M = n • Module.rank R W) :
    Module.FiniteModule.Finite R M ↔ Module.Finite R W := by
  simp only [← rank_lt_aleph0_iff, hVW, nsmul_lt_aleph0_iff_of_ne_zero hn]

Finite Generation of Modules under Rank Scaling

Informal description

Let $R$ be a ring, and let $M$ and $W$ be free $R$-modules with $W$ also an additive commutative monoid. Suppose there exists a natural number $n \neq 0$ such that the rank of $M$ over $R$ is equal to $n$ times the rank of $W$ over $R$, i.e., $\text{rank}_R M = n \cdot \text{rank}_R W$. Then $M$ is finitely generated as an $R$-module if and only if $W$ is finitely generated as an $R$-module.

Module.finBasis definition

[Module.Finite R M] : Basis (Fin (finrank R M)) R M

Full source

/-- A finite rank free module has a basis indexed by `Fin (finrank R M)`. -/
noncomputable def finBasis [Module.Finite R M] :
    Basis (Fin (finrank R M)) R M :=
  (Module.Free.chooseBasis R M).reindex (Fintype.equivFinOfCardEq
    (finrank_eq_card_chooseBasisIndex R M).symm)

Basis of a finite-rank free module indexed by its dimension

Informal description

For a finite-rank free module $ M $ over a ring $ R $, there exists a basis indexed by the finite type $ \text{Fin } (\text{finrank } R M) $, where $ \text{finrank } R M $ is the dimension of $ M $ as an $ R $-module.

Module.finBasisOfFinrankEq definition

[Module.Finite R M] {n : ℕ} (hn : finrank R M = n) : Basis (Fin n) R M

Full source

/-- A rank `n` free module has a basis indexed by `Fin n`. -/
noncomputable def finBasisOfFinrankEq [Module.Finite R M] {n : ℕ} (hn : finrank R M = n) :
    Basis (Fin n) R M := (finBasis R M).reindex (finCongr hn)

Basis of a finite-rank free module indexed by its dimension $ n $

Informal description

Given a finite-rank free module $ M $ over a ring $ R $ and a natural number $ n $ such that the dimension of $ M $ is $ n $, there exists a basis of $ M $ indexed by the finite type $ \text{Fin } n $.

Module.basisUnique definition

(ι : Type*) [Unique ι] (h : finrank R M = 1) : Basis ι R M

Full source

/-- A free module with rank 1 has a basis with one element. -/
noncomputable def basisUnique (ι : Type*) [Unique ι]
    (h : finrank R M = 1) :
    Basis ι R M :=
  haveI : Module.Finite R M :=
    Module.finite_of_finrank_pos (_root_.zero_lt_one.trans_le h.symm.le)
  (finBasisOfFinrankEq R M h).reindex (Equiv.ofUnique _ _)

Basis of a rank 1 free module indexed by a unique type

Informal description

Given a type `ι` with exactly one element and a free module `M` over a ring `R` with dimension 1, there exists a basis of `M` indexed by `ι`. This basis is constructed by reindexing the basis obtained from `Module.finBasisOfFinrankEq` using the unique equivalence between `Fin 1` and `ι`.

Module.basisUnique_repr_eq_zero_iff theorem

{ι : Type*} [Unique ι] {h : finrank R M = 1} {v : M} {i : ι} : (basisUnique ι h).repr v i = 0 ↔ v = 0

Full source

@[simp]
theorem basisUnique_repr_eq_zero_iff {ι : Type*} [Unique ι]
    {h : finrank R M = 1} {v : M} {i : ι} :
    (basisUnique ι h).repr v i = 0 ↔ v = 0 :=
  ⟨fun hv =>
    (basisUnique ι h).repr.map_eq_zero_iff.mp (Finsupp.ext fun j => Subsingleton.elim i j ▸ hv),
    fun hv => by rw [hv, LinearEquiv.map_zero, Finsupp.zero_apply]⟩

Vanishing of coefficients in a rank-1 free module's unique basis representation

Informal description

Let $R$ be a ring, $M$ a free $R$-module of dimension $1$, and $\iota$ a type with a unique element. For any vector $v \in M$ and index $i \in \iota$, the coefficient of $v$ with respect to the unique basis indexed by $\iota$ is zero if and only if $v$ is the zero vector. In other words, for the basis $\mathcal{B}$ obtained from `basisUnique`, we have $\mathcal{B}^*(v)_i = 0 \leftrightarrow v = 0$.

Algebra.instFiniteOfIsQuadraticExtension instance

 (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S] [IsQuadraticExtension R S] :
  Module.Finite R S

Full source

instance (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S]
    [IsQuadraticExtension R S] :
    Module.Finite R S := finite_of_finrank_eq_succ <| IsQuadraticExtension.finrank_eq_two R S

Finite Generation of Quadratic Extensions over Strong Rank Condition Rings

Informal description

For a commutative semiring $R$ satisfying the strong rank condition, and a semiring $S$ that is a quadratic extension of $R$ via an algebra structure, the module $S$ is finitely generated over $R$.

Main result