mathlib3 documentation

algebra.category.Module.adjunctions

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
noncomputable def Module.free (R : Type u) [ring R] :
Type u ⥤ Module R

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
source
@[simp]
theorem Module.free_obj (R : Type u) [ring R] (X : Type u) :
(Module.free R).obj X = Module.of R (X →₀ R)
source
@[simp]
theorem Module.free_map (R : Type u) [ring R] (X Y : Type u) (f : X ⟶ Y) :
(Module.free R).map f = finsupp.lmap_domain R R f
source
noncomputable def Module.adj (R : Type u) [ring R] :
Module.free R ⊣ category_theory.forget (Module R)

The free-forgetful adjunction for R-modules.

Equations
source
@[protected, instance]
noncomputable def Module.category_theory.forget.category_theory.is_right_adjoint (R : Type u) [ring R] :
category_theory.is_right_adjoint (category_theory.forget (Module R))
Equations
source
noncomputable def Module.free.ε (R : Type u) [comm_ring R] :
𝟙_ (Module R) ⟶ (Module.free R).obj (𝟙_ (Type u))

(Implementation detail) The unitor for free R.

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

(Implementation detail) The tensorator for free R.

Equations
source
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) ≫ (Module.free.μ R Y Y').hom = (Module.free.μ R X X').hom ≫ (Module.free R).map (f ⊗ g)
source
theorem Module.free.left_unitality (R : Type u) [comm_ring R] (X : Type u) :
(λ_ ((Module.free R).obj X)).hom = (Module.free.ε R ⊗ 𝟙 ((Module.free R).obj X)) ≫ (Module.free.μ R (𝟙_ (Type u)) X).hom ≫ category_theory.map (Module.free R).obj (λ_ X).hom
source
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) ⊗ Module.free.ε R) ≫ (Module.free.μ R X (𝟙_ (Type u))).hom ≫ category_theory.map (Module.free R).obj (ρ_ X).hom
source
theorem Module.free.associativity (R : Type u) [comm_ring R] (X Y Z : Type u) :
((Module.free.μ R X Y).hom ⊗ 𝟙 ((Module.free R).obj Z)) ≫ (Module.free.μ R (X ⊗ Y) Z).hom ≫ category_theory.map (Module.free R).obj (α_ 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) ⊗ (Module.free.μ R Y Z).hom) ≫ (Module.free.μ R X (Y ⊗ Z)).hom
source
@[simp]
theorem Module.free.obj.category_theory.lax_monoidal_ε (R : Type u) [comm_ring R] :
category_theory.lax_monoidal.ε (Module.free R).obj = Module.free.ε R
source
@[simp]
theorem Module.free.obj.category_theory.lax_monoidal_μ (R : Type u) [comm_ring R] (X Y : Type u) :
category_theory.lax_monoidal.μ (Module.free R).obj X Y = (Module.free.μ R X Y).hom
source
@[protected, instance]
noncomputable def Module.free.obj.category_theory.lax_monoidal (R : Type u) [comm_ring R] :
category_theory.lax_monoidal (Module.free R).obj

The free R-module functor is lax monoidal.

Equations
source
@[protected, instance]
def Module.free.category_theory.lax_monoidal.ε.category_theory.is_iso (R : Type u) [comm_ring R] :
category_theory.is_iso (category_theory.lax_monoidal.ε (Module.free R).obj)
source
noncomputable def Module.monoidal_free (R : Type u) [comm_ring R] :
category_theory.monoidal_functor (Type u) (Module R)

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

Equations
source
@[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
source
def category_theory.Free.of (R : Type u_1) {C : Type u} (X : C) :
category_theory.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
source
@[protected, instance]
noncomputable def category_theory.category_Free (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] :
category_theory.category (category_theory.Free R C)
Equations
source
@[protected, instance]
noncomputable def category_theory.Free.category_theory.preadditive (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] :
category_theory.preadditive (category_theory.Free R C)
Equations
source
@[protected, instance]
noncomputable def category_theory.Free.category_theory.linear (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] :
category_theory.linear R (category_theory.Free R C)
Equations
source
theorem category_theory.Free.single_comp_single (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) :
finsupp.single f r ≫ finsupp.single g s = finsupp.single (f ≫ g) (r * s)
source
noncomputable def category_theory.Free.embedding (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] :
C ⥤ category_theory.Free R C

A category embeds into its R-linear completion.

Equations
source
@[simp]
theorem category_theory.Free.embedding_obj (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] (X : C) :
(category_theory.Free.embedding R C).obj X = X
source
@[simp]
theorem category_theory.Free.embedding_map (R : Type u_1) [comm_ring R] (C : Type u) [category_theory.category C] (X Y : C) (f : X ⟶ Y) :
(category_theory.Free.embedding R C).map f = finsupp.single f 1
source
@[simp]
theorem category_theory.Free.lift_map (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C ⥤ D) (X Y : category_theory.Free R C) (f : X ⟶ Y) :
(category_theory.Free.lift R F).map f = finsupp.sum f (λ (f' : X ⟶ Y) (r : R), r • F.map f')
source
def category_theory.Free.lift (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C ⥤ D) :
category_theory.Free R 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
source
@[simp]
theorem category_theory.Free.lift_obj (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C ⥤ D) (X : category_theory.Free R C) :
(category_theory.Free.lift R F).obj X = F.obj X
source
@[simp]
theorem category_theory.Free.lift_map_single (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (r : R) :
(category_theory.Free.lift R F).map (finsupp.single f r) = r • F.map f
source
@[protected, instance]
def category_theory.Free.lift_additive (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C ⥤ D) :
(category_theory.Free.lift R F).additive
source
@[protected, instance]
def category_theory.Free.lift_linear (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C ⥤ D) :
category_theory.functor.linear R (category_theory.Free.lift R F)
source
noncomputable def category_theory.Free.embedding_lift_iso (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C ⥤ D) :
category_theory.Free.embedding R C ⋙ category_theory.Free.lift R F ≅ F

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

Equations
source
@[ext]
noncomputable def category_theory.Free.ext (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] {F G : category_theory.Free R C ⥤ D} [F.additive] [category_theory.functor.linear R F] [G.additive] [category_theory.functor.linear R G] (α : category_theory.Free.embedding R C ⋙ F ≅ category_theory.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
source
noncomputable def category_theory.Free.lift_unique (R : Type u_1) [comm_ring R] {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] [category_theory.preadditive D] [category_theory.linear R D] (F : C ⥤ D) (L : category_theory.Free R C ⥤ D) [L.additive] [category_theory.functor.linear R L] (α : category_theory.Free.embedding R C ⋙ L ≅ F) :
L ≅ category_theory.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