nonempty_monoidal_iff_preservesFiniteProducts

English

Let F be a functor between Cartesian monoidal categories. Then F is monoidal if and only if F preserves finite products.

Русский

Пусть F — функтор между декартовыми моноидальными категориями. Тогда F моноидален тогда и только тогда, когда F сохраняет конечные произведения.

LaTeX

$$$$\operatorname{IsMonoidal}(F) \iff \operatorname{PreservesFiniteProducts}(F).$$$$

Lean4

/-- A functor between Cartesian monoidal categories is monoidal iff it preserves finite products.
-/
theorem nonempty_monoidal_iff_preservesFiniteProducts : Nonempty F.Monoidal ↔ PreservesFiniteProducts F :=
  ⟨fun ⟨_⟩ ↦ inferInstance, fun _ ↦ ⟨ofChosenFiniteProducts F⟩⟩

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