mapId_eq — Mathlib

English

Mapping by the identity morphism is the identity functor: Over.map(id_Y) = id_{Over Y}.

Русский

Отображение по тождественному морфизму — тождественный функтор: Over.map(id_Y) = id_{Over Y}.

LaTeX

$$$\\mathrm{Over.map}(\\mathrm{id}_Y) = \\mathrm{id}_{\\mathrm{Over}(Y)}$$$

Lean4

/-- Mapping by the identity morphism is just the identity functor. -/
theorem mapId_eq (Y : T) : map (𝟙 Y) = 𝟭 _ := by
  fapply Functor.ext
  · intro x
    dsimp [Over, Over.map, Comma.mapRight]
    simp only [Category.comp_id]
    exact rfl
  · intro x y u
    dsimp [Over, Over.map, Comma.mapRight]
    simp

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