id_tensor_pre_app_comp_ev — Mathlib

English

A compatibility equality between left-tensor whiskering, pre-app, and evaluation holds: B ◁ (pre f) ≔ ev-type equality with f.

Русский

Совместимость слева по тензору, pre-app и оценивание: выполняется равенство, связывающее эти операции.

LaTeX

$$$ B \triangleleft (\mathrm{pre} f).\mathrm{app} X \;\circ\; (\mathrm{ihom.ev} B).\mathrm{app} X = f \triangleright (A \to X) \circ (\mathrm{ihom.ev} A).\mathrm{app} X $$$

Lean4

@[reassoc (attr := simp)]
theorem id_tensor_pre_app_comp_ev (f : B ⟶ A) (X : C) :
    B ◁ (pre f).app X ≫ (ihom.ev B).app X = f ▷ (A ⟶[C] X) ≫ (ihom.ev A).app X :=
  conjugateEquiv_counit _ _ ((tensoringLeft C).map f) X

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