Documentation

Mathlib.Algebra.Category.ModuleCat.Adjunctions

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.

@[simp]
theorem ModuleCat.free_map (R : Type u) [Ring R] {X : Type u} {Y : Type u} (f : X Y) :
@[simp]
theorem ModuleCat.free_obj (R : Type u) [Ring R] (X : Type u) :

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.

Instances For

    The free-forgetful adjunction for R-modules.

    Instances For
      @[simp]
      theorem ModuleCat.Free.ε_apply (R : Type u) [CommRing R] (r : R) :
      ↑(ModuleCat.Free.ε R) r = fun₀ | PUnit.unit => r

      (Implementation detail) The tensorator for Free R.

      Instances For

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

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

          Instances For
            def CategoryTheory.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.

            Instances For
              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 (fun₀ | f => r) fun₀ | g => s) = fun₀ | CategoryTheory.CategoryStruct.comp f g => r * s
              @[simp]
              theorem CategoryTheory.Free.embedding_map (R : Type u_1) [CommRing R] (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :
              (CategoryTheory.Free.embedding R C).map f = fun₀ | f => 1

              A category embeds into its R-linear completion.

              Instances For

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

                Instances For
                  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 fun₀ | f => r) = r F.map f

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

                  Instances For