Mon (ModuleCat R) ≌ AlgCat 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.

@[implicit_reducible]

noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toRing {R : Type u} [CommRing R] (A : ModuleCat R) [CategoryTheory.MonObj A] : Ring ↑A

@[implicit_reducible]

noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.Algebra_of_Mon_ {R : Type u} [CommRing R] (A : ModuleCat R) [CategoryTheory.MonObj A] : Algebra R ↑A

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.algebraMap {R : Type u} [CommRing R] (A : ModuleCat R) [CategoryTheory.MonObj A] (r : R) : (_root_.algebraMap R ↑A) r = (CategoryTheory.ConcreteCategory.hom CategoryTheory.MonObj.one) r

noncomputable def ModuleCat.MonModuleEquivalenceAlgebra.functor {R : Type u} [CommRing R] : CategoryTheory.Functor (CategoryTheory.Mon (ModuleCat R)) (AlgCat R)

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

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply {R : Type u} [CommRing R] {x✝ x✝¹ : CategoryTheory.Mon (ModuleCat R)} (f : x✝ ⟶ x✝¹) (a : ↑x✝.X) : (AlgCat.Hom.hom (functor.map f)) a = (CategoryTheory.ConcreteCategory.hom f.hom) a

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier {R : Type u} [CommRing R] (A : CategoryTheory.Mon (ModuleCat R)) : ↑(functor.obj A) = ↑A.X

@[implicit_reducible]

noncomputable def ModuleCat.MonModuleEquivalenceAlgebra.inverseObj {R : Type u} [CommRing R] (A : AlgCat R) : CategoryTheory.MonObj (of R ↑A)

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

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one {R : Type u} [CommRing R] (A : AlgCat R) : CategoryTheory.MonObj.one = ofHom (Algebra.linearMap R ↑A)

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul {R : Type u} [CommRing R] (A : AlgCat R) : CategoryTheory.MonObj.mul = ofHom (LinearMap.mul' R ↑A)

noncomputable def ModuleCat.MonModuleEquivalenceAlgebra.inverse {R : Type u} [CommRing R] : CategoryTheory.Functor (AlgCat R) (CategoryTheory.Mon (ModuleCat R))

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

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier {R : Type u} [CommRing R] (A : AlgCat R) : ↑(inverse.obj A).X = ↑A

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom {R : Type u} [CommRing R] {X✝ Y✝ : AlgCat R} (f : X✝ ⟶ Y✝) : (inverse.map f).hom = ofHom (AlgCat.Hom.hom f).toLinearMap

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup {R : Type u} [CommRing R] (A : AlgCat R) : (inverse.obj A).X.isAddCommGroup = A.isRing.toAddCommGroup

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule {R : Type u} [CommRing R] (A : AlgCat R) : (inverse.obj A).X.isModule = Algebra.toModule

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon {R : Type u} [CommRing R] (A : AlgCat R) : (inverse.obj A).mon = inverseObj A

noncomputable def ModuleCat.monModuleEquivalenceAlgebra {R : Type u} [CommRing R] : CategoryTheory.Mon (ModuleCat R) ≌ AlgCat R

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

noncomputable def ModuleCat.monModuleEquivalenceAlgebraForget {R : Type u} [CommRing R] : MonModuleEquivalenceAlgebra.functor.comp (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)) ≅ CategoryTheory.Mon.forget (ModuleCat R)

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