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

noncomputable def ModuleCat.monoidAlgebraFree (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 monoid algebra R[X].

Equations

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

@[simp]

theorem ModuleCat.monoidAlgebraFree_map (R : Type u) [Ring R] {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : (monoidAlgebraFree R).map f = ofHom (MonoidAlgebra.mapDomainLinearMap R R ⇑(CategoryTheory.ConcreteCategory.hom f))

@[simp]

theorem ModuleCat.monoidAlgebraFree_obj_carrier (R : Type u) [Ring R] (X : Type u) : ↑((monoidAlgebraFree R).obj X) = MonoidAlgebra R X

noncomputable def ModuleCat.freeMk {R : Type u} [Ring R] {X : Type u} (x : X) : ↑((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 : (free R).obj X ⟶ M} (h : ∀ (x : X), (CategoryTheory.ConcreteCategory.hom f) (freeMk x) = (CategoryTheory.ConcreteCategory.hom g) (freeMk x)) : f = g

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

noncomputable def ModuleCat.freeDesc {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} (f : X ⟶ ↑M) : (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 = ModuleCat.ofHom ((Finsupp.lift (↑M) R X) ⇑(CategoryTheory.ConcreteCategory.hom f))

@[simp]

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

@[simp]

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

noncomputable def ModuleCat.freeHomEquiv {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} : ((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

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

@[simp]

theorem ModuleCat.freeHomEquiv_apply {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} (φ : (free R).obj X ⟶ M) : freeHomEquiv φ = TypeCat.ofHom fun (x : X) => (CategoryTheory.ConcreteCategory.hom φ) (freeMk x)

@[simp]

theorem ModuleCat.freeHomEquiv_symm_apply {R : Type u} [Ring R] {X : Type u} {M : ModuleCat R} (ψ : X ⟶ ↑M) : freeHomEquiv.symm ψ = freeDesc (TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom ψ))

noncomputable def ModuleCat.adj (R : Type u) [Ring R] : 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) : (adj R).homEquiv X M = freeHomEquiv

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

noncomputable def ModuleCat.FreeMonoidal.εIso (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R) ≅ (free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (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 := ModuleCat.ofHom (Finsupp.lsingle PUnit.unit), inv := ModuleCat.ofHom (Finsupp.lapply PUnit.unit), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

noncomputable def ModuleCat.FreeMonoidal.μIso (R : Type u) [CommRing R] (X Y : Type u) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((free R).obj X) ((free R).obj Y) ≅ (free R).obj (CategoryTheory.MonoidalCategoryStruct.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 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) : (CategoryTheory.ConcreteCategory.hom (μIso R X Y).hom) (freeMk x ⊗ₜ[R] freeMk y) = freeMk (x, y)

@[simp]

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

@[implicit_reducible]

noncomputable instance ModuleCat.instMonoidalFree (R : Type u) [CommRing R] : (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.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.ε (free R))) 1 = freeMk PUnit.unit

@[simp]

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

@[simp]

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

@[simp]

theorem ModuleCat.free_δ_freeMk (R : Type u) [CommRing R] {X Y : Type u} (z : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.OplaxMonoidal.δ (free R) X Y)) (freeMk z) = freeMk z.1 ⊗ₜ[R] 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) : 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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Free.instLinear (R : Type u_1) [CommRing R] (C : Type u) [Category.{v, u} C] : Linear R (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) [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) : CategoryStruct.comp (Finsupp.single f r) (Finsupp.single g s) = Finsupp.single (CategoryStruct.comp f g) (r * s)

noncomputable def CategoryTheory.Free.embedding (R : Type u_1) [CommRing R] (C : Type u) [Category.{v, u} C] : Functor C (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) [Category.{v, u} C] (X : C) : (embedding R C).obj X = X

@[simp]

theorem CategoryTheory.Free.embedding_map (R : Type u_1) [CommRing R] (C : Type u) [Category.{v, u} C] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) : (embedding R C).map f = Finsupp.single f 1

def CategoryTheory.Free.lift (R : Type u_1) [CommRing R] {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] [Preadditive D] [Linear R D] (F : Functor C D) : Functor (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_map (R : Type u_1) [CommRing R] {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] [Preadditive D] [Linear R D] (F : Functor C D) {x✝ x✝¹ : Free R C} (f : x✝ ⟶ x✝¹) : (lift R F).map f = Finsupp.sum f fun (f' : x✝ ⟶ x✝¹) (r : R) => r • F.map f'

@[simp]

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

theorem CategoryTheory.Free.lift_map_single (R : Type u_1) [CommRing R] {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] [Preadditive D] [Linear R D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) (r : R) : (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} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] [Preadditive D] [Linear R D] (F : Functor C D) : (lift R F).Additive

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

noncomputable def CategoryTheory.Free.embeddingLiftIso (R : Type u_1) [CommRing R] {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] [Preadditive D] [Linear R D] (F : Functor C D) : (embedding R C).comp (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.

noncomputable def CategoryTheory.Free.ext (R : Type u_1) [CommRing R] {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] [Preadditive D] [Linear R D] {F G : Functor (Free R C) D} [F.Additive] [Functor.Linear R F] [G.Additive] [Functor.Linear R G] (α : (embedding R C).comp F ≅ (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) ⋯

noncomputable def CategoryTheory.Free.liftUnique (R : Type u_1) [CommRing R] {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] [Preadditive D] [Linear R D] (F : Functor C D) (L : Functor (Free R C) D) [L.Additive] [Functor.Linear R L] (α : (embedding R C).comp L ≅ F) : L ≅ 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)