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 {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} {f 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 Y : Type u} (f : X → Y) (x : X) : ((ModuleCat.free R).map f) (ModuleCat.freeMk x) = ModuleCat.freeMk (f 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 := ⋯ }

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

@[simp]

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

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.FreeMonoidal.εIso (R : Type u) [CommRing R] : 𝟙_ (ModuleCat R) ≅ (ModuleCat.free R).obj (𝟙_ (Type u))

The canonical isomorphism 𝟙_ (ModuleCat R) ≅ (free R).obj (𝟙_ (Type u)). (This should not be used directly: it is part of the implementation of the monoidal structure on the functor free R.)

Equations

• ModuleCat.FreeMonoidal.εIso R = { hom := Finsupp.lsingle PUnit.unit, inv := Finsupp.lapply PUnit.unit, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem ModuleCat.FreeMonoidal.εIso_hom_one (R : Type u) [CommRing R] : (ModuleCat.FreeMonoidal.εIso R).hom 1 = ModuleCat.freeMk PUnit.unit

@[simp]

theorem ModuleCat.FreeMonoidal.εIso_inv_freeMk (R : Type u) [CommRing R] (x : PUnit.{u + 1} ) : (ModuleCat.FreeMonoidal.εIso R).inv (ModuleCat.freeMk x) = 1

def ModuleCat.FreeMonoidal.μIso (R : Type u) [CommRing R] (X Y : Type u) : CategoryTheory.MonoidalCategory.tensorObj ((ModuleCat.free R).obj X) ((ModuleCat.free R).obj Y) ≅ (ModuleCat.free R).obj (CategoryTheory.MonoidalCategory.tensorObj X Y)

The canonical isomorphism (free R).obj X ⊗ (free R).obj Y ≅ (free R).obj (X ⊗ Y) for two types X and Y. (This should not be used directly: it is is part of the implementation of the monoidal structure on the functor free R.)

Equations

• ModuleCat.FreeMonoidal.μIso R X Y = (finsuppTensorFinsupp' R X Y).toModuleIso

@[simp]

theorem ModuleCat.FreeMonoidal.μIso_hom_freeMk_tmul_freeMk (R : Type u) [CommRing R] {X Y : Type u} (x : X) (y : Y) : (ModuleCat.FreeMonoidal.μIso R X Y).hom (ModuleCat.freeMk x ⊗ₜ[R] ModuleCat.freeMk y) = ModuleCat.freeMk (x, y)

@[simp]

theorem ModuleCat.FreeMonoidal.μIso_inv_freeMk (R : Type u) [CommRing R] {X Y : Type u} (z : CategoryTheory.MonoidalCategory.tensorObj X Y) : (ModuleCat.FreeMonoidal.μIso R X Y).inv (ModuleCat.freeMk z) = ModuleCat.freeMk z.1 ⊗ₜ[R] ModuleCat.freeMk z.2

instance ModuleCat.instMonoidalFree (R : Type u) [CommRing R] : (ModuleCat.free R).Monoidal

The free functor Type u ⥤ ModuleCat R is a monoidal functor.

Equations

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

@[simp]

theorem ModuleCat.free_ε_one (R : Type u) [CommRing R] : (CategoryTheory.Functor.LaxMonoidal.ε (ModuleCat.free R)) 1 = ModuleCat.freeMk PUnit.unit

@[simp]

theorem ModuleCat.free_η_freeMk (R : Type u) [CommRing R] (x : PUnit.{u + 1} ) : (CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.free R)) (ModuleCat.freeMk x) = 1

@[simp]

theorem ModuleCat.free_μ_freeMk_tmul_freeMk (R : Type u) [CommRing R] {X Y : Type u} (x : X) (y : Y) : (CategoryTheory.Functor.LaxMonoidal.μ (ModuleCat.free R) X Y) (ModuleCat.freeMk x ⊗ₜ[R] ModuleCat.freeMk y) = ModuleCat.freeMk (x, y)

@[simp]

theorem ModuleCat.free_δ_freeMk (R : Type u) [CommRing R] {X Y : Type u} (z : CategoryTheory.MonoidalCategory.tensorObj X Y) : (CategoryTheory.Functor.OplaxMonoidal.δ (ModuleCat.free R) X Y) (ModuleCat.freeMk z) = ModuleCat.freeMk z.1 ⊗ₜ[R] ModuleCat.freeMk z.2

def CategoryTheory.Free : Type u_1 → (C : 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 Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) : CategoryTheory.CategoryStruct.comp (Finsupp.single f r) (Finsupp.single g s) = Finsupp.single (CategoryTheory.CategoryStruct.comp f g) (r * s)

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.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✝¹ : C} (f : x✝ ⟶ x✝¹) : (CategoryTheory.Free.embedding R C).map f = Finsupp.single f 1

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.

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

@[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✝¹ : CategoryTheory.Free R C} (f : x✝ ⟶ x✝¹) : (CategoryTheory.Free.lift R F).map f = Finsupp.sum f fun (f' : x✝ ⟶ x✝¹) (r : R) => r • F.map f'

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