map_id_obj' — Mathlib

English

In the opposite category, the map for the identity preserves the opposite opens: (map id_X).obj (unop U) = unop U.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_id_obj' (U) (p) : (map (𝟙 X)).obj ⟨U, p⟩ = ⟨U, p⟩ :=
  rfl

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