The category of bimonoids in a braided monoidal category.

We define bimonoids in a braided monoidal category C as comonoid objects in the category of monoid objects in C.

We verify that this is equivalent to the monoid objects in the category of comonoid objects.

TODO

• Define Hopf monoids, which in a cartesian monoidal category are exactly group objects, and use this to define group schemes.
• Construct the category of modules, and show that it is monoidal with a monoidal forgetful functor to C.
• Some form of Tannaka reconstruction: given a monoidal functor F : C ⥤ D into a braided category D, the internal endomorphisms of F form a bimonoid in presheaves on D, in good circumstances this is representable by a bimonoid in D, and then C is monoidally equivalent to the modules over that bimonoid.

def Bimon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Type (max (max u₁ v₁) v₁)

A bimonoid object in a braided category C is a comonoid object in the (monoidal) category of monoid objects in C.

Equations

• Bimon_ C = Comon_ (Mon_ C)

instance Bimon_.instCategory (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Category.{v₁, max u₁ v₁} (Bimon_ C)

Equations

• Bimon_.instCategory C = inferInstanceAs (CategoryTheory.Category.{v₁, max u₁ v₁} (Comon_ (Mon_ C)))

theorem Bimon_.ext (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : Bimon_ C} {Y : Bimon_ C} {f : X ⟶ Y} {g : X ⟶ Y} (w : f.hom.hom = g.hom.hom) : f = g

@[simp]

theorem Bimon_.id_hom' (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X

@[simp]

theorem Bimon_.comp_hom' (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Bimon_ C} {N : Bimon_ C} {K : Bimon_ C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[reducible, inline]

abbrev Bimon_.toMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (Bimon_ C) (Mon_ C)

The forgetful functor from bimonoid objects to monoid objects.

Equations

• Bimon_.toMon_ C = Comon_.forget (Mon_ C)

def Bimon_.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (Bimon_ C) C

The forgetful functor from bimonoid objects to the underlying category.

Equations

• Bimon_.forget C = (Bimon_.toMon_ C).comp (Mon_.forget C)

@[simp]

theorem Bimon_.toMon_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (Bimon_.toMon_ C).comp (Mon_.forget C) = Bimon_.forget C

@[simp]

theorem Bimon_.toComon__obj_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) : ((Bimon_.toComon_ C).obj A).comul = A.comul.hom

@[simp]

theorem Bimon_.toComon__map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ {X Y : Comon_ (Mon_ C)} (f : X ⟶ Y), ((Bimon_.toComon_ C).map f).hom = f.hom.hom

@[simp]

theorem Bimon_.toComon__obj_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) : ((Bimon_.toComon_ C).obj A).counit = A.counit.hom

@[simp]

theorem Bimon_.toComon__obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) : ((Bimon_.toComon_ C).obj A).X = A.X.X

def Bimon_.toComon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (Bimon_ C) (Comon_ C)

The forgetful functor from bimonoid objects to comonoid objects.

Equations

• Bimon_.toComon_ C = (Mon_.forgetMonoidal C).toOplaxMonoidalFunctor.mapComon

@[simp]

theorem Bimon_.toComon_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (Bimon_.toComon_ C).comp (Comon_.forget C) = Bimon_.forget C

def Bimon_.toMon_Comon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : Mon_ (Comon_ C)

The object level part of the forward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bimon_.toMon_Comon_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : (Bimon_.toMon_Comon_obj C M).X = (Bimon_.toComon_ C).obj M

@[simp]

theorem Bimon_.toMon_Comon_obj_one_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : (Bimon_.toMon_Comon_obj C M).one.hom = M.X.one

@[simp]

theorem Bimon_.toMon_Comon_obj_mul_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : (Bimon_.toMon_Comon_obj C M).mul.hom = M.X.mul

@[simp]

theorem Bimon_.toMon_Comon__obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : (Bimon_.toMon_Comon_ C).obj M = Bimon_.toMon_Comon_obj C M

@[simp]

theorem Bimon_.toMon_Comon__map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ {X Y : Bimon_ C} (f : X ⟶ Y), ((Bimon_.toMon_Comon_ C).map f).hom = (Bimon_.toComon_ C).map f

def Bimon_.toMon_Comon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (Bimon_ C) (Mon_ (Comon_ C))

The forward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bimon_.ofMon_Comon_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (Bimon_.ofMon_Comon_obj C M).X = (Comon_.forgetMonoidal C).mapMon.obj M

@[simp]

theorem Bimon_.ofMon_Comon_obj_comul_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (Bimon_.ofMon_Comon_obj C M).comul.hom = M.X.comul

@[simp]

theorem Bimon_.ofMon_Comon_obj_counit_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (Bimon_.ofMon_Comon_obj C M).counit.hom = M.X.counit

def Bimon_.ofMon_Comon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : Bimon_ C

The object level part of the backward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bimon_.ofMon_Comon__obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (Bimon_.ofMon_Comon_ C).obj M = Bimon_.ofMon_Comon_obj C M

@[simp]

theorem Bimon_.ofMon_Comon__map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ {X Y : Mon_ (Comon_ C)} (f : X ⟶ Y), ((Bimon_.ofMon_Comon_ C).map f).hom = (Comon_.forgetMonoidal C).mapMon.map f

def Bimon_.ofMon_Comon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (Mon_ (Comon_ C)) (Bimon_ C)

The backward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

• One or more equations did not get rendered due to their size.

def Bimon_.equivMon_Comon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Bimon_ C ≌ Mon_ (Comon_ C)

The equivalence Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

• One or more equations did not get rendered due to their size.