preimage_id — Mathlib

English

For a fully faithful functor F and any object X, the preimage of the identity on F X is the identity on X.

Русский

Для полностью верного функторa F и любого объекта X предобраз единичного морфизма на F X равен единичному морфизму на X.

LaTeX

$$$\forall X:\; hF.preimage(\mathrm{id}_{F X}) = \mathrm{id}_X$$$

Lean4

@[simp]
theorem preimage_id {X : C} : hF.preimage (𝟙 (F.obj X)) = 𝟙 X :=
  hF.map_injective (by simp)

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