rightUnitorEquivalence — Mathlib

English

There is an equivalence between C × Discrete(PUnit) and C, given by the right unitor and its inverse.

Русский

Существует эквивалентность между C × Discrete(PUnit) и C, заданная правым унитором и его обратной.

LaTeX

$$$C \\times \\mathrm{Discrete}(PUnit) \\simeq C$$$

Lean4

/-- The equivalence of categories expressing right unity of products of categories. -/
@[simps]
def rightUnitorEquivalence : C × Discrete (PUnit : Type w) ≌ C
    where
  functor := rightUnitor C
  inverse := rightInverseUnitor C
  unitIso := Iso.refl _
  counitIso := Iso.refl _

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