feat: port CategoryTheory.Monoidal.Skeleton (#4844)

Mathlib.lean

@@ -921,6 +921,7 @@ import Mathlib.CategoryTheory.Monoidal.Preadditive
 import Mathlib.CategoryTheory.Monoidal.Rigid.Basic
 import Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
+import Mathlib.CategoryTheory.Monoidal.Skeleton
 import Mathlib.CategoryTheory.Monoidal.Subcategory
 import Mathlib.CategoryTheory.Monoidal.Tor
 import Mathlib.CategoryTheory.Monoidal.Transport

Mathlib/CategoryTheory/Monoidal/Skeleton.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2021 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+
+! This file was ported from Lean 3 source module category_theory.monoidal.skeleton
+! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Transport
+import Mathlib.CategoryTheory.Skeletal
+
+/-!
+# The monoid on the skeleton of a monoidal category
+
+The skeleton of a monoidal category is a monoid.
+-/
+
+
+namespace CategoryTheory
+
+open MonoidalCategory
+
+universe v u
+
+variable {C : Type u} [Category.{v} C] [MonoidalCategory C]
+
+/-- If `C` is monoidal and skeletal, it is a monoid.
+See note [reducible non-instances]. -/
+@[reducible]
+def monoidOfSkeletalMonoidal (hC : Skeletal C) : Monoid C where
+  mul X Y := (X ⊗ Y : C)
+  one := (𝟙_ C : C)
+  one_mul X := hC ⟨λ_ X⟩
+  mul_one X := hC ⟨ρ_ X⟩
+  mul_assoc X Y Z := hC ⟨α_ X Y Z⟩
+#align category_theory.monoid_of_skeletal_monoidal CategoryTheory.monoidOfSkeletalMonoidal
+
+/-- If `C` is braided and skeletal, it is a commutative monoid. -/
+def commMonoidOfSkeletalBraided [BraidedCategory C] (hC : Skeletal C) : CommMonoid C :=
+  { monoidOfSkeletalMonoidal hC with mul_comm := fun X Y => hC ⟨β_ X Y⟩ }
+#align category_theory.comm_monoid_of_skeletal_braided CategoryTheory.commMonoidOfSkeletalBraided
+
+/-- The skeleton of a monoidal category has a monoidal structure itself, induced by the equivalence.
+-/
+noncomputable instance : MonoidalCategory (Skeleton C) :=
+  Monoidal.transport (skeletonEquivalence C).symm
+
+/--
+The skeleton of a monoidal category can be viewed as a monoid, where the multiplication is given by
+the tensor product, and satisfies the monoid axioms since it is a skeleton.
+-/
+noncomputable instance : Monoid (Skeleton C) :=
+  monoidOfSkeletalMonoidal (skeletonIsSkeleton _).skel
+
+-- TODO: Transfer the braided structure to the skeleton of C along the equivalence, and show that
+-- the skeleton is a commutative monoid.
+end CategoryTheory