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.

@[simp]

theorem ModuleCat.free_map (R : Type u) [Ring R] {X : Type u} {Y : Type u} (f : X ⟶ Y) : (ModuleCat.free R).map f = Finsupp.lmapDomain R R f

@[simp]

theorem ModuleCat.free_obj (R : Type u) [Ring R] (X : Type u) : (ModuleCat.free R).obj X = ModuleCat.of R (X →₀ R)

def ModuleCat.free (R : Type u) [Ring R] : CategoryTheory.Functor (Type u) (ModuleCat R)

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.

def ModuleCat.adj (R : Type u) [Ring R] : ModuleCat.free R ⊣ CategoryTheory.forget (ModuleCat R)

The free-forgetful adjunction for R-modules.

instance ModuleCat.instIsRightAdjointTypeTypesModuleCatModuleCategoryForgetModuleConcreteCategory (R : Type u) [Ring R] : CategoryTheory.IsRightAdjoint (CategoryTheory.forget (ModuleCat R))

def ModuleCat.Free.ε (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategory.tensorUnit (ModuleCat R) ⟶ (ModuleCat.free R).obj (CategoryTheory.MonoidalCategory.tensorUnit (Type u))

(Implementation detail) The unitor for Free R.

@[simp]

theorem ModuleCat.Free.ε_apply (R : Type u) [CommRing R] (r : R) : ↑(ModuleCat.Free.ε R) r = fun₀ | PUnit.unit => r

def ModuleCat.Free.μ (R : Type u) [CommRing R] (α : Type u) (β : Type u) : CategoryTheory.MonoidalCategory.tensorObj ((ModuleCat.free R).obj α) ((ModuleCat.free R).obj β) ≅ (ModuleCat.free R).obj (CategoryTheory.MonoidalCategory.tensorObj α β)

(Implementation detail) The tensorator for Free R.

theorem ModuleCat.Free.μ_natural (R : Type u) [CommRing R] {X : Type u} {Y : Type u} {X' : Type u} {Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ((ModuleCat.free R).map f) ((ModuleCat.free R).map g)) (ModuleCat.Free.μ R Y Y').hom = CategoryTheory.CategoryStruct.comp (ModuleCat.Free.μ R X X').hom ((ModuleCat.free R).map (CategoryTheory.MonoidalCategory.tensorHom f g))

theorem ModuleCat.Free.left_unitality (R : Type u) [CommRing R] (X : Type u) : (CategoryTheory.MonoidalCategory.leftUnitor ((ModuleCat.free R).obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (ModuleCat.Free.ε R) (CategoryTheory.CategoryStruct.id ((ModuleCat.free R).obj X))) (CategoryTheory.CategoryStruct.comp (ModuleCat.Free.μ R (CategoryTheory.MonoidalCategory.tensorUnit (Type u)) X).hom (CategoryTheory.map (ModuleCat.free R).toPrefunctor.obj (CategoryTheory.MonoidalCategory.leftUnitor X).hom))

theorem ModuleCat.Free.right_unitality (R : Type u) [CommRing R] (X : Type u) : (CategoryTheory.MonoidalCategory.rightUnitor ((ModuleCat.free R).obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((ModuleCat.free R).obj X)) (ModuleCat.Free.ε R)) (CategoryTheory.CategoryStruct.comp (ModuleCat.Free.μ R X (CategoryTheory.MonoidalCategory.tensorUnit (Type u))).hom (CategoryTheory.map (ModuleCat.free R).toPrefunctor.obj (CategoryTheory.MonoidalCategory.rightUnitor X).hom))

theorem ModuleCat.Free.associativity (R : Type u) [CommRing R] (X : Type u) (Y : Type u) (Z : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (ModuleCat.Free.μ R X Y).hom (CategoryTheory.CategoryStruct.id ((ModuleCat.free R).obj Z))) (CategoryTheory.CategoryStruct.comp (ModuleCat.Free.μ R (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.map (ModuleCat.free R).toPrefunctor.obj (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator ((ModuleCat.free R).obj X) ((ModuleCat.free R).obj Y) ((ModuleCat.free R).obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((ModuleCat.free R).obj X)) (ModuleCat.Free.μ R Y Z).hom) (ModuleCat.Free.μ R X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom)

@[simp]

theorem ModuleCat.Free.instLaxMonoidalTypeTypesTypesMonoidalModuleCatToRingModuleCategoryMonoidalCategoryObjToQuiverToCategoryStructToPrefunctorFreeInstFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor_μ (R : Type u) [CommRing R] (X : Type u) (Y : Type u) : CategoryTheory.LaxMonoidal.μ X Y = (ModuleCat.Free.μ R X Y).hom

@[simp]

theorem ModuleCat.Free.instLaxMonoidalTypeTypesTypesMonoidalModuleCatToRingModuleCategoryMonoidalCategoryObjToQuiverToCategoryStructToPrefunctorFreeInstFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor_ε (R : Type u) [CommRing R] : CategoryTheory.LaxMonoidal.ε = ModuleCat.Free.ε R

instance ModuleCat.Free.instLaxMonoidalTypeTypesTypesMonoidalModuleCatToRingModuleCategoryMonoidalCategoryObjToQuiverToCategoryStructToPrefunctorFreeInstFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor (R : Type u) [CommRing R] : CategoryTheory.LaxMonoidal (ModuleCat.free R).toPrefunctor.obj

The free R-module functor is lax monoidal.

instance ModuleCat.Free.instIsIsoModuleCatToRingModuleCategoryTensorUnitMonoidalCategoryObjTypeToQuiverToCategoryStructTypesToPrefunctorFreeTypesMonoidalεInstFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorInstLaxMonoidalTypeTypesTypesMonoidalModuleCatToRingModuleCategoryMonoidalCategoryObjToQuiverToCategoryStructToPrefunctorFreeInstFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor (R : Type u) [CommRing R] : CategoryTheory.IsIso CategoryTheory.LaxMonoidal.ε

def ModuleCat.monoidalFree (R : Type u) [CommRing R] : CategoryTheory.MonoidalFunctor (Type u) (ModuleCat R)

The free functor Type u ⥤ ModuleCat R, as a monoidal functor.

def CategoryTheory.Free : Type u_1 → Type u → Type u

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

def CategoryTheory.Free.of (R : Type u_1) {C : Type u} (X : C) : CategoryTheory.Free R 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.

instance CategoryTheory.categoryFree (R : Type u_1) [CommRing R] (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{max v u_1, u} (CategoryTheory.Free R C)

instance CategoryTheory.Free.instPreadditiveFreeCategoryFree (R : Type u_1) [CommRing R] (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Preadditive (CategoryTheory.Free R C)

instance CategoryTheory.Free.instLinearToSemiringToCommSemiringFreeCategoryFreeInstPreadditiveFreeCategoryFree (R : Type u_1) [CommRing R] (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Linear R (CategoryTheory.Free R C)

theorem CategoryTheory.Free.single_comp_single (R : Type u_1) [CommRing R] (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r : R) (s : R) : (CategoryTheory.CategoryStruct.comp (fun₀ | f => r) fun₀ | g => s) = fun₀ | CategoryTheory.CategoryStruct.comp f g => r * s

@[simp]

theorem CategoryTheory.Free.embedding_map (R : Type u_1) [CommRing R] (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.Free.embedding R C).map f = fun₀ | f => 1

@[simp]

theorem CategoryTheory.Free.embedding_obj (R : Type u_1) [CommRing R] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Free.embedding R C).obj X = X

def CategoryTheory.Free.embedding (R : Type u_1) [CommRing R] (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (CategoryTheory.Free R C)

A category embeds into its R-linear completion.

@[simp]

theorem CategoryTheory.Free.lift_map (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) {X : CategoryTheory.Free R C} {Y : CategoryTheory.Free R C} (f : X ⟶ Y) : (CategoryTheory.Free.lift R F).map f = Finsupp.sum f fun f' r => r • F.map f'

@[simp]

theorem CategoryTheory.Free.lift_obj (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.Free R C) : (CategoryTheory.Free.lift R F).obj X = F.obj X

def CategoryTheory.Free.lift (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Free R C) D

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

theorem CategoryTheory.Free.lift_map_single (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (r : R) : ((CategoryTheory.Free.lift R F).map fun₀ | f => r) = r • F.map f

instance CategoryTheory.Free.lift_additive (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor.Additive (CategoryTheory.Free.lift R F)

instance CategoryTheory.Free.lift_linear (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor.Linear R (CategoryTheory.Free.lift R F)

def CategoryTheory.Free.embeddingLiftIso (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor.comp (CategoryTheory.Free.embedding R C) (CategoryTheory.Free.lift R F) ≅ F

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

def CategoryTheory.Free.ext (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] {F : CategoryTheory.Functor (CategoryTheory.Free R C) D} {G : CategoryTheory.Functor (CategoryTheory.Free R C) D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Linear R F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Linear R G] (α : CategoryTheory.Functor.comp (CategoryTheory.Free.embedding R C) F ≅ CategoryTheory.Functor.comp (CategoryTheory.Free.embedding R C) G) : F ≅ G

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

def CategoryTheory.Free.liftUnique (R : Type u_1) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) (L : CategoryTheory.Functor (CategoryTheory.Free R C) D) [CategoryTheory.Functor.Additive L] [CategoryTheory.Functor.Linear R L] (α : CategoryTheory.Functor.comp (CategoryTheory.Free.embedding R C) L ≅ F) : L ≅ CategoryTheory.Free.lift R F

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