mathlib documentation

category_theory.monoidal.Mon_

The category of monoids in a monoidal category.

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

@[simp]

theorem Mon_.trivial_X (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(Mon_.trivial C).X = 𝟙_ C

def Mon_.trivial (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

The trivial monoid object. We later show this is initial in Mon_ C.

Equations

Mon_.trivial C = {X := 𝟙_ C _inst_2, one := 𝟙 (𝟙_ C), mul := (λ_ (𝟙_ C)).hom, one_mul' := _, mul_one' := _, mul_assoc' := _}

@[simp]

theorem Mon_.trivial_mul (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(Mon_.trivial C).mul = (λ_ (𝟙_ C)).hom

@[simp]

theorem Mon_.trivial_one (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(Mon_.trivial C).one = 𝟙 (𝟙_ C)

@[instance]

def Mon_.inhabited (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

inhabited (Mon_ C)

Equations

Mon_.inhabited C = {default := Mon_.trivial C _inst_2}

@[simp]

theorem Mon_.one_mul_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M : Mon_ C} {Z : C} (f : Z ⟶ M.X) :

(M.one ⊗ f) ≫ M.mul = (λ_ Z).hom ≫ f

@[simp]

theorem Mon_.mul_one_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M : Mon_ C} {Z : C} (f : Z ⟶ M.X) :

(f ⊗ M.one) ≫ M.mul = (ρ_ Z).hom ≫ f

theorem Mon_.assoc_flip {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {M : Mon_ C} :

(𝟙 M.X ⊗ M.mul) ≫ M.mul = (α_ M.X M.X M.X).inv ≫ (M.mul ⊗ 𝟙 M.X) ≫ M.mul

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) :

x = y ↔ x.hom = y.hom

@[ext]

structure Mon_.hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M N : Mon_ C) :

Type v₁

hom : M.X ⟶ N.X
one_hom' : M.one ≫ c.hom = N.one . "obviously"
mul_hom' : M.mul ≫ c.hom = (c.hom ⊗ c.hom) ≫ N.mul . "obviously"

A morphism of monoid objects.

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) (h : x.hom = y.hom) :

x = y

def Mon_.id {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M : Mon_ C) :

M.hom M

The identity morphism on a monoid object.

Equations

M.id = {hom := 𝟙 M.X, one_hom' := _, mul_hom' := _}

@[simp]

theorem Mon_.id_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M : Mon_ C) :

M.id.hom = 𝟙 M.X

@[instance]

def Mon_.hom_inhabited {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M : Mon_ C) :

inhabited (M.hom M)

Equations

M.hom_inhabited = {default := M.id}

def Mon_.comp {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) :

M.hom O

Composition of morphisms of monoid objects.

Equations

Mon_.comp f g = {hom := f.hom ≫ g.hom, one_hom' := _, mul_hom' := _}

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

(Mon_.comp f g).hom = f.hom ≫ g.hom

@[instance]

def Mon_.category_theory.category {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.category (Mon_ C)

Equations

Mon_.category_theory.category = {to_category_struct := {to_has_hom := {hom := λ (M N : Mon_ C), M.hom N}, id := Mon_.id _inst_2, comp := λ (M N O : Mon_ C) (f : M ⟶ N) (g : N ⟶ O), Mon_.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem Mon_.id_hom' {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (M : Mon_ C) :

(𝟙 M).hom = 𝟙 M.X

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

(f ≫ g).hom = f.hom ≫ g.hom

@[simp]

theorem Mon_.forget_obj (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

(Mon_.forget C).obj A = A.X

@[simp]

theorem Mon_.forget_map (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (A B : Mon_ C) (f : A ⟶ B) :

(Mon_.forget C).map f = f.hom

def Mon_.forget (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

The forgetful functor from monoid objects to the ambient category.

Equations

Mon_.forget C = {obj := λ (A : Mon_ C), A.X, map := λ (A B : Mon_ C) (f : A ⟶ B), f.hom, map_id' := _, map_comp' := _}

@[instance]

def Mon_.forget_faithful {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.faithful (Mon_.forget C)

@[instance]

def Mon_.category_theory.is_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A ⟶ B) [e : category_theory.is_iso ((Mon_.forget C).map f)] :

category_theory.is_iso f.hom

Equations

Mon_.category_theory.is_iso f = e

@[instance]

def Mon_.category_theory.reflects_isomorphisms {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.reflects_isomorphisms (Mon_.forget C)

The forgetful functor from monoid objects to the ambient category reflects isomorphisms.

Equations

Mon_.category_theory.reflects_isomorphisms = {reflects := λ (X Y : Mon_ C) (f : X ⟶ Y) (e : category_theory.is_iso ((Mon_.forget C).map f)), {inv := {hom := category_theory.is_iso.inv f.hom (Mon_.category_theory.is_iso f), one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}}

@[instance]

def Mon_.unique_hom_from_trivial {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

unique (Mon_.trivial C ⟶ A)

Equations

A.unique_hom_from_trivial = {to_inhabited := {default := {hom := A.one, one_hom' := _, mul_hom' := _}}, uniq := _}

@[instance]

def Mon_.category_theory.limits.has_initial {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.limits.has_initial (Mon_ C)

def category_theory.lax_monoidal_functor.map_Mon {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.lax_monoidal_functor C D) :

Mon_ C ⥤ Mon_ D

A lax monoidal functor takes monoid objects to monoid objects.

That is, a lax monoidal functor F : C ⥤ D induces a functor Mon_ C ⥤ Mon_ D.

Equations

F.map_Mon = {obj := λ (A : Mon_ C), {X := F.to_functor.obj A.X, one := F.ε ≫ F.to_functor.map A.one, mul := F.μ A.X A.X ≫ F.to_functor.map A.mul, one_mul' := _, mul_one' := _, mul_assoc' := _}, map := λ (A B : Mon_ C) (f : A ⟶ B), {hom := F.to_functor.map f.hom, one_hom' := _, mul_hom' := _}, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.lax_monoidal_functor.map_Mon_obj_one {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.lax_monoidal_functor C D) (A : Mon_ C) :

(F.map_Mon.obj A).one = F.ε ≫ F.to_functor.map A.one

@[simp]

theorem category_theory.lax_monoidal_functor.map_Mon_map_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.lax_monoidal_functor C D) (A B : Mon_ C) (f : A ⟶ B) :

(F.map_Mon.map f).hom = F.to_functor.map f.hom

@[simp]

theorem category_theory.lax_monoidal_functor.map_Mon_obj_mul {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.lax_monoidal_functor C D) (A : Mon_ C) :

(F.map_Mon.obj A).mul = F.μ A.X A.X ≫ F.to_functor.map A.mul

@[simp]

theorem category_theory.lax_monoidal_functor.map_Mon_obj_X {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.lax_monoidal_functor C D) (A : Mon_ C) :

(F.map_Mon.obj A).X = F.to_functor.obj A.X

def category_theory.lax_monoidal_functor.map_Mon_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] :

category_theory.lax_monoidal_functor C D ⥤ Mon_ C ⥤ Mon_ D

map_Mon is functorial in the lax monoidal functor.

Equations

category_theory.lax_monoidal_functor.map_Mon_functor C D = {obj := category_theory.lax_monoidal_functor.map_Mon _inst_4, map := λ (F G : category_theory.lax_monoidal_functor C D) (α : F ⟶ G), {app := λ (A : Mon_ C), {hom := α.to_nat_trans.app A.X, one_hom' := _, mul_hom' := _}, naturality' := _}, map_id' := _, map_comp' := _}

def Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.lax_monoidal_functor (category_theory.discrete punit) C ⥤ Mon_ C

Implementation of Mon_.equiv_lax_monoidal_functor_punit.

Equations

Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C = {obj := λ (F : category_theory.lax_monoidal_functor (category_theory.discrete punit) C), F.map_Mon.obj (Mon_.trivial (category_theory.discrete punit)), map := λ (F G : category_theory.lax_monoidal_functor (category_theory.discrete punit) C) (α : F ⟶ G), ((category_theory.lax_monoidal_functor.map_Mon_functor (category_theory.discrete punit) C).map α).app (Mon_.trivial (category_theory.discrete punit)), map_id' := _, map_comp' := _}

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon_obj (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (F : category_theory.lax_monoidal_functor (category_theory.discrete punit) C) :

(Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C).obj F = F.map_Mon.obj (Mon_.trivial (category_theory.discrete punit))

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon_map (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (F G : category_theory.lax_monoidal_functor (category_theory.discrete punit) C) (α : F ⟶ G) :

(Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C).map α = ((category_theory.lax_monoidal_functor.map_Mon_functor (category_theory.discrete punit) C).map α).app (Mon_.trivial (category_theory.discrete punit))

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal_obj_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :

((Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C).obj A).ε = A.one

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal_obj_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) (_x _x_1 : category_theory.discrete punit) :

((Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C).obj A).μ _x _x_1 = A.mul

def Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

Mon_ C ⥤ category_theory.lax_monoidal_functor (category_theory.discrete punit) C

Implementation of Mon_.equiv_lax_monoidal_functor_punit.

Equations

Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C = {obj := λ (A : Mon_ C), {to_functor := {obj := λ (_x : category_theory.discrete punit), A.X, map := λ (_x _x_1 : category_theory.discrete punit) (_x : _x ⟶ _x_1), 𝟙 A.X, map_id' := _, map_comp' := _}, ε := A.one, μ := λ (_x _x : category_theory.discrete punit), A.mul, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, map := λ (A B : Mon_ C) (f : A ⟶ B), {to_nat_trans := {app := λ (_x : category_theory.discrete punit), f.hom, naturality' := _}, unit' := _, tensor' := _}, map_id' := _, map_comp' := _}

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal_map_to_nat_trans_app (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (A B : Mon_ C) (f : A ⟶ B) (_x : category_theory.discrete punit) :

((Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C).map f).to_nat_trans.app _x = f.hom

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal_obj_to_functor_map (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) (_x _x_1 : category_theory.discrete punit) (_x_2 : _x ⟶ _x_1) :

((Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C).obj A).to_functor.map _x_2 = 𝟙 A.X

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal_obj_to_functor_obj (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) (_x : category_theory.discrete punit) :

((Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C).obj A).to_functor.obj _x = A.X

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.unit_iso_hom_app_to_nat_trans_app (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.lax_monoidal_functor (category_theory.discrete punit) C) (X_1 : category_theory.discrete punit) :

((Mon_.equiv_lax_monoidal_functor_punit.unit_iso C).hom.app X).to_nat_trans.app X_1 = ((λ (_x : category_theory.discrete punit), X.to_functor.map_iso (category_theory.eq_to_iso _)) X_1).hom

def Mon_.equiv_lax_monoidal_functor_punit.unit_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

𝟭 (category_theory.lax_monoidal_functor (category_theory.discrete punit) C) ≅ Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C ⋙ Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C

Implementation of Mon_.equiv_lax_monoidal_functor_punit.

Equations

Mon_.equiv_lax_monoidal_functor_punit.unit_iso C = category_theory.nat_iso.of_components (λ (F : category_theory.lax_monoidal_functor (category_theory.discrete punit) C), category_theory.monoidal_nat_iso.of_components (λ (_x : category_theory.discrete punit), F.to_functor.map_iso (category_theory.eq_to_iso _)) _ _ _) _

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.unit_iso_inv_app_to_nat_trans_app (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.lax_monoidal_functor (category_theory.discrete punit) C) (X_1 : category_theory.discrete punit) :

((Mon_.equiv_lax_monoidal_functor_punit.unit_iso C).inv.app X).to_nat_trans.app X_1 = category_theory.is_iso.inv ({to_nat_trans := {app := λ (X_1 : category_theory.discrete punit), ((λ (_x : category_theory.discrete punit), X.to_functor.map_iso (category_theory.eq_to_iso _)) X_1).hom, naturality' := _}, unit' := _, tensor' := _}.to_nat_trans.app X_1)

def Mon_.equiv_lax_monoidal_functor_punit.counit_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C ⋙ Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C ≅ 𝟭 (Mon_ C)

Implementation of Mon_.equiv_lax_monoidal_functor_punit.

Equations

Mon_.equiv_lax_monoidal_functor_punit.counit_iso C = category_theory.nat_iso.of_components (λ (F : Mon_ C), {hom := {hom := 𝟙 ((Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C ⋙ Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C).obj F).X, one_hom' := _, mul_hom' := _}, inv := {hom := 𝟙 ((𝟭 (Mon_ C)).obj F).X, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) _

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.counit_iso_inv_app_hom (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X : Mon_ C) :

((Mon_.equiv_lax_monoidal_functor_punit.counit_iso C).inv.app X).hom = 𝟙 ((𝟭 (Mon_ C)).obj X).X

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit.counit_iso_hom_app_hom (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X : Mon_ C) :

((Mon_.equiv_lax_monoidal_functor_punit.counit_iso C).hom.app X).hom = 𝟙 ((Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C ⋙ Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C).obj X).X

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit_counit_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(Mon_.equiv_lax_monoidal_functor_punit C).counit_iso = Mon_.equiv_lax_monoidal_functor_punit.counit_iso C

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit_inverse (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(Mon_.equiv_lax_monoidal_functor_punit C).inverse = Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit_unit_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(Mon_.equiv_lax_monoidal_functor_punit C).unit_iso = Mon_.equiv_lax_monoidal_functor_punit.unit_iso C

@[simp]

theorem Mon_.equiv_lax_monoidal_functor_punit_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(Mon_.equiv_lax_monoidal_functor_punit C).functor = Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C

def Mon_.equiv_lax_monoidal_functor_punit (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.lax_monoidal_functor (category_theory.discrete punit) C ≌ Mon_ C

Monoid objects in C are "just" lax monoidal functors from the trivial monoidal category to C.

Equations

Mon_.equiv_lax_monoidal_functor_punit C = {functor := Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon C _inst_2, inverse := Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal C _inst_2, unit_iso := Mon_.equiv_lax_monoidal_functor_punit.unit_iso C _inst_2, counit_iso := Mon_.equiv_lax_monoidal_functor_punit.counit_iso C _inst_2, functor_unit_iso_comp' := _}

Projects:

Check that Mon_ Mon ≌ CommMon, via the Eckmann-Hilton argument. (You'll have to hook up the cartesian monoidal structure on Mon first, available in #3463)
Check that Mon_ Top ≌ [bundled topological monoids].
Check that Mon_ AddCommGroup ≌ Ring. (We've already got Mon_ (Module R) ≌ Algebra R, in category_theory.monoidal.internal.Module.)
Can you transport this monoidal structure to Ring or Algebra R? How does it compare to the "native" one?
Show that if C is braided then Mon_ C is naturally monoidal.