# 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.

source
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] [Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [Free S N] :
Free S (M →ₗ[R] N)
source
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] [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)
source
theorem Module.rank_linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [StrongRankCondition R] [StrongRankCondition S] [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)
source
theorem Module.finrank_linearMap (R : Type u) (S : Type u') (M : Type v) (N : Type w) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N] [StrongRankCondition R] [StrongRankCondition S] [Free S N] :
finrank S (M →ₗ[R] N) = finrank R M * finrank S N

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

source
theorem Module.rank_linearMap_self (R : Type u) (S : Type u') (M : Type v) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [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)
source
theorem Module.finrank_linearMap_self (R : Type u) (S : Type u') (M : Type v) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Free R M] [Module.Finite R M] [StrongRankCondition R] [StrongRankCondition S] [Module R S] [SMulCommClass R S S] :
finrank S (M →ₗ[R] S) = finrank R M
source
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)
source
theorem cardinalMk_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)
source
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) ≤ Module.finrank K M

Stacks Tag 09HS

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