Free module

Free modules are the free objects in . #m/def/module Departing from classical tradition, we call a module equipped with an isomorphism from a free module a framed module, while a module for which there merely exists such an isomorphism is a framable module. Assuming the Axiom of Choice, any module over a division ring is framable: See Assuming choice, every vector space has a basis.

Notation

In these notes, we have two conventions for the free module over generated by a set . The first is

where we think of elements as maps of finite support , and we identify with . The second is

which allows for the explicit naming of the basis to be used.

Being framable is equivalent to the existence of a basis, where by a basis for an -module , we mean an -spanning set such that each is given by a unique -linear combination of elements.

Universal property

Let be a ring and be a set. The free module is a pair consisting of an -module and a function such that given any -module and function there exists a unique module homomorphism such that the following diagram commutes

This has a unique extension to a functor such that

becomes a natural transformation.

Monoidal functor

When is a commutative ring this forms a monoidal functor with respect to the cartesian structure on and the tensor product on . #m/thm/cat If in , then we let

Construction as maps

Let be a set and be a ring. The free module is the set of maps of finite support with addition and scaling induced by those of , #m/def/module
i.e. for all

where we identify with invoking an Iverson bracket.

Proof of universal property

Clearly as constructed is an -module with basis Now let be an -module and be a function. For a module homomorphism to make the diagram commute, we require that for all , which fully specifies so that for

as required.

Properties

carries the additional structure of an -comonoid, namely the Free -comonoid

#state/tidy | #lang/en | #SemBr