εIso

Mathlib.CategoryTheory.Monoidal.Functor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Monoidal.εIso

English

Coherence relationship between δ, η, and tensorHom in another layout.

Русский

Кохерентность δ, η и tensorHom в другом расположении.

LaTeX

$$$δ F X (I) ∘ (η F ⊗ f) = F.map (λ_X) ∘ (λ_{F X})^{-1} ∘ f$$$

Lean4

/-- The isomorphism `𝟙_ D ≅ F.obj (𝟙_ C)` when `F` is a monoidal functor. -/
@[simps]
def εIso : 𝟙_ D ≅ F.obj (𝟙_ C) where
  hom := ε F
  inv := η F

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru