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
def
ModuleCat.MonModuleEquivalenceAlgebra.functor
{R : Type u}
[CommRing R]
:
CategoryTheory.Functor (Mon_ (ModuleCat R)) (AlgebraCat R)
Converting a monoid object in ModuleCat R
to a bundled algebra.
Instances For
@[simp]
theorem
ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one
{R : Type u}
[CommRing R]
(A : AlgebraCat R)
:
@[simp]
theorem
ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul
{R : Type u}
[CommRing R]
(A : AlgebraCat R)
:
@[simp]
theorem
ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_X
{R : Type u}
[CommRing R]
(A : AlgebraCat R)
:
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
def
ModuleCat.MonModuleEquivalenceAlgebra.inverse
{R : Type u}
[CommRing R]
:
CategoryTheory.Functor (AlgebraCat R) (Mon_ (ModuleCat R))
Converting a bundled algebra to a monoid object in ModuleCat R
.
Instances For
def
ModuleCat.monModuleEquivalenceAlgebra
{R : Type u}
[CommRing R]
:
Mon_ (ModuleCat R) ≌ AlgebraCat R
The category of internal monoid objects in ModuleCat R
is equivalent to the category of "native" bundled R
-algebras.
Instances For
def
ModuleCat.monModuleEquivalenceAlgebraForget
{R : Type u}
[CommRing R]
:
CategoryTheory.Functor.comp ModuleCat.MonModuleEquivalenceAlgebra.functor
(CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)) ≅ Mon_.forget (ModuleCat R)
The equivalence Mon_ (ModuleCat R) ≌ AlgebraCat R
is naturally compatible with the forgetful functors to ModuleCat R
.