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.

instance Module.Free.linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [Module.Free S N] : Module.Free S (M →ₗ[R] N)

Equations

• ⋯ = ⋯

instance Module.Finite.linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [Module.Finite S N] : Module.Finite S (M →ₗ[R] N)

Equations

• ⋯ = ⋯

theorem FiniteDimensional.rank_linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [StrongRankCondition R] [StrongRankCondition S] [Module.Free S N] : Module.rank S (M →ₗ[R] N) = Cardinal.lift.{w, v} (Module.rank R M) * Cardinal.lift.{v, w} (Module.rank S N)

theorem FiniteDimensional.finrank_linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [StrongRankCondition R] [StrongRankCondition S] [Module.Free S N] : FiniteDimensional.finrank S (M →ₗ[R] N) = FiniteDimensional.finrank R M * FiniteDimensional.finrank S N

The finrank of M →ₗ[R] N as an S-module is (finrank R M) * (finrank S N).

theorem FiniteDimensional.rank_linearMap_self (R : Type u) (S : Type u') (M : Type v) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [StrongRankCondition R] [StrongRankCondition S] [Module R S] [SMulCommClass R S S] : Module.rank S (M →ₗ[R] S) = Cardinal.lift.{u', v} (Module.rank R M)

theorem FiniteDimensional.finrank_linearMap_self (R : Type u) (S : Type u') (M : Type v) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [StrongRankCondition R] [StrongRankCondition S] [Module R S] [SMulCommClass R S S] : FiniteDimensional.finrank S (M →ₗ[R] S) = FiniteDimensional.finrank R M

instance Finite.algHom (K : Type u_1) (M : Type u_2) (L : Type v) [CommRing K] [Ring M] [Algebra K M] [Module.Free K M] [Module.Finite K M] [CommRing L] [IsDomain L] [Algebra K L] : Finite (M →ₐ[K] L)

Equations

• ⋯ = ⋯

theorem cardinal_mk_algHom_le_rank (K : Type u_1) (M : Type u_2) (L : Type v) [CommRing K] [Ring M] [Algebra K M] [Module.Free K M] [Module.Finite K M] [CommRing L] [IsDomain L] [Algebra K L] : Cardinal.mk (M →ₐ[K] L) ≤ Cardinal.lift.{v, u_2} (Module.rank K M)

theorem card_algHom_le_finrank (K : Type u_1) (M : Type u_2) (L : Type v) [CommRing K] [Ring M] [Algebra K M] [Module.Free K M] [Module.Finite K M] [CommRing L] [IsDomain L] [Algebra K L] : Nat.card (M →ₐ[K] L) ≤ FiniteDimensional.finrank K M

instance Module.Finite.addMonoidHom (M : Type v) (N : Type w) [AddCommGroup M] [Module.Finite ℤ M] [Module.Free ℤ M] [AddCommGroup N] [Module.Finite ℤ N] : Module.Finite ℤ (M →+ N)

Equations

• ⋯ = ⋯

instance Module.Free.addMonoidHom (M : Type v) (N : Type w) [AddCommGroup M] [Module.Finite ℤ M] [Module.Free ℤ M] [AddCommGroup N] [Module.Free ℤ N] : Module.Free ℤ (M →+ N)

Equations

• ⋯ = ⋯

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