English
There is an equivalence of categories between the opposite of a product and the product of opposites: (C × D)ᵒᵖ ≅ Cᵒᵖ × Dᵒᵖ.
Русский
Существует эквивалентность категорий между противоположностью произведения и произведением противоположностей: (C × D)ᵒᵖ ≅ Cᵒᵖ × Dᵒᵖ.
LaTeX
$$$ (C \\times D)^{\\mathrm{op}} \\simeq C^{\\mathrm{op}} \\times D^{\\mathrm{op}} $$$
Lean4
/-- The equivalence between the opposite of a product and the product of the opposites. -/
@[simps!]
def prodOpEquiv : (C × D)ᵒᵖ ≌ Cᵒᵖ × Dᵒᵖ
where
functor := { obj := fun X ↦ ⟨op X.unop.1, op X.unop.2⟩, map := fun f ↦ ⟨f.unop.1.op, f.unop.2.op⟩ }
inverse := { obj := fun ⟨X, Y⟩ ↦ op ⟨X.unop, Y.unop⟩, map := fun ⟨f, g⟩ ↦ op ⟨f.unop, g.unop⟩ }
unitIso := Iso.refl _
counitIso := Iso.refl _
