curry'_ihom_map — Mathlib

English

Let C be a monoidal closed category. For any objects X, Y, Z with X closed, and morphisms f: X → Y and g: Y → Z, the currying interacts with the internal hom via curry'(f) ≫ (ihom X).map g = curry'(f ≫ g).

Русский

Пусть C — замкнутая моноидальная категория. Пусть X, Y, Z — объекты с X закрытым, и f: X → Y, g: Y → Z. Тогда каррирование и внутреннее отображение взаимодействуют так: curry'(f) ≫ (ihom(X)).map(g) = curry'(f ≫ g).

LaTeX

$$$ curry'(f) \circ (ihom X).map(g) = curry'(f \circ g) $$$

Lean4

theorem curry'_ihom_map {X Y Z : C} [Closed X] (f : X ⟶ Y) (g : Y ⟶ Z) : curry' f ≫ (ihom X).map g = curry' (f ≫ g) :=
  by simp only [curry', ← curry_natural_right, Category.assoc]

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