feat(CategoryTheory/Monoidal/Bimon): definition of bimonoid object in a braided category (#12970)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib.lean

@@ -1475,6 +1475,7 @@ import Mathlib.CategoryTheory.Monad.Monadicity
 import Mathlib.CategoryTheory.Monad.Products
 import Mathlib.CategoryTheory.Monad.Types
 import Mathlib.CategoryTheory.Monoidal.Bimod
+import Mathlib.CategoryTheory.Monoidal.Bimon_
 import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.Braided.Opposite
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Mathlib/CategoryTheory/Monoidal/Bimon_.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Mathlib.CategoryTheory.Monoidal.Comon_
+
+/-!
+# 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.
+-/
+
+noncomputable section
+
+universe v₁ v₂ u₁ u₂ u
+
+open CategoryTheory MonoidalCategory
+
+variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] [BraidedCategory C]
+
+/--
+A bimonoid object in a braided category `C` is a comonoid object in the (monoidal)
+category of monoid objects in `C`.
+-/
+def Bimon_ := Comon_ (Mon_ C)
+
+namespace Bimon_
+
+instance : Category (Bimon_ C) := inferInstanceAs (Category (Comon_ (Mon_ C)))
+
+@[ext] lemma ext {X Y : Bimon_ C} {f g : X ⟶ Y} (w : f.hom.hom = g.hom.hom) : f = g :=
+  Comon_.Hom.ext _ _ (Mon_.Hom.ext _ _ w)
+
+@[simp] theorem id_hom' (M : Bimon_ C) : Comon_.Hom.hom (𝟙 M) = 𝟙 M.X := rfl
+
+@[simp]
+theorem comp_hom' {M N K : Bimon_ C} (f : M ⟶ N) (g : N ⟶ K) : (f ≫ g).hom = f.hom ≫ g.hom :=
+  rfl
+
+/-- The forgetful functor from bimonoid objects to monoid objects. -/
+abbrev toMon_ : Bimon_ C ⥤ Mon_ C := Comon_.forget (Mon_ C)
+
+/-- The forgetful functor from bimonoid objects to the underlying category. -/
+def forget : Bimon_ C ⥤ C := toMon_ C ⋙ Mon_.forget C
+
+@[simp]
+theorem toMon_forget : toMon_ C ⋙ Mon_.forget C = forget C := rfl
+
+/-- The forgetful functor from bimonoid objects to comonoid objects. -/
+@[simps!]
+def toComon_ : Bimon_ C ⥤ Comon_ C := (Mon_.forgetMonoidal C).toOplaxMonoidalFunctor.mapComon
+
+@[simp]
+theorem toComon_forget : toComon_ C ⋙ Comon_.forget C = forget C := rfl
+
+/-- The object level part of the forward direction of `Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)` -/
+def toMon_Comon_obj (M : Bimon_ C) : Mon_ (Comon_ C) where
+  X := (toComon_ C).obj M
+  one := { hom := M.X.one }
+  mul :=
+  { hom := M.X.mul,
+    hom_comul := by dsimp; simp [tensor_μ] }
+
+attribute [simps] toMon_Comon_obj -- We add this after the fact to avoid a timeout.
+
+/-- The forward direction of `Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)` -/
+@[simps]
+def toMon_Comon_ : Bimon_ C ⥤ Mon_ (Comon_ C) where
+  obj := toMon_Comon_obj C
+  map f :=
+  { hom := (toComon_ C).map f }
+
+/-- The object level part of the backward direction of `Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)` -/
+@[simps]
+def ofMon_Comon_obj (M : Mon_ (Comon_ C)) : Bimon_ C where
+  X := (Comon_.forgetMonoidal C).toLaxMonoidalFunctor.mapMon.obj M
+  counit := { hom := M.X.counit }
+  comul :=
+  { hom := M.X.comul,
+    mul_hom := by dsimp; simp [tensor_μ] }
+
+/-- The backward direction of `Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)` -/
+@[simps]
+def ofMon_Comon_ : Mon_ (Comon_ C) ⥤ Bimon_ C where
+  obj := ofMon_Comon_obj C
+  map f :=
+  { hom := (Comon_.forgetMonoidal C).toLaxMonoidalFunctor.mapMon.map f }
+
+/-- The equivalence `Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)` -/
+def equivMon_Comon_ : Bimon_ C ≌ Mon_ (Comon_ C) where
+  functor := toMon_Comon_ C
+  inverse := ofMon_Comon_ C
+  unitIso := NatIso.ofComponents (fun _ => Comon_.mkIso (Mon_.mkIso (Iso.refl _)))
+  counitIso := NatIso.ofComponents (fun _ => Mon_.mkIso (Comon_.mkIso (Iso.refl _)))
+
+end Bimon_

