The functor of forming finitely supported functions on a type with values in a [Ring R]
is the left adjoint of
the forgetful functor from R
-modules to types.
The free functor Type u ⥤ ModuleCat R
sending a type X
to the
free R
-module with generators x : X
, implemented as the type X →₀ R
.
Instances For
The free-forgetful adjunction for R-modules.
Instances For
(Implementation detail) The unitor for Free R
.
Instances For
(Implementation detail) The tensorator for Free R
.
Instances For
The free R-module functor is lax monoidal.
The free functor Type u ⥤ ModuleCat R
, as a monoidal functor.
Instances For
Consider an object of C
as an object of the R
-linear completion.
It may be preferable to use (Free.embedding R C).obj X
instead;
this functor can also be used to lift morphisms.
Instances For
A category embeds into its R
-linear completion.
Instances For
A functor to an R
-linear category lifts to a functor from its R
-linear completion.
Instances For
The embedding into the R
-linear completion, followed by the lift,
is isomorphic to the original functor.
Instances For
Two R
-linear functors out of the R
-linear completion are isomorphic iff their
compositions with the embedding functor are isomorphic.
Instances For
Free.lift
is unique amongst R
-linear functors Free R C ⥤ D
which compose with embedding ℤ C
to give the original functor.