of_cartesianMonoidalCategory — Mathlib

English

If F and G are monoidal functors and α: F ⇒ G is a natural transformation, then α is monoidal; i.e., the monoidal structure is compatible with α.

Русский

Если F и G — моноидальные функторы, а α: F ⇒ G — естественное преобразование, то α моноидально; т.е. структура моноидальности совместима с α.

LaTeX

$$$$\operatorname{IsMonoidal}(\alpha)$$ with coherence relations: $$\alpha_{X \otimes Y} = \alpha_X \otimes \alpha_Y, \quad \alpha_I = \mathrm{id}_I.$$$$

Lean4

instance of_cartesianMonoidalCategory (α : F ⟶ G) : IsMonoidal α
    where
  unit := (cancel_mono (Functor.Monoidal.εIso _).inv).1 (toUnit_unique _ _)
  tensor
    {X Y} := by
    rw [← cancel_mono (Functor.Monoidal.μIso _ _ _).inv]
    rw [← cancel_epi (Functor.Monoidal.μIso _ _ _).inv]
    apply CartesianMonoidalCategory.hom_ext <;> simp

Похожие утверждения