op_map_comp_obj — Mathlib

English

For maps f and g, the obj level of the op version satisfies (map (f ≫ g)).op.obj U = (map f).op.obj ((map g).op.obj U).

Русский

Для отображений f и g уровень объектов противоположной категории удовлетворяет: (map (f ≫ g)).op.obj U = (map f).op.obj ((map g).op.obj U).

LaTeX

$$$ (\\mathrm{map}(f\\circ g)).\\mathrm{op}.\\mathrm{obj} U = (\\mathrm{map} f).\\mathrm{op}.\\mathrm{obj}((\\mathrm{map} g).\\mathrm{op}.\\mathrm{obj} U)$$$

Lean4

@[simp]
theorem op_map_comp_obj (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map (f ≫ g)).op.obj U = (map f).op.obj ((map g).op.obj U) :=
  rfl

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