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

• ModuleCat.free R = { obj := fun (X : Type ?u.23) => ModuleCat.of R (X →₀ R), map := fun {x x_1 : Type ?u.23} (f : x ⟶ x_1) => Finsupp.lmapDomain R R f, map_id := ⋯, map_comp := ⋯ }

noncomputable def ModuleCat.freeMk {R : Type u} [Ring R] {X : Type u} (x : X) : ↑((ModuleCat.free R).obj X)

Constructor for elements in the module (free R).obj X.

Equations

• ModuleCat.freeMk x = Finsupp.single x 1

theorem ModuleCat.free_hom_ext_iff {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} {f : (ModuleCat.free R).obj X ⟶ M} {g : (ModuleCat.free R).obj X ⟶ M} : f = g ↔ ∀ (x : X), f (ModuleCat.freeMk x) = g (ModuleCat.freeMk x)

theorem ModuleCat.free_hom_ext {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} {f : (ModuleCat.free R).obj X ⟶ M} {g : (ModuleCat.free R).obj X ⟶ M} (h : ∀ (x : X), f (ModuleCat.freeMk x) = g (ModuleCat.freeMk x)) : f = g

noncomputable def ModuleCat.freeDesc {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} (f : X ⟶ ↑M) : (ModuleCat.free R).obj X ⟶ M

The morphism of modules (free R).obj X ⟶ M corresponding to a map f : X ⟶ M.

Equations

• ModuleCat.freeDesc f = (Finsupp.lift (↑M) R X) f

@[simp]

theorem ModuleCat.freeDesc_apply {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} (f : X ⟶ ↑M) (x : X) : (ModuleCat.freeDesc f) (ModuleCat.freeMk x) = f x

@[simp]

theorem ModuleCat.free_map_apply {R : Type u} [Ring R] {X : Type u} {Y : Type u} (f : X → Y) (x : X) : ((ModuleCat.free R).map f) (ModuleCat.freeMk x) = ModuleCat.freeMk (f x)

@[simp]

theorem ModuleCat.freeHomEquiv_symm_apply {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} (ψ : X → ↑M) : ModuleCat.freeHomEquiv.symm ψ = ModuleCat.freeDesc ψ

@[simp]

theorem ModuleCat.freeHomEquiv_apply {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} (φ : (ModuleCat.free R).obj X ⟶ M) (x : X) : ModuleCat.freeHomEquiv φ x = φ (ModuleCat.freeMk x)

def ModuleCat.freeHomEquiv {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} : ((ModuleCat.free R).obj X ⟶ M) ≃ (X → ↑M)

The bijection ((free R).obj X ⟶ M) ≃ (X → M) when X is a type and M a module.

Equations

• ModuleCat.freeHomEquiv = { toFun := fun (φ : (ModuleCat.free R).obj X ⟶ M) (x : X) => φ (ModuleCat.freeMk x), invFun := fun (ψ : X → ↑M) => ModuleCat.freeDesc ψ, left_inv := ⋯, right_inv := ⋯ }

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.

@[simp]

theorem ModuleCat.adj_homEquiv (R : Type u) [Ring R] (X : Type u) (M : ModuleCat R) : (ModuleCat.adj R).homEquiv X M = ModuleCat.freeHomEquiv

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

Equations

• ⋯ = ⋯

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 α β = (finsuppTensorFinsupp' R α β).toModuleIso

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.instLaxMonoidalObjFree_μ (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.instLaxMonoidalObjFree_ε (R : Type u) [CommRing R] : CategoryTheory.LaxMonoidal.ε = ModuleCat.Free.ε R

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

The free R-module functor is lax monoidal.

Equations

• ModuleCat.Free.instLaxMonoidalObjFree R = CategoryTheory.LaxMonoidal.ofTensorHom (ModuleCat.free R).obj (ModuleCat.Free.ε R) (fun (X Y : Type ?u.34) => (ModuleCat.Free.μ R X Y).hom) ⋯ ⋯ ⋯ ⋯

instance ModuleCat.Free.instIsIsoε (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 = { toLaxMonoidalFunctor := CategoryTheory.LaxMonoidalFunctor.of (ModuleCat.free R).obj, ε_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 u_1 v, u} (CategoryTheory.Free R C)

Equations

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

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

Equations

• CategoryTheory.Free.instPreadditive R C = { homGroup := fun (x x_1 : CategoryTheory.Free R C) => Finsupp.instAddCommGroup, add_comp := ⋯, comp_add := ⋯ }

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

Equations

• CategoryTheory.Free.instLinear R C = { homModule := fun (x x_1 : CategoryTheory.Free R C) => Finsupp.module (x ⟶ x_1) R, smul_comp := ⋯, comp_smul := ⋯ }

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 x_1 : C} (f : x ⟶ x_1), (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 = { obj := fun (X : C) => X, map := fun {x x_1 : C} (f : x ⟶ x_1) => 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 x_1 : CategoryTheory.Free R C} (f : x ⟶ x_1), (CategoryTheory.Free.lift R F).map f = Finsupp.sum f fun (f' : x ⟶ x_1) (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.Free.lift R F).Additive

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.Free.embedding R C).comp (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} [F.Additive] [CategoryTheory.Functor.Linear R F] [G.Additive] [CategoryTheory.Functor.Linear R G] (α : (CategoryTheory.Free.embedding R C).comp F ≅ (CategoryTheory.Free.embedding R C).comp 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) [L.Additive] [CategoryTheory.Functor.Linear R L] (α : (CategoryTheory.Free.embedding R C).comp 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)