leftUnitorEquivalence — Mathlib

English

There is an equivalence between the product of the discrete unit with C and C: Prod (Discrete PUnit) × C ≃ C, implemented by the left unitor and its inverse.

Русский

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

LaTeX

$$$\\mathrm{Prod}(\\mathrm{Discrete}(PUnit), C) \\simeq C$$$

Lean4

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

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