Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Module docstring

{"# Finite and free modules using matrices

We provide some instances for finite and free modules involving matrices.

Main results

Module.Free.linearMap : if M and N are finite and free, then M →ₗ[R] N is free.
Module.Finite.ofBasis : A free module with a basis indexed by a Fintype is finite.
Module.Finite.linearMap : if M and N are finite and free, then M →ₗ[R] N is finite. "}

Module.Free.linearMap instance

[Module.Free S N] : Module.Free S (M →ₗ[R] N)

Full source

instance Module.Free.linearMap [Module.Free S N] : Module.Free S (M →ₗ[R] N) :=
  Module.Free.of_equiv (linearMapEquivFun R S M N).symm

Freeness of Linear Maps between Free Modules

Informal description

For any free module $N$ over a semiring $S$, the space of linear maps $M \to N$ over a ring $R$ is also a free $S$-module.

Module.Finite.linearMap instance

[Module.Finite S N] : Module.Finite S (M →ₗ[R] N)

Full source

instance Module.Finite.linearMap [Module.Finite S N] : Module.Finite S (M →ₗ[R] N) :=
  Module.Finite.equiv (linearMapEquivFun R S M N).symm

Finitely Generated Module of Linear Maps from $M$ to a Finitely Generated $N$

Informal description

For any finitely generated module $N$ over a semiring $S$, the space of linear maps $M \to N$ over a ring $R$ is also finitely generated as an $S$-module.

Module.rank_linearMap theorem

: Module.rank S (M →ₗ[R] N) = lift.{w} (Module.rank R M) * lift.{v} (Module.rank S N)

Full source

theorem Module.rank_linearMap :
    Module.rank S (M →ₗ[R] N) = lift.{w} (Module.rank R M) * lift.{v} (Module.rank S N) := by
  rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
    ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]

Rank of Linear Maps: $\text{rank}_S(M \to_R N) = \text{rank}_R M \cdot \text{rank}_S N$

Informal description

Let $R$ and $S$ be rings, and let $M$ be an $R$-module and $N$ be an $S$-module. The rank of the $S$-module of linear maps from $M$ to $N$ is equal to the product of the lifted ranks of $M$ as an $R$-module and $N$ as an $S$-module, i.e., \[ \text{rank}_S (M \to_{R} N) = \text{rank}_R M \cdot \text{rank}_S N, \] where the ranks are lifted to appropriate cardinal universes.

Module.finrank_linearMap theorem

: finrank S (M →ₗ[R] N) = finrank R M * finrank S N

Full source

/-- The finrank of `M →ₗ[R] N` as an `S`-module is `(finrank R M) * (finrank S N)`. -/
theorem Module.finrank_linearMap :
    finrank S (M →ₗ[R] N) = finrank R M * finrank S N := by
  simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]

Finite Rank of Linear Maps: $\text{finrank}_S(M \to_R N) = \text{finrank}_R M \cdot \text{finrank}_S N$

Informal description

Let $R$ and $S$ be rings, and let $M$ be a finite-rank $R$-module and $N$ be a finite-rank $S$-module. The finite rank of the $S$-module of linear maps from $M$ to $N$ is equal to the product of the finite ranks of $M$ as an $R$-module and $N$ as an $S$-module, i.e., \[ \text{finrank}_S (M \to_{R} N) = \text{finrank}_R M \cdot \text{finrank}_S N. \]

Module.rank_linearMap_self theorem

