Projective modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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).
We require that the module sits in at least as high a universe as the ring: without this, free modules don't even exist, and it's unclear if projective modules are even a useful notion.
- Direct sum of two projective modules is projective.
- Arbitrary sum of projective modules is projective.
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.