English
Let X be an object in the forgetful enrichment category ForgetEnrichment W C. The underlying hom to W of the identity on X coincides with the enriched identity on the underlying C-object ForgetEnrichment.to W X.
Русский
Пусть X является объектом в обогащённой по забыванию категории ForgetEnrichment W C. Соответствующая забытию гомома в W от тождества на X равна обогащённому тождественному морфизму на основе X в C: homTo_W(id_X) = eId_W(ForgetEnrichment.to_W X).
LaTeX
$$$\\mathrm{homTo}_W(\\mathbf{1}_X) = eId_W(\\mathrm{ForgetEnrichment.to_W}X)$$$
Lean4
/-- The identity in the "underlying" category of an enriched category. -/
@[simp]
theorem homTo_id (X : ForgetEnrichment W C) : ForgetEnrichment.homTo W (𝟙 X) = eId W (ForgetEnrichment.to W X : C) :=
Category.id_comp _
