Projective modules #
This file contains a definition of a projective module, the proof that our definition is equivalent to a lifting property, and the proof that all free modules are projective.
Main definitions #
R be a ring (or a semiring) and let
M be an
is_projective R M: the proposition saying that
Mis a projective
Main theorems #
is_projective.lifting_property: a map from a projective module can be lifted along a surjection.
is_projective.of_lifting_property: If for all R-module surjections
A →ₗ B, all maps
M →ₗ Blift to
M →ₗ A, then
is_projective.of_free: Free modules are projective
Implementation notes #
The actual definition of projective we use is that the natural R-module map from the free R-module on the type M down to M splits. This is more convenient than certain other definitions which involve quantifying over universes, and also universe-polymorphic (the ring and module can be in different universes).
Everything works for semirings and modules except that apparently we don't have free modules over semirings, so here we stick to rings.
- Direct sum of two projective modules is projective.
- Arbitrary sum of projective modules is projective.
- Any module admits a surjection from a projective module.
All of these should be relatively straightforward.
An R-module is projective if it is a direct summand of a free module, or equivalently if maps from the module lift along surjections. There are several other equivalent definitions.
A projective R-module has the property that maps from it lift along surjections.
A module which satisfies the universal property is projective. Note that the universe variables
huniv are somewhat restricted.