mathlib documentation

algebra.category.Module.adjunctions

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.

def Module.free (R : Type u) [ring R] :
Type u Module R

The free functor Type u ⥤ Module R sending a type X to the free R-module with generators x : X, implemented as the type X →₀ R.

Equations
@[simp]
theorem Module.free_obj (R : Type u) [ring R] (X : Type u) :
@[simp]
theorem Module.free_map (R : Type u) [ring R] (X Y : Type u) (f : X Y) :

The free-forgetful adjunction for R-modules.

Equations