The category of monoids in a monoidal category, and modules over an internal monoid.
structure
Mon_
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
Type (max u v)
- X : C
- one : 𝟙_ C ⟶ c.X
- mul : c.X ⊗ c.X ⟶ c.X
- one_mul' : (c.one ⊗ 𝟙 c.X) ≫ c.mul = (λ_ c.X).hom . "obviously"
- mul_one' : (𝟙 c.X ⊗ c.one) ≫ c.mul = (ρ_ c.X).hom . "obviously"
- mul_assoc' : (c.mul ⊗ 𝟙 c.X) ≫ c.mul = (α_ c.X c.X c.X).hom ≫ (𝟙 c.X ⊗ c.mul) ≫ c.mul . "obviously"
A monoid object internal to a monoidal category.
When the monoidal category is preadditive, this is also sometimes called an "algebra object".
theorem
Mon_.hom.ext_iff
{C : Type u}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.monoidal_category C}
{M N : Mon_ C}
(x y : M.hom N) :
theorem
Mon_.hom.ext
{C : Type u}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.monoidal_category C}
{M N : Mon_ C}
(x y : M.hom N) :
@[simp]
theorem
Mon_.id_hom
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(M : Mon_ C) :
@[instance]
def
Mon_.hom_inhabited
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(M : Mon_ C) :
Equations
- M.hom_inhabited = {default := M.id}
@[simp]
theorem
Mon_.comp_hom
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{M N O : Mon_ C}
(f : M.hom N)
(g : N.hom O) :
@[instance]
def
Mon_.category_theory.category
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C] :
@[simp]
theorem
Mon_.id_hom'
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(M : Mon_ C) :
@[simp]
theorem
Mon_.comp_hom'
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{M N K : Mon_ C}
(f : M ⟶ N)
(g : N ⟶ K) :
The forgetful functor from monoid objects to the ambient category.
structure
Mod
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C] :
Mon_ C → Type (max u v)
- X : C
- act : A.X ⊗ c.X ⟶ c.X
- one_act' : (A.one ⊗ 𝟙 c.X) ≫ c.act = (λ_ c.X).hom . "obviously"
- assoc' : (A.mul ⊗ 𝟙 c.X) ≫ c.act = (α_ A.X A.X c.X).hom ≫ (𝟙 A.X ⊗ c.act) ≫ c.act . "obviously"
A module object for a monoid object, all internal to some monoidal category.
theorem
Mod.hom.ext_iff
{C : Type u}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.monoidal_category C}
{A : Mon_ C}
{M N : Mod A}
(x y : M.hom N) :
theorem
Mod.hom.ext
{C : Type u}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.monoidal_category C}
{A : Mon_ C}
{M N : Mod A}
(x y : M.hom N) :
@[simp]
theorem
Mod.id_hom
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C}
(M : Mod A) :
@[instance]
def
Mod.hom_inhabited
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C}
(M : Mod A) :
Equations
- M.hom_inhabited = {default := M.id}
@[simp]
theorem
Mod.comp_hom
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C}
{M N O : Mod A}
(f : M.hom N)
(g : N.hom O) :
@[instance]
def
Mod.category_theory.category
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C} :
@[simp]
theorem
Mod.id_hom'
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C}
(M : Mod A) :
@[simp]
theorem
Mod.comp_hom'
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A : Mon_ C}
{M N K : Mod A}
(f : M ⟶ N)
(g : N ⟶ K) :
@[simp]
theorem
Mod.regular_act
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
(Mod.regular A).act = A.mul
def
Mod.regular
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
Mod A
A monoid object as a module over itself.
@[simp]
theorem
Mod.regular_X
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
(Mod.regular A).X = A.X
@[instance]
def
Mod.inhabited
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
Equations
- Mod.inhabited A = {default := Mod.regular A}
def
Mod.comap
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C} :
A morphism of monoid objects induces a "restriction" or "comap" functor between the categories of module objects.
@[simp]
theorem
Mod.comap_map_hom
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
(f : A ⟶ B)
(M N : Mod B)
(g : M ⟶ N) :
@[simp]
theorem
Mod.comap_obj_X
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
(f : A ⟶ B)
(M : Mod B) :
Projects:
- Check that
Mon_ Mon ≌ CommMon, via the Eckmann-Hilton argument. (You'll have to hook up the cartesian monoidal structure onMonfirst, available in #3463) - Check that
Mon_ Top ≌ [bundled topological monoids]. - Check that
Mon_ AddCommGroup ≌ Ring. (You'll have to hook up the monoidal structure onAddCommGroup. Currently we have the monoidal structure onModule R; perhaps one could specialize toR = ℤand transport the monoidal structure across an equivalence? This sounds like some work!) - Check that
Mon_ (Module R) ≌ Algebra R. - Show that if
Cis braided (see #3550) thenMon_ Cis naturally monoidal. - Can you transport this monoidal structure to
RingorAlgebra R? How does it compare to the "native" one?