coev_app_comp_pre_app — Mathlib

English

ACompatibility: (pre f).app_Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z.

Русский

Совместимость: (pre f).app_Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z.

LaTeX

$$$ (\mathrm{pre} f).\mathrm{app} Y \;\gg\; (\mathrm{ihom} W).map g = (\mathrm{ihom} X).map g \;\gg\; (\mathrm{pre} f).\mathrm{app} Z $$$

Lean4

@[reassoc (attr := simp)]
theorem coev_app_comp_pre_app (f : B ⟶ A) :
    (ihom.coev A).app X ≫ (pre f).app (A ⊗ X) = (ihom.coev B).app X ≫ (ihom B).map (f ▷ _) :=
  unit_conjugateEquiv _ _ ((tensoringLeft C).map f) X

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