ε_η_app — Mathlib

English

The η and ε components of the endofunctor monoidal structure compose to the identity on the functor's unit.

Русский

Компоненты η и ε конца моноидальной структуры композиции дают тождественный натурал.

LaTeX

$$$ (\\varepsilon F).app X \\circ (\\eta F).app X = \\mathrm{id} $$$

Lean4

@[reassoc (attr := simp)]
theorem ε_η_app (X : C) [F.Monoidal] : (ε F).app X ≫ (η F).app X = 𝟙 _ :=
  (εIso F).hom_inv_id_app X

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