Documentation

Mathlib.CategoryTheory.Monoidal.Internal.Module

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.

source
noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.Ring_of_Mon_ {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) :
Ring ↑A.X
Equations
source
noncomputable instance ModuleCat.MonModuleEquivalenceAlgebra.Algebra_of_Mon_ {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) :
Algebra R ↑A.X
Equations
source
@[simp]
theorem ModuleCat.MonModuleEquivalenceAlgebra.algebraMap {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) (r : R) :
(algebraMap R ↑A.X) r = A.one.hom r
source
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.
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) :
    (ModuleCat.MonModuleEquivalenceAlgebra.functor.map f).hom a = f.hom.hom a
    source
    @[simp]
    theorem ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier {R : Type u} [CommRing R] (A : Mon_ (ModuleCat R)) :
    ↑(ModuleCat.MonModuleEquivalenceAlgebra.functor.obj A) = ↑A.X
    source
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_X_isAddCommGroup {R : Type u} [CommRing R] (A : AlgebraCat R) :
      (ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).X.isAddCommGroup = Ring.toAddCommGroup
      source
      @[simp]
      theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one_hom {R : Type u} [CommRing R] (A : AlgebraCat R) :
      (ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).one.hom = Algebra.linearMap R ↑A
      source
      @[simp]
      theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_X_isModule {R : Type u} [CommRing R] (A : AlgebraCat R) :
      (ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).X.isModule = Algebra.toModule
      source
      @[simp]
      theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul_hom {R : Type u} [CommRing R] (A : AlgebraCat R) :
      (ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).mul.hom = LinearMap.mul' R ↑A
      source
      @[simp]
      theorem ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_X_carrier {R : Type u} [CommRing R] (A : AlgebraCat R) :
      ↑(ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).X = ↑A
      source
      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.
      Instances For
        source
        @[simp]
        theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom_hom {R : Type u} [CommRing R] {X✝ Y✝ : AlgebraCat R} (f : X✝ ⟶ Y✝) :
        (ModuleCat.MonModuleEquivalenceAlgebra.inverse.map f).hom.hom = f.hom.toLinearMap
        source
        @[simp]
        theorem ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj {R : Type u} [CommRing R] (A : AlgebraCat R) :
        ModuleCat.MonModuleEquivalenceAlgebra.inverse.obj A = ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A
        source
        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.
        Instances For
          source
          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.
          Instances For