map_id — Mathlib

English

The functor map with identity morphism is the identity on Subobject X.

Русский

Функтор map с тождественным отображением равен идентичности на Subobject X.

LaTeX

$$$(\mathrm{map}(\mathrm{id}_X)).\mathrm{obj}$ is the identity on $\mathrm{Subobject}(X)$$$

Lean4

theorem map_id (x : Subobject X) : (map (𝟙 X)).obj x = x :=
  by
  induction x using Quotient.inductionOn' with
  | _ f
  exact Quotient.sound ⟨(MonoOver.mapId _).app f⟩

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