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.

noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.Ring_of_Mon_ {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) : Ring ↑A.X

Equations

• ModuleCat.MonModuleEquivalenceAlgebra.Ring_of_Mon_ A = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• ModuleCat.MonModuleEquivalenceAlgebra.Algebra_of_Mon_ A = Algebra.mk { toFun := A.one.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.algebraMap {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) (r : R) : (algebraMap R ↑A.X) r = A.one r

noncomputable 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.

Equations

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

@[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] : ∀ {x x_1 : Mon_ (ModuleCat R)} (f : x ⟶ x_1) (a : ↑x.X), (ModuleCat.MonModuleEquivalenceAlgebra.functor.map f) a = f.hom a

noncomputable def ModuleCat.MonModuleEquivalenceAlgebra.inverseObj {R : Type u} [CommRing R] (A : AlgebraCat R) : Mon_ (ModuleCat R)

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

Equations

• ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A = { X := ModuleCat.of R ↑A, one := Algebra.linearMap R ↑A, mul := LinearMap.mul' R ↑A, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one {R : Type u} [CommRing R] (A : AlgebraCat R) : (ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).one = Algebra.linearMap R ↑A

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul {R : Type u} [CommRing R] (A : AlgebraCat R) : (ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).mul = LinearMap.mul' R ↑A

@[simp]

theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_X {R : Type u} [CommRing R] (A : AlgebraCat R) : (ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).X = ModuleCat.of R ↑A

noncomputable 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.

Equations

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

@[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

noncomputable 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.

Equations

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

noncomputable def ModuleCat.monModuleEquivalenceAlgebraForget {R : Type u} [CommRing R] : ModuleCat.MonModuleEquivalenceAlgebra.functor.comp (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.

Equations

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