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) (M : Type v) (N : Type w) [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup N] [Module R N] [Module.Free R N] [Module.Finite R M] [Module.Finite R N] : Module.Free R (M →ₗ[R] N)

Equations

• (_ : Module.Free R (M →ₗ[R] N)) = (_ : Module.Free R (M →ₗ[R] N))

instance Module.Finite.linearMap {R : Type u} (M : Type v) (N : Type w) [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup N] [Module R N] [Module.Free R N] [Module.Finite R M] [Module.Finite R N] : Module.Finite R (M →ₗ[R] N)

Equations

• (_ : Module.Finite R (M →ₗ[R] N)) = (_ : Module.Finite R (M →ₗ[R] N))

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

Equations

• (_ : Module.Finite ℤ (M →+ N)) = (_ : Module.Finite ℤ (M →+ N))

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

Equations

• (_ : Module.Free ℤ (M →+ N)) = (_ : Module.Free ℤ (M →+ N))

theorem FiniteDimensional.finrank_linearMap (R : Type u) (M : Type v) (N : Type w) [CommRing 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 →ₗ[R] N) = FiniteDimensional.finrank R M * FiniteDimensional.finrank R N

The finrank of M →ₗ[R] N is (finrank R M) * (finrank R N).

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