mathlibdocumentation

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 Module.free (R : Type u) [ring R] :
Type u

The free functor Type u ⥤ Module R sending a type X to the free R-module with generators x : X, implemented as the type X →₀ R.

Equations
@[simp]
theorem Module.free_obj (R : Type u) [ring R] (X : Type u) :
(Module.free R).obj X = (X →₀ R)
@[simp]
theorem Module.free_map (R : Type u) [ring R] (X Y : Type u) (f : X Y) :
(Module.free R).map f = f
noncomputable def Module.adj (R : Type u) [ring R] :

Equations
@[protected, instance]
Equations
noncomputable def Module.free.ε (R : Type u) [comm_ring R] :
𝟙_ (Module R) (Module.free R).obj (𝟙_ (Type u))

Equations
@[simp]
theorem Module.free.ε_apply (R : Type u) [comm_ring R] (r : R) :
r = finsupp.single punit.star r
noncomputable def Module.free.μ (R : Type u) [comm_ring R] (α β : Type u) :
(Module.free R).obj α (Module.free R).obj β (Module.free R).obj β)

Equations
theorem Module.free.μ_natural (R : Type u) [comm_ring R] {X Y X' Y' : Type u} (f : X Y) (g : X' Y') :
((Module.free R).map f (Module.free R).map g) Y Y').hom = X X').hom (Module.free R).map (f g)
theorem Module.free.left_unitality (R : Type u) [comm_ring R] (X : Type u) :
(λ_ ((Module.free R).obj X)).hom = 𝟙 ((Module.free R).obj X)) (𝟙_ (Type u)) X).hom (λ_ X).hom
theorem Module.free.right_unitality (R : Type u) [comm_ring R] (X : Type u) :
(ρ_ ((Module.free R).obj X)).hom = (𝟙 ((Module.free R).obj X) X (𝟙_ (Type u))).hom (ρ_ X).hom
theorem Module.free.associativity (R : Type u) [comm_ring R] (X Y Z : Type u) :
X Y).hom 𝟙 ((Module.free R).obj Z)) (X Y) Z).hom (α_ X Y Z).hom = (α_ ((Module.free R).obj X) ((Module.free R).obj Y) ((Module.free R).obj Z)).hom (𝟙 ((Module.free R).obj X) Y Z).hom) X (Y Z)).hom
@[simp]
theorem Module.free.obj.category_theory.lax_monoidal_μ (R : Type u) [comm_ring R] (X Y : Type u) :
= X Y).hom
@[protected, instance]
noncomputable def Module.free.obj.category_theory.lax_monoidal (R : Type u) [comm_ring R] :

The free R-module functor is lax monoidal.

Equations
@[protected, instance]
noncomputable def Module.monoidal_free (R : Type u) [comm_ring R] :

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

Equations
@[nolint]
def category_theory.Free (R : Type u_1) (C : Type u) :
Type u

Free R C is a type synonym for C, which, given [comm_ring 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
Instances for category_theory.Free
def category_theory.Free.of (R : Type u_1) {C : Type u} (X : 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
@[protected, instance]
noncomputable def category_theory.category_Free (R : Type u_1) [comm_ring R] (C : Type u)  :
Equations
@[protected, instance]
noncomputable def category_theory.Free.category_theory.preadditive (R : Type u_1) [comm_ring R] (C : Type u)  :
Equations
@[protected, instance]
noncomputable def category_theory.Free.category_theory.linear (R : Type u_1) [comm_ring R] (C : Type u)  :
Equations
theorem category_theory.Free.single_comp_single (R : Type u_1) [comm_ring R] (C : Type u) {X Y Z : C} (f : X Y) (g : Y Z) (r s : R) :
= finsupp.single (f g) (r * s)
noncomputable def category_theory.Free.embedding (R : Type u_1) [comm_ring R] (C : Type u)  :

A category embeds into its R-linear completion.

Equations
@[simp]
theorem category_theory.Free.embedding_obj (R : Type u_1) [comm_ring R] (C : Type u) (X : C) :
= X
@[simp]
theorem category_theory.Free.embedding_map (R : Type u_1) [comm_ring R] (C : Type u) (X Y : C) (f : X Y) :
=
@[simp]
theorem category_theory.Free.lift_map (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) (X Y : C) (f : X Y) :
.map f = (λ (f' : X Y) (r : R), r F.map f')
def category_theory.Free.lift (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) :

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

Equations
Instances for category_theory.Free.lift
@[simp]
theorem category_theory.Free.lift_obj (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) (X : C) :
.obj X = F.obj X
@[simp]
theorem category_theory.Free.lift_map_single (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) {X Y : C} (f : X Y) (r : R) :
.map r) = r F.map f
@[protected, instance]
def category_theory.Free.lift_additive (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) :
@[protected, instance]
def category_theory.Free.lift_linear (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) :
noncomputable def category_theory.Free.embedding_lift_iso (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) :

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

Equations
@[ext]
noncomputable def category_theory.Free.ext (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} {F G : D} [F.additive] [G.additive] (α : ) :
F G

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

Equations
noncomputable def category_theory.Free.lift_unique (R : Type u_1) [comm_ring R] {C : Type u} {D : Type u} (F : C D) (L : D) [L.additive] (α : F) :

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

Equations