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.

source
noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.Ring_of_Mon_ {R : Type u} [CommRing R] (A : ModuleCat R) [Mon_Class A] :
Ring ↑A
Equations
    source
    noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.Algebra_of_Mon_ {R : Type u} [CommRing R] (A : ModuleCat R) [Mon_Class A] :
    Algebra R ↑A
    Equations
      source
      @[simp]
      theorem ModuleCat.MonModuleEquivalenceAlgebra.algebraMap {R : Type u} [CommRing R] (A : ModuleCat R) [Mon_Class A] (r : R) :
      (_root_.algebraMap R ↑A) r = (CategoryTheory.ConcreteCategory.hom Mon_Class.one) r
      source
      noncomputable def ModuleCat.MonModuleEquivalenceAlgebra.functor {R : Type u} [CommRing R] :
      CategoryTheory.Functor (Mon_ (ModuleCat R)) (AlgCat R)

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

      Equations
        Instances For
          source
          @[simp]
          theorem ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply {R : Type u} [CommRing R] {x✝ x✝¹ : Mon_ (ModuleCat R)} (f : x✝ ⟶ x✝¹) (a : ↑x✝.X) :
          (AlgCat.Hom.hom (functor.map f)) a = (CategoryTheory.ConcreteCategory.hom f.hom) a
          source
          @[simp]
          theorem ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) :
          ↑(functor.obj A) = ↑A.X
          source
          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
            Instances For
              source
              @[simp]
              theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one {R : Type u} [CommRing R] (A : AlgCat R) :
              Mon_Class.one = ofHom (Algebra.linearMap R ↑A)
              source
              @[simp]
              theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul {R : Type u} [CommRing R] (A : AlgCat R) :
              Mon_Class.mul = ofHom (LinearMap.mul' R ↑A)
              source
              noncomputable def ModuleCat.MonModuleEquivalenceAlgebra.inverse {R : Type u} [CommRing R] :
              CategoryTheory.Functor (AlgCat R) (Mon_ (ModuleCat R))

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

              Equations
                Instances For
                  source
                  @[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
                  source
                  @[simp]
                  theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon {R : Type u} [CommRing R] (A : AlgCat R) :
                  (inverse.obj A).mon = inverseObj A
                  source
                  @[simp]
                  theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup {R : Type u} [CommRing R] (A : AlgCat R) :
                  (inverse.obj A).X.isAddCommGroup = A.isRing.toAddCommGroup
                  source
                  @[simp]
                  theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier {R : Type u} [CommRing R] (A : AlgCat R) :
                  ↑(inverse.obj A).X = ↑A
                  source
                  @[simp]
                  theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule {R : Type u} [CommRing R] (A : AlgCat R) :
                  (inverse.obj A).X.isModule = Algebra.toModule
                  source
                  noncomputable def ModuleCat.monModuleEquivalenceAlgebra {R : Type u} [CommRing R] :
                  Mon_ (ModuleCat R) ≌ AlgCat R

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

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

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

                      Equations
                        Instances For