mapId — Mathlib

English

The map associated to the identity is equal to the identity functor on Opens X: map(identity) = identity.

Русский

Отображение, соответствующее тождественному отображению, совпадает с тождественным функтором на Opens X: map(identity) = identity.

LaTeX

$$$\\mathrm{map}(\\mathrm{id}_X) = \\mathrm{id}_{\\mathrm{Opens}(X)}$$$

Lean4

/-- The functor `Opens X ⥤ Opens X` given by taking preimages under the identity function
is naturally isomorphic to the identity functor.
-/
@[simps]
def mapId : map (𝟙 X) ≅ 𝟭 (Opens X)
    where
  hom := { app := fun U => eqToHom (map_id_obj U) }
  inv := { app := fun U => eqToHom (map_id_obj U).symm }

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