: Module.rank S (M →ₗ[R] S) = lift.{u'} (Module.rank R M)

Full source

theorem Module.rank_linearMap_self :
    Module.rank S (M →ₗ[R] S) = lift.{u'} (Module.rank R M) := by
  rw [rank_linearMap, rank_self, lift_one, mul_one]

Rank of Linear Maps to the Base Ring: $\text{rank}_S(M \to_R S) = \text{rank}_R M$

Informal description

Let $R$ and $S$ be rings, and let $M$ be an $R$-module. The rank of the $S$-module of linear maps from $M$ to $S$ is equal to the lifted rank of $M$ as an $R$-module, i.e., \[ \text{rank}_S (M \to_{R} S) = \text{rank}_R M, \] where the rank is lifted to an appropriate cardinal universe.

Module.finrank_linearMap_self theorem

: finrank S (M →ₗ[R] S) = finrank R M

Full source

theorem Module.finrank_linearMap_self : finrank S (M →ₗ[R] S) = finrank R M := by
  rw [finrank_linearMap, finrank_self, mul_one]

Finite Rank Identity for Linear Maps to Base Ring: $\text{finrank}_S(M \to_R S) = \text{finrank}_R M$

Informal description

Let $R$ and $S$ be rings, and let $M$ be a finite-rank $R$-module. The finite rank of the $S$-module of linear maps from $M$ to $S$ is equal to the finite rank of $M$ as an $R$-module, i.e., \[ \text{finrank}_S (M \to_R S) = \text{finrank}_R M. \]

Finite.algHom instance

: Finite (M →ₐ[K] L)

Full source

instance Finite.algHom : Finite (M →ₐ[K] L) :=
  (linearIndependent_algHom_toLinearMap K M L).finite

Finiteness of Algebra Homomorphisms from Finite-Dimensional Algebras

Informal description

For any field extension $L/K$ and finite-dimensional $K$-algebra $M$, the set of $K$-algebra homomorphisms from $M$ to $L$ is finite.

cardinalMk_algHom_le_rank theorem

: #(M →ₐ[K] L) ≤ lift.{v} (Module.rank K M)

Full source

theorem cardinalMk_algHom_le_rank : #(M →ₐ[K] L) ≤ lift.{v} (Module.rank K M) := by
  convert (linearIndependent_algHom_toLinearMap K M L).cardinal_lift_le_rank
  · rw [lift_id]
  · have := Module.nontrivial K L
    rw [lift_id, Module.rank_linearMap_self]

Cardinality Bound for Algebra Homomorphisms: $\#(M \to_K L) \leq \text{rank}_K M$

Informal description

Let $K$ be a field, $L$ a field extension of $K$, and $M$ a $K$-algebra. The cardinality of the set of $K$-algebra homomorphisms from $M$ to $L$ is bounded above by the rank of $M$ as a $K$-module (lifted to an appropriate cardinal universe), i.e., \[ \#(M \to_{K} L) \leq \text{rank}_K M. \]

card_algHom_le_finrank theorem

: Nat.card (M →ₐ[K] L) ≤ finrank K M

Full source

@[stacks 09HS]
theorem card_algHom_le_finrank : Nat.card (M →ₐ[K] L) ≤ finrank K M := by
  convert toNat_le_toNat (cardinalMk_algHom_le_rank K M L) ?_
  · rw [toNat_lift, finrank]
  · rw [lift_lt_aleph0]; have := Module.nontrivial K L; apply Module.rank_lt_aleph0

Cardinality Bound for Algebra Homomorphisms: $\text{card}(M \to_K L) \leq \text{finrank}_K M$

Informal description

For a field extension $L/K$ and a finite-dimensional $K$-algebra $M$, the cardinality of the set of $K$-algebra homomorphisms from $M$ to $L$ is bounded above by the finite rank of $M$ as a $K$-module, i.e., \[ \text{card}(M \to_{K} L) \leq \text{finrank}_K M. \]

Module.Finite.addMonoidHom instance

[Module.Finite ℤ N] : Module.Finite ℤ (M →+ N)

Full source

instance Module.Finite.addMonoidHom [Module.Finite ℤ N] : Module.Finite ℤ (M →+ N) :=
  Module.Finite.equiv (addMonoidHomLequivInt ℤ).symm

Finitely Generated Module of Additive Group Homomorphisms to a Finitely Generated Module

Informal description

For any finitely generated $\mathbb{Z}$-module $N$, the space of additive group homomorphisms $M \to N$ is also finitely generated as a $\mathbb{Z}$-module.

Module.Free.addMonoidHom instance

[Module.Free ℤ N] : Module.Free ℤ (M →+ N)

Full source

instance Module.Free.addMonoidHom [Module.Free ℤ N] : Module.Free ℤ (M →+ N) :=
  letI : Module.Free ℤ (M →ₗ[ℤ] N) := Module.Free.linearMap _ _ _ _
  Module.Free.of_equiv (addMonoidHomLequivInt ℤ).symm

Freeness of Additive Group Homomorphisms to a Free Module

Informal description

For any free $\mathbb{Z}$-module $N$, the space of additive group homomorphisms $M \to N$ is also a free $\mathbb{Z}$-module.

Matrix.rank_vecMulVec theorem

 {K m n : Type u} [CommRing K] [Fintype n] [DecidableEq n] (w : m → K) (v : n → K) :
  (Matrix.vecMulVec w v).toLin'.rank ≤ 1

Full source

theorem Matrix.rank_vecMulVec {K m n : Type u} [CommRing K] [Fintype n]
    [DecidableEq n] (w : m → K) (v : n → K) : (Matrix.vecMulVec w v).toLin'.rank ≤ 1 := by
  nontriviality K
  rw [Matrix.vecMulVec_eq (Fin 1), Matrix.toLin'_mul]
  refine le_trans (LinearMap.rank_comp_le_left _ _) ?_
  refine (LinearMap.rank_le_domain _).trans_eq ?_
  rw [rank_fun', Fintype.card_ofSubsingleton, Nat.cast_one]

Rank of Outer Product Matrix is at Most One

Informal description

Let $K$ be a commutative ring, and let $m$ and $n$ be finite types with $n$ decidable. For any vectors $w \colon m \to K$ and $v \colon n \to K$, the rank of the linear map associated with the outer product matrix $\text{vecMulVec}(w, v)$ is at most $1$.