rightInverseUnitor — Mathlib

English

There is a right inverse unitor: rightInverseUnitor: C ⥤ C × Discrete(PUnit) which maps X to (X, ∗) and f to (f, id).

Русский

Существует правый обратный унитор: C ⥤ C × Discrete(PUnit), который отправляет X в (X, ∗) и морфизм f в (f, id).

LaTeX

$$$\\mathrm{rightInverseUnitor}: \\mathcal{C} \\to \\mathcal{C} \\times \\mathrm{Discrete}(PUnit)$ with $\\mathrm{obj}(X) = (X, ∗)$ and $\\mathrm{map}(f) = (f, id)$$$

Lean4

/-- The right inverse unitor `C ⥤ C × 1` -/
@[simps]
def rightInverseUnitor : C ⥤ C × Discrete (PUnit : Type w)
    where
  obj X := ⟨X, ⟨PUnit.unit⟩⟩
  map f := ⟨f, 𝟙 _⟩

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