unit_uniqueUpToIso_hom — Mathlib

English

If h and h' are DayConvolution structures on the same data, their units are canonically isomorphic; the two units are equal after precomposition with the canonical iso, i.e., the unit is unique up to a unique iso.

Русский

Если h и h' — структуры DayConvolution на тех же данных, их единицы канонически изоморфны; единство уникально до единого изоморфизма.

LaTeX

$$$ h(unit) \\;='\\; h'(unit) \\circ \\big(\\text{uniqueUpToIso } h h'\\big).hom$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_uniqueUpToIso_hom (h : DayConvolution F G) (h' : DayConvolution F G) :
    h.unit ≫ Functor.whiskerLeft (tensor C) (h.uniqueUpToIso h').hom = h'.unit := by simp [uniqueUpToIso]

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