mathlib docs: category_theory.monoidal.CommMon

source

structure CommMon_ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

Type (max u₁ v₁)

to_Mon_ : Mon_ C
mul_comm' : (β_ c.to_Mon_.X c.to_Mon_.X).hom ≫ c.to_Mon_.mul = c.to_Mon_.mul . "obviously"

A commutative monoid object internal to a monoidal category.

source

@[simp]

theorem CommMon_.trivial_to_Mon_ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(CommMon_.trivial C).to_Mon_ = Mon_.trivial C

source

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

CommMon_ C

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

Equations

CommMon_.trivial C = {to_Mon_ := {X := (Mon_.trivial C).X, one := (Mon_.trivial C).one, mul := (Mon_.trivial C).mul, one_mul' := _, mul_one' := _, mul_assoc' := _}, mul_comm' := _}

source

@[instance]

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

inhabited (CommMon_ C)

Equations

CommMon_.inhabited C = {default := CommMon_.trivial C _inst_3}

source

@[instance]

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

category_theory.category (CommMon_ C)

Equations

CommMon_.category_theory.category = category_theory.induced_category.category CommMon_.to_Mon_

source

@[simp]

theorem CommMon_.id_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (A : CommMon_ C) :

(𝟙 A).hom = 𝟙 A.to_Mon_.X

source

@[simp]

theorem CommMon_.comp_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {R S T : CommMon_ C} (f : R ⟶ S) (g : S ⟶ T) :

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

source

def CommMon_.forget₂_Mon_ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

CommMon_ C ⥤ Mon_ C

The forgetful functor from commutative monoid objects to monoid objects.

Equations

CommMon_.forget₂_Mon_ C = category_theory.induced_functor CommMon_.to_Mon_

source

@[instance]

def CommMon_.forget₂_Mon_.full (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

category_theory.full (CommMon_.forget₂_Mon_ C)

source

@[instance]

def CommMon_.forget₂_Mon_.faithful (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

category_theory.faithful (CommMon_.forget₂_Mon_ C)

source

@[simp]

theorem CommMon_.forget₂_Mon_obj_one (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (A : CommMon_ C) :

((CommMon_.forget₂_Mon_ C).obj A).one = A.to_Mon_.one

source

@[simp]

theorem CommMon_.forget₂_Mon_obj_mul (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (A : CommMon_ C) :

((CommMon_.forget₂_Mon_ C).obj A).mul = A.to_Mon_.mul

source

@[simp]

theorem CommMon_.forget₂_Mon_map_hom (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {A B : CommMon_ C} (f : A ⟶ B) :

((CommMon_.forget₂_Mon_ C).map f).hom = f.hom

source

@[instance]

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

unique (CommMon_.trivial C ⟶ A)

Equations

A.unique_hom_from_trivial = A.to_Mon_.unique_hom_from_trivial

source

@[instance]

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

category_theory.limits.has_initial (CommMon_ C)

source

def category_theory.lax_braided_functor.map_CommMon {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] (F : category_theory.lax_braided_functor C D) :

CommMon_ C ⥤ CommMon_ D

A lax braided functor takes commutative monoid objects to commutative monoid objects.

That is, a lax braided functor F : C ⥤ D induces a functor CommMon_ C ⥤ CommMon_ D.

Equations

F.map_CommMon = {obj := λ (A : CommMon_ C), {to_Mon_ := {X := (F.to_lax_monoidal_functor.map_Mon.obj A.to_Mon_).X, one := (F.to_lax_monoidal_functor.map_Mon.obj A.to_Mon_).one, mul := (F.to_lax_monoidal_functor.map_Mon.obj A.to_Mon_).mul, one_mul' := _, mul_one' := _, mul_assoc' := _}, mul_comm' := _}, map := λ (A B : CommMon_ C) (f : A ⟶ B), F.to_lax_monoidal_functor.map_Mon.map f, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.lax_braided_functor.map_CommMon_map {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] (F : category_theory.lax_braided_functor C D) (A B : CommMon_ C) (f : A ⟶ B) :

F.map_CommMon.map f = F.to_lax_monoidal_functor.map_Mon.map f

source

@[simp]

theorem category_theory.lax_braided_functor.map_CommMon_obj_to_Mon_ {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] (F : category_theory.lax_braided_functor C D) (A : CommMon_ C) :

(F.map_CommMon.obj A).to_Mon_ = F.to_lax_monoidal_functor.map_Mon.obj A.to_Mon_

source

def category_theory.lax_braided_functor.map_CommMon_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] :

category_theory.lax_braided_functor C D ⥤ CommMon_ C ⥤ CommMon_ D

map_CommMon is functorial in the lax braided functor.

Equations

category_theory.lax_braided_functor.map_CommMon_functor C D = {obj := category_theory.lax_braided_functor.map_CommMon _inst_6, map := λ (F G : category_theory.lax_braided_functor C D) (α : F ⟶ G), {app := λ (A : CommMon_ C), {hom := α.to_nat_trans.app A.to_Mon_.X, one_hom' := _, mul_hom' := _}, naturality' := _}, map_id' := _, map_comp' := _}

source

def CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

category_theory.lax_braided_functor (category_theory.discrete punit) C ⥤ CommMon_ C

Implementation of CommMon_.equiv_lax_braided_functor_punit.

Equations

CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C = {obj := λ (F : category_theory.lax_braided_functor (category_theory.discrete punit) C), F.map_CommMon.obj (CommMon_.trivial (category_theory.discrete punit)), map := λ (F G : category_theory.lax_braided_functor (category_theory.discrete punit) C) (α : F ⟶ G), ((category_theory.lax_braided_functor.map_CommMon_functor (category_theory.discrete punit) C).map α).app (CommMon_.trivial (category_theory.discrete punit)), map_id' := _, map_comp' := _}

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon_obj (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (F : category_theory.lax_braided_functor (category_theory.discrete punit) C) :

(CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C).obj F = F.map_CommMon.obj (CommMon_.trivial (category_theory.discrete punit))

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon_map (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (F G : category_theory.lax_braided_functor (category_theory.discrete punit) C) (α : F ⟶ G) :

(CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C).map α = ((category_theory.lax_braided_functor.map_CommMon_functor (category_theory.discrete punit) C).map α).app (CommMon_.trivial (category_theory.discrete punit))

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided_obj_to_lax_monoidal_functor_to_functor_map (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (A : CommMon_ C) (_x _x_1 : category_theory.discrete punit) (_x_2 : _x ⟶ _x_1) :

((CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C).obj A).to_lax_monoidal_functor.to_functor.map _x_2 = 𝟙 A.to_Mon_.X

source

def CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

CommMon_ C ⥤ category_theory.lax_braided_functor (category_theory.discrete punit) C

Implementation of CommMon_.equiv_lax_braided_functor_punit.

Equations

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

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided_map_to_nat_trans_app (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (A B : CommMon_ C) (f : A ⟶ B) (_x : category_theory.discrete punit) :

((CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C).map f).to_nat_trans.app _x = f.hom

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided_obj_to_lax_monoidal_functor_to_functor_obj (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (A : CommMon_ C) (_x : category_theory.discrete punit) :

((CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C).obj A).to_lax_monoidal_functor.to_functor.obj _x = A.to_Mon_.X

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided_obj_to_lax_monoidal_functor_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (A : CommMon_ C) :

((CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C).obj A).to_lax_monoidal_functor.ε = A.to_Mon_.one

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided_obj_to_lax_monoidal_functor_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (A : CommMon_ C) (_x _x_1 : category_theory.discrete punit) :

((CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C).obj A).to_lax_monoidal_functor.μ _x _x_1 = A.to_Mon_.mul

source

def CommMon_.equiv_lax_braided_functor_punit.unit_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

𝟭 (category_theory.lax_braided_functor (category_theory.discrete punit) C) ≅ CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C ⋙ CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C

Implementation of CommMon_.equiv_lax_braided_functor_punit.

Equations

CommMon_.equiv_lax_braided_functor_punit.unit_iso C = category_theory.nat_iso.of_components (λ (F : category_theory.lax_braided_functor (category_theory.discrete punit) C), category_theory.lax_braided_functor.mk_iso (category_theory.monoidal_nat_iso.of_components (λ (_x : category_theory.discrete punit), F.to_lax_monoidal_functor.to_functor.map_iso (category_theory.eq_to_iso _)) _ _ _)) _

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.unit_iso_inv_app_to_nat_trans_app (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : category_theory.lax_braided_functor (category_theory.discrete punit) C) (X_1 : category_theory.discrete punit) :

((CommMon_.equiv_lax_braided_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_lax_monoidal_functor.to_functor.map_iso (category_theory.eq_to_iso _)) X_1).hom, naturality' := _}, unit' := _, tensor' := _}.to_nat_trans.app X_1)

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.unit_iso_hom_app_to_nat_trans_app (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : category_theory.lax_braided_functor (category_theory.discrete punit) C) (X_1 : category_theory.discrete punit) :

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

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.counit_iso_inv_app_hom (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : CommMon_ C) :

((CommMon_.equiv_lax_braided_functor_punit.counit_iso C).inv.app X).hom = 𝟙 ((𝟭 (CommMon_ C)).obj X).to_Mon_.X

source

def CommMon_.equiv_lax_braided_functor_punit.counit_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C ⋙ CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C ≅ 𝟭 (CommMon_ C)

Implementation of CommMon_.equiv_lax_braided_functor_punit.

Equations

CommMon_.equiv_lax_braided_functor_punit.counit_iso C = category_theory.nat_iso.of_components (λ (F : CommMon_ C), {hom := {hom := 𝟙 ((CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C ⋙ CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C).obj F).to_Mon_.X, one_hom' := _, mul_hom' := _}, inv := {hom := 𝟙 ((𝟭 (CommMon_ C)).obj F).to_Mon_.X, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) _

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit.counit_iso_hom_app_hom (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : CommMon_ C) :

((CommMon_.equiv_lax_braided_functor_punit.counit_iso C).hom.app X).hom = 𝟙 ((CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C ⋙ CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C).obj X).to_Mon_.X

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(CommMon_.equiv_lax_braided_functor_punit C).functor = CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C

source

def CommMon_.equiv_lax_braided_functor_punit (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

category_theory.lax_braided_functor (category_theory.discrete punit) C ≌ CommMon_ C

Commutative monoid objects in C are "just" braided lax monoidal functors from the trivial braided monoidal category to C.

Equations

CommMon_.equiv_lax_braided_functor_punit C = {functor := CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon C _inst_3, inverse := CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C _inst_3, unit_iso := CommMon_.equiv_lax_braided_functor_punit.unit_iso C _inst_3, counit_iso := CommMon_.equiv_lax_braided_functor_punit.counit_iso C _inst_3, functor_unit_iso_comp' := _}

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit_inverse (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(CommMon_.equiv_lax_braided_functor_punit C).inverse = CommMon_.equiv_lax_braided_functor_punit.CommMon_to_lax_braided C

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit_unit_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(CommMon_.equiv_lax_braided_functor_punit C).unit_iso = CommMon_.equiv_lax_braided_functor_punit.unit_iso C

source

@[simp]

theorem CommMon_.equiv_lax_braided_functor_punit_counit_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(CommMon_.equiv_lax_braided_functor_punit C).counit_iso = CommMon_.equiv_lax_braided_functor_punit.counit_iso C

mathlib documentation

The category of commutative monoids in a braided monoidal category.