# mathlibdocumentation

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

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) :
(Module.free R).obj X = (X →₀ R)
@[simp]
theorem Module.free_map (R : Type u) [ring R] (X Y : Type u) (f : X Y) :
(Module.free R).map f = f
def Module.adj (R : Type u) [ring R] :

The free-forgetful adjunction for R-modules.

Equations
@[instance]
Equations
@[instance]

The free R-module functor is lax monoidal.

Equations
@[nolint]
def category_theory.Free (R : Type u_1) (C : Type u) :
Type u

Free R C is a type synonym for C, which, given [comm_ring R] and [category C], we will equip with a category structure where the morphisms are formal R-linear combinations of the morphisms in C.

Equations
def category_theory.Free.of (R : Type u_1) {C : Type u} (X : C) :

Consider an object of C as an object of the R-linear completion.

Equations
@[instance]
def category_theory.category_Free (R : Type u_1) [comm_ring R] (C : Type u)  :
Equations
@[simp]
theorem category_theory.Free.single_comp_single (R : Type u_1) [comm_ring R] (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (r s : R) :
= finsupp.single (f g) (r * s)
@[instance]
def category_theory.Free.category_theory.preadditive (R : Type u_1) [comm_ring R] (C : Type u)  :
Equations
@[instance]
def category_theory.Free.category_theory.linear (R : Type u_1) [comm_ring R] (C : Type u)  :
Equations
def category_theory.Free.embedding (R : Type u_1) [comm_ring R] (C : Type u)  :

A category embeds into its R-linear completion.

Equations
@[simp]
theorem category_theory.Free.embedding_obj (R : Type u_1) [comm_ring R] (C : Type u) (X : C) :
= X
@[simp]
theorem category_theory.Free.embedding_map (R : Type u_1) [comm_ring R] (C : Type u) (X Y : C) (f : X Y) :
=
@[simp]
theorem category_theory.Free.lift_map (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) (X Y : C) (f : X Y) :
.map f = (λ (f' : X Y) (r : R), r F.map f')
def category_theory.Free.lift (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) :

A functor to a preadditive category lifts to a functor from its R-linear completion.

Equations
@[simp]
theorem category_theory.Free.lift_obj (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) (X : C) :
.obj X = F.obj X
@[simp]
theorem category_theory.Free.lift_map_single (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) {X Y : C} (f : X Y) (r : R) :
.map r) = r F.map f
@[instance]
def category_theory.Free.lift_additive (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) :
@[instance]
def category_theory.Free.lift_linear (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) :
def category_theory.Free.embedding_lift_iso (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) :

The embedding into the R-linear completion, followed by the lift, is isomorphic to the original functor.

Equations
@[ext]
def category_theory.Free.ext (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} {F G : D} [F.additive] [G.additive] (α : ) :
F G

Two R-linear functors out of the R-linear completion are isomorphic iff their compositions with the embedding functor are isomorphic.

Equations
def category_theory.Free.lift_unique (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) (L : D) [L.additive] (α : F) :

Free.lift is unique amongst R-linear functors Free R C ⥤ D which compose with embedding ℤ C to give the original functor.

Equations