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.

noncomputable 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) :
noncomputable def Module.adj (R : Type u) [ring R] :

The free-forgetful adjunction for R-modules.

Equations
noncomputable def Module.free.ε (R : Type u) [comm_ring R] :
𝟙_ (Module R) (Module.free R).obj (𝟙_ (Type u))

(Implementation detail) The unitor for free R.

Equations
@[simp]
theorem Module.free.ε_apply (R : Type u) [comm_ring R] (r : R) :
noncomputable def Module.free.μ (R : Type u) [comm_ring R] (α β : Type u) :
(Module.free R).obj α (Module.free R).obj β (Module.free R).obj β)

(Implementation detail) The tensorator for free R.

Equations
theorem Module.free.μ_natural (R : Type u) [comm_ring R] {X Y X' Y' : Type u} (f : X Y) (g : X' Y') :
theorem Module.free.left_unitality (R : Type u) [comm_ring R] (X : Type u) :
theorem Module.free.right_unitality (R : Type u) [comm_ring R] (X : Type u) :
theorem Module.free.associativity (R : Type u) [comm_ring R] (X Y Z : Type u) :
@[protected, 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
Instances for category_theory.Free
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.

It may be preferable to use (Free.embedding R C).obj X instead; this functor can also be used to lift morphisms.

Equations
@[protected, instance]
Equations
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) :
noncomputable def category_theory.Free.embedding (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] :

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 an R-linear category lifts to a functor from its R-linear completion.

Equations
Instances for category_theory.Free.lift
@[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