opProdIsoCoprod — Mathlib

English

The composite of the primed opProdIsoCoprod with its inverse equals the opposite of the cocone-point-unique iso between hc and hc'.

Русский

Составление опп ProdIsoCoprod' с его обратным равняется противоположности единообразного изоморфизма hc и hc'.

LaTeX

$$(opProdIsoCoprod' hf hc).hom ≫ (opProdIsoCoprod' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv$$

Lean4

/-- The canonical isomorphism from the opposite of the binary product to the coproduct in the opposite
category.
-/
def opProdIsoCoprod : op (A ⨯ B) ≅ (op A ⨿ op B)
    where
  hom := (prod.lift coprod.inl.unop coprod.inr.unop).op
  inv := coprod.desc prod.fst.op prod.snd.op
  hom_inv_id := by
    apply Quiver.Hom.unop_inj
    ext <;>
      · simp only
        apply Quiver.Hom.op_inj
        simp
  inv_hom_id := by
    ext <;>
      · simp only [colimit.ι_desc_assoc]
        apply Quiver.Hom.unop_inj
        simp

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