Mathlib/CategoryTheory/Monoidal/Comon_.lean

@@ -46,7 +46,7 @@ structure Comon_ where
   comul_counit : comul ≫ (X ◁ counit) = (ρ_ X).inv := by aesop_cat
   comul_assoc : comul ≫ (X ◁ comul) ≫ (α_ X X X).inv = comul ≫ (comul ▷ X) := by aesop_cat
 
-attribute [reassoc] Comon_.counit_comul Comon_.comul_counit
+attribute [reassoc (attr := simp)] Comon_.counit_comul Comon_.comul_counit
 
 attribute [reassoc (attr := simp)] Comon_.comul_assoc
 
@@ -138,12 +138,12 @@ instance : (forget C).ReflectsIsomorphisms where
   reflects f e :=
     ⟨⟨{ hom := inv f.hom }, by aesop_cat⟩⟩
 
-/-- Construct an isomorphism of monoids by giving an isomorphism between the underlying objects
-and checking compatibility with unit and multiplication only in the forward direction.
+/-- Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects
+and checking compatibility with counit and comultiplication only in the forward direction.
 -/
 @[simps]
-def mkIso {M N : Comon_ C} (f : M.X ≅ N.X) (f_counit : f.hom ≫ N.counit = M.counit)
-    (f_comul : f.hom ≫ N.comul = M.comul ≫ (f.hom ⊗ f.hom)) : M ≅ N where
+def mkIso {M N : Comon_ C} (f : M.X ≅ N.X) (f_counit : f.hom ≫ N.counit = M.counit := by aesop_cat)
+    (f_comul : f.hom ≫ N.comul = M.comul ≫ (f.hom ⊗ f.hom) := by aesop_cat) : M ≅ N where
   hom :=
     { hom := f.hom
       hom_counit := f_counit
@@ -275,7 +275,16 @@ theorem tensorObj_comul (A B : Comon_ C) :
   apply Quiver.Hom.unop_inj
   dsimp [op_tensorObj, op_associator]
   rw [Category.assoc, Category.assoc, Category.assoc]
-  rfl
+
+/-- The forgetful functor from `Comon_ C` to `C` is monoidal when `C` is braided monoidal. -/
+def forgetMonoidal : MonoidalFunctor (Comon_ C) C :=
+  { forget C with
+    ε := 𝟙 _
+    μ := fun X Y => 𝟙 _ }
+
+@[simp] theorem forgetMonoidal_toFunctor : (forgetMonoidal C).toFunctor = forget C := rfl
+@[simp] theorem forgetMonoidal_ε : (forgetMonoidal C).ε = 𝟙 (𝟙_ C) := rfl
+@[simp] theorem forgetMonoidal_μ (X Y : Comon_ C) : (forgetMonoidal C).μ X Y = 𝟙 (X.X ⊗ Y.X) := rfl
 
 end Comon_
 
@@ -318,5 +327,4 @@ def mapComon (F : OplaxMonoidalFunctor C D) : Comon_ C ⥤ Comon_ D where
 -- TODO We haven't yet set up the category structure on `OplaxMonoidalFunctor C D`
 -- and so can't state `mapComonFunctor : OplaxMonoidalFunctor C D ⥤ Comon_ C ⥤ Comon_ D`.
 
-
 end CategoryTheory.OplaxMonoidalFunctor

Mathlib/CategoryTheory/Monoidal/Functor.lean

@@ -286,6 +286,7 @@ noncomputable def MonoidalFunctor.μIso (F : MonoidalFunctor.{v₁, v₂} C D) (
 #align category_theory.monoidal_functor.μ_iso CategoryTheory.MonoidalFunctor.μIso
 
 /-- The underlying oplax monoidal functor of a (strong) monoidal functor. -/
+@[simps]
 noncomputable def MonoidalFunctor.toOplaxMonoidalFunctor (F : MonoidalFunctor C D) :
     OplaxMonoidalFunctor C D :=
   { F with

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -164,8 +164,8 @@ instance : (forget C).ReflectsIsomorphisms where
 and checking compatibility with unit and multiplication only in the forward direction.
 -/
 @[simps]
-def isoOfIso {M N : Mon_ C} (f : M.X ≅ N.X) (one_f : M.one ≫ f.hom = N.one)
-    (mul_f : M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul) : M ≅ N where
+def mkIso {M N : Mon_ C} (f : M.X ≅ N.X) (one_f : M.one ≫ f.hom = N.one := by aesop_cat)
+    (mul_f : M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul := by aesop_cat) : M ≅ N where
   hom :=
     { hom := f.hom
       one_hom := one_f
@@ -177,7 +177,7 @@ def isoOfIso {M N : Mon_ C} (f : M.X ≅ N.X) (one_f : M.one ≫ f.hom = N.one)
         rw [← cancel_mono f.hom]
         slice_rhs 2 3 => rw [mul_f]
         simp }
-#align Mon_.iso_of_iso Mon_.isoOfIso
+#align Mon_.iso_of_iso Mon_.mkIso
 
 instance uniqueHomFromTrivial (A : Mon_ C) : Unique (trivial C ⟶ A) where
   default :=
@@ -493,13 +493,26 @@ instance monMonoidalStruct : MonoidalCategoryStruct (Mon_ C) :=
     whiskerRight := fun f Y => tensorHom f (𝟙 Y)
     whiskerLeft := fun X _ _ g => tensorHom (𝟙 X) g
     tensorUnit := trivial C
-    associator := fun M N P ↦ isoOfIso (α_ M.X N.X P.X) one_associator mul_associator
-    leftUnitor := fun M ↦ isoOfIso (λ_ M.X) one_leftUnitor mul_leftUnitor
-    rightUnitor := fun M ↦ isoOfIso (ρ_ M.X) one_rightUnitor mul_rightUnitor }
+    associator := fun M N P ↦ mkIso (α_ M.X N.X P.X) one_associator mul_associator
+    leftUnitor := fun M ↦ mkIso (λ_ M.X) one_leftUnitor mul_leftUnitor
+    rightUnitor := fun M ↦ mkIso (ρ_ M.X) one_rightUnitor mul_rightUnitor }
 
 @[simp]
 theorem tensorUnit_X : (𝟙_ (Mon_ C)).X = 𝟙_ C := rfl
 
+@[simp]
+theorem tensorUnit_one : (𝟙_ (Mon_ C)).one = 𝟙 (𝟙_ C) := rfl
+
+@[simp]
+theorem tensorUnit_mul : (𝟙_ (Mon_ C)).mul = (λ_ (𝟙_ C)).hom := rfl
+
+@[simp]
+theorem tensorObj_one (X Y : Mon_ C) : (X ⊗ Y).one = (λ_ (𝟙_ C)).inv ≫ (X.one ⊗ Y.one) := rfl
+
+@[simp]
+theorem tensorObj_mul (X Y : Mon_ C) :
+    (X ⊗ Y).mul = tensor_μ C (X.X, Y.X) (X.X, Y.X) ≫ (X.mul ⊗ Y.mul) := rfl
+
 @[simp]
 theorem whiskerLeft_hom {X Y : Mon_ C} (f : X ⟶ Y) (Z : Mon_ C) :
     (f ▷ Z).hom = f.hom ▷ Z.X := by
@@ -598,7 +611,7 @@ theorem mul_braiding {X Y : Mon_ C} :
   simp only [Category.assoc]
 
 instance : SymmetricCategory (Mon_ C) where
-  braiding := fun X Y => isoOfIso (β_ X.X Y.X) one_braiding mul_braiding
+  braiding := fun X Y => mkIso (β_ X.X Y.X) one_braiding mul_braiding
   symmetry := fun X Y => by
     ext
     simp [← SymmetricCategory.braiding_swap_eq_inv_braiding]

Mathlib/CategoryTheory/Opposites.lean

@@ -49,6 +49,10 @@ theorem Quiver.Hom.unop_op {X Y : C} (f : X ⟶ Y) : f.op.unop = f :=
   rfl
 #align quiver.hom.unop_op Quiver.Hom.unop_op
 
+@[simp]
+theorem Quiver.Hom.unop_op' {X Y : Cᵒᵖ} {x} :
+    @Quiver.Hom.unop C _ X Y no_index (Opposite.op (unop := x)) = x := rfl
+
 @[simp]
 theorem Quiver.Hom.op_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f :=
   rfl