instHasCoproductOppositeOp — Mathlib

English

The inverse composed with the lift equals the descend of f'.op.

Русский

Обратное, сопоставленное с подъемом, равно descend(f'.op).

LaTeX

$$$(\mathrm{opProductIsoCoproduct}'(hf, hc))^{-1} \circ (hf.lift f')^{\mathrm{op}} = hc.desc f'.op$$

Lean4

instance : HasCoproduct (op <| Z ·) :=
  hasColimit_of_iso
    ((Discrete.natIsoFunctor ≪≫ Discrete.natIso (fun _ ↦ by rfl)) :
        (Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op ≅ Discrete.functor (op <| Z ·)).symm

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