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.

Equations

• One or more equations did not get rendered due to their size.

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

The free-forgetful adjunction for R-modules.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ModuleCat.instIsRightAdjointTypeTypesModuleCatModuleCategoryForgetModuleConcreteCategory R = { left := ModuleCat.free R, adj := ModuleCat.adj R }

def ModuleCat.Free.ε (R : Type u) [CommRing R] : 𝟙_ (ModuleCat R) ⟶ (ModuleCat.free R).obj (𝟙_ (Type u))

(Implementation detail) The unitor for Free R.

Equations

• ModuleCat.Free.ε R = Finsupp.lsingle PUnit.unit

@[simp]

theorem ModuleCat.Free.ε_apply (R : Type u) [CommRing R] (r : R) : (ModuleCat.Free.ε R) r = Finsupp.single 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.

Equations

• ModuleCat.Free.μ R α β = LinearEquiv.toModuleIso (finsuppTensorFinsupp' 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 (𝟙_ (Type u)) X).hom (CategoryTheory.map (ModuleCat.free R).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 (𝟙_ (Type u))).hom (CategoryTheory.map (ModuleCat.free R).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).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.instLaxMonoidalTypeTypesInstMonoidalCategoryTypesChosenFiniteProductsModuleCatToRingModuleCategoryMonoidalCategoryObjToQuiverToCategoryStructToPrefunctorFreeInstFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor_ε (R : Type u) [CommRing R] : CategoryTheory.LaxMonoidal.ε = ModuleCat.Free.ε R

@[simp]

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

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

The free R-module functor is lax monoidal.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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.

Equations

• ModuleCat.monoidalFree R = let __src := CategoryTheory.LaxMonoidalFunctor.of (ModuleCat.free R).obj; { toLaxMonoidalFunctor := __src, ε_isIso := ⋯, μ_isIso := ⋯ }

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.

Equations

• CategoryTheory.Free x C = 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.

Equations

• CategoryTheory.Free.of R X = X

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)

Equations

• CategoryTheory.categoryFree R C = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

Equations

• CategoryTheory.Free.instPreadditiveFreeCategoryFree R C = { homGroup := fun (X Y : CategoryTheory.Free R C) => Finsupp.instAddCommGroup, add_comp := ⋯, comp_add := ⋯ }

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)

Equations

• One or more equations did not get rendered due to their size.

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 (Finsupp.single f r) (Finsupp.single g s) = Finsupp.single (CategoryTheory.CategoryStruct.comp f g) (r * s)

@[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

@[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 = Finsupp.single f 1

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.

Equations

• CategoryTheory.Free.embedding R C = { toPrefunctor := { obj := fun (X : C) => X, map := fun {X Y : C} (f : X ⟶ Y) => Finsupp.single f 1 }, map_id := ⋯, map_comp := ⋯ }

@[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' : X ⟶ Y) (r : 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.

Equations

• One or more equations did not get rendered due to their size.

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 (Finsupp.single 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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• CategoryTheory.Free.ext R α = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Free R C) => α.app X) ⋯

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.

Equations

• CategoryTheory.Free.liftUnique R F L α = CategoryTheory.Free.ext R (α ≪≫ (CategoryTheory.Free.embeddingLiftIso R F).symm)