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
@[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]
Equations
@[simp]
theorem category_theory.Free.single_comp_single (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] {X Y Z : C} (f : X Y) (g : Y Z) (r s : R) :

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) [category_theory.category C] (X : C) :
@[simp]
theorem category_theory.Free.embedding_map (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] (X Y : C) (f : X Y) :
@[simp]
theorem category_theory.Free.lift_map (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C D) (X Y : category_theory.Free R C) (f : X Y) :
(category_theory.Free.lift R F).map f = finsupp.sum f (λ (f' : X Y) (r : R), r F.map f')

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

Equations
@[simp]
theorem category_theory.Free.lift_map_single (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C D) {X Y : C} (f : X Y) (r : R) :

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

Equations
@[ext]

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

Equations

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

Equations