op_map_id_obj — Mathlib

English

In the opposite category, the map induced by the identity has object equality: (map(id_X)).op.obj U = U.

Русский

В противоположной категории отображение, порождённое тождеством, сохраняет открытость: (map(id_X)).op.obj U = U.

LaTeX

$$$(\\mathrm{map}(\\mathrm{id}_X)).\\mathrm{op}.\\mathrm{obj} U = U$$$

Lean4

theorem op_map_id_obj (U : (Opens X)ᵒᵖ) : (map (𝟙 X)).op.obj U = U := by simp

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