TensorAlgebra as a functor ModuleCat R ⥤ AlgCat R

In this file we define the functor AlgCat.tensorAlgebra : ModuleCat R ⥤ AlgCat R sending an R-module M to the tensor algebra TensorAlgebra R M. We show that this functor is a left-adjoint to the forgetful functor AlgCat R ⥤ ModuleCat R.

def AlgCat.tensorAlgebra (R : Type u) [CommRing R] : CategoryTheory.Functor (ModuleCat R) (AlgCat R)

The functor sending an R-module M to its tensor algebra over R.

Equations

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

@[simp]

theorem AlgCat.tensorAlgebra_map (R : Type u) [CommRing R] {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) : (tensorAlgebra R).map f = ofHom ((TensorAlgebra.lift R) (TensorAlgebra.ι R ∘ₗ ModuleCat.Hom.hom f))

@[simp]

theorem AlgCat.tensorAlgebra_obj_carrier (R : Type u) [CommRing R] (M : ModuleCat R) : ↑((tensorAlgebra R).obj M) = TensorAlgebra R ↑M

def AlgCat.tensorAlgebraAdj (R : Type u) [CommRing R] : tensorAlgebra R ⊣ CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)

Taking the tensor algebra forms a left adjoint of the forgetful functor from AlgCat R to ModuleCat R.

Equations

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

@[simp]

theorem AlgCat.tensorAlgebraAdj_counit_app (R : Type u) [CommRing R] (A : AlgCat R) : (tensorAlgebraAdj R).counit.app A = ofHom ((TensorAlgebra.lift R) LinearMap.id)

@[simp]

theorem AlgCat.tensorAlgebraAdj_unit_app (R : Type u) [CommRing R] (M : ModuleCat R) : (tensorAlgebraAdj R).unit.app M = ModuleCat.ofHom (TensorAlgebra.ι R)

instance AlgCat.instIsRightAdjointModuleCatForget₂AlgHomCarrierLinearMapIdCarrierOfSmall (R : Type v) [CommRing R] [Small.{u, v} R] : (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint

instance AlgCat.instIsRightAdjointAddCommGrpCatRingCatForget₂RingHomCarrierAddMonoidHomCarrier : (CategoryTheory.forget₂ RingCat AddCommGrpCat).IsRightAdjoint