opCoproductIsoProduct — Mathlib

English

The canonical isomorphism between the opposite of the coproduct and the product in the opposite category is defined by opCoproductIsoProduct'.

Русский

Каноническое изоморфизмop(копроизведение) к произведению в противоположной категории задаётся через opCoproductIsoProduct'.

LaTeX

$$$\\text{opCoproductIsoProduct} := \\text{opCoproductIsoProduct'} (coproductIsCoproduct Z) (productIsProduct (op \\circ Z))$$$

Lean4

/-- The canonical isomorphism from the opposite of the coproduct to the product in the opposite
category.
-/
def opCoproductIsoProduct : op (∐ Z) ≅ ∏ᶜ (op <| Z ·) :=
  opCoproductIsoProduct' (coproductIsCoproduct Z) (productIsProduct (op <| Z ·))

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