Documentation

Mathlib.CategoryTheory.Monoidal.Internal.Module

Mon_ (ModuleCat R) ≌ AlgebraCat R #

The category of internal monoid objects in ModuleCat R is equivalent to the category of "native" bundled R-algebras.

Moreover, this equivalence is compatible with the forgetful functors to ModuleCat R.

@[simp]
theorem ModuleCat.MonModuleEquivalenceAlgebra.algebraMap {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) (r : R) :
↑(algebraMap R A.X) r = A.one r
@[simp]
theorem ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) :
↑(ModuleCat.MonModuleEquivalenceAlgebra.functor.obj A) = A.X
@[simp]
theorem ModuleCat.MonModuleEquivalenceAlgebra.functor_map_apply {R : Type u} [CommRing R] {A : Mon_ (ModuleCat R)} {B : Mon_ (ModuleCat R)} (f : A B) (a : A.X) :
↑(ModuleCat.MonModuleEquivalenceAlgebra.functor.map f) a = f.hom a

Converting a monoid object in ModuleCat R to a bundled algebra.

Instances For

    Converting a bundled algebra to a monoid object in ModuleCat R.

    Instances For
      @[simp]
      theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj {R : Type u} [CommRing R] (A : AlgebraCat R) :
      ModuleCat.MonModuleEquivalenceAlgebra.inverse.obj A = ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A
      @[simp]
      theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom {R : Type u} [CommRing R] :
      ∀ {X Y : AlgebraCat R} (f : X Y), (ModuleCat.MonModuleEquivalenceAlgebra.inverse.map f).hom = AlgHom.toLinearMap f

      Converting a bundled algebra to a monoid object in ModuleCat R.

      Instances For

        The category of internal monoid objects in ModuleCat R is equivalent to the category of "native" bundled R-algebras.

        Instances For

          The equivalence Mon_ (ModuleCat R) ≌ AlgebraCat R is naturally compatible with the forgetful functors to ModuleCat R.

          Instances For