mathlib

94a52c43 - feat(category_theory/monoidal): prove that in a braided monoidal category unitors and associators are monoidal natural transformations (#13121)

feat(category_theory/monoidal): prove that in a braided monoidal category unitors and associators are monoidal natural transformations (#13121) This PR contains proofs of lemmas that are used in the stacked PR to define a monoidal structure on the category of monoids in a braided monoidal category. The lemmas can be summarised by saying that in a braided monoidal category unitors and associators are monoidal natural transformations. Note that for these statements to make sense we would need to define monoidal functors that are sources and targets of these monoidal natural transformations. For example, the morphisms `(α_ X Y Z).hom` are the components of a monoidal natural transformation ``` (tensor.prod (𝟭 C)) ⊗⋙ tensor ⟶ Α_ ⊗⋙ ((𝟭 C).prod tensor) ⊗⋙ tensor ``` where `Α_ : monoidal_functor ((C × C) × C) (C × (C × C))` is the associator functor given by `λ X, (X.1.1, (X.1.2, X.2))` on objects. I didn't define the functor `Α_`. (The easiest way would be to build it up using `prod'` we have already defined from `fst` and `snd`, which we would need to define as monoidal functors.) Instead, I stated and proved the commutative diagram that expresses the monoidality of the above transformation. Ditto for unitors. Please let me know if you'd like me to define all the required functors and monoidal natural transformations. The monoidal natural transformations themselves are not used in the proof that the category of monoids in a braided monoidal category is monoidal and only provide meaningful names to the lemmas that are used in the proof. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net>