Documentation

Mathlib.CategoryTheory.Monoidal.Internal.Module

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.

noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.Ring_of_Mon_ {R : Type u} [CommRing R] (A : ModuleCat R) [Mon_Class A] :
Ring A
Equations
  • One or more equations did not get rendered due to their size.
noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.Algebra_of_Mon_ {R : Type u} [CommRing R] (A : ModuleCat R) [Mon_Class A] :
Algebra R A
Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    noncomputable def ModuleCat.MonModuleEquivalenceAlgebra.inverseObj {R : Type u} [CommRing R] (A : AlgCat R) :
    Mon_Class (of R A)

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

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

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

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

        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.
        Instances For

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

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