prod_map_pre_app_comp_ev — Mathlib

English

If f: B ⟶ A with B exponentiable and X an object, then (B ◁ (pre f).app X) ≫ (exp.ev B).app X = f ▷ (A ⟹ X) ≫ (exp A).app X.

Русский

Пусть f: B ⟶ A и B экспоненцируем, пусть X — произвольный объект. Тогда выполняется равенство: (B ◁ (pre f).app X) ≫ (exp.ev B).app X = f ▷ (A ⟹ X) ≫ (exp A).app X.

LaTeX

$$$ (B \\triangleleft (\\mathrm{pre}\, f).\\mathrm{app}\\,X) \\;\\gg\\; (\\exp\\mathrm{ev}\\, B).\\mathrm{app}\\,X \\\\ = \\\\ f \\triangleright (A \\Rightarrow X) \\;\\gg\\; (\\exp A).\\mathrm{ev}.app X $$$

Lean4

theorem prod_map_pre_app_comp_ev (f : B ⟶ A) [Exponentiable B] (X : C) :
    (B ◁ (pre f).app X) ≫ (exp.ev B).app X = f ▷ (A ⟹ X) ≫ (exp.ev A).app X :=
  conjugateEquiv_counit _ _ ((tensoringLeft _).map f) X

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