map_bijective — Mathlib

English

Let F be fully faithful. Then for any X,Y the map on hom-sets F.map is bijective; it is both injective and surjective.

Русский

Пусть F — полностью верный функтор. Тогда отображение F.map : Hom_C(X,Y) → Hom_D(FX,FY) биективно: оно инъективно и сюръективно.

LaTeX

$$$\forall X,Y:\; \operatorname{Bijective}\big(F.map : (X \to Y) \to (F X \to F Y)\big)$$$

Lean4

theorem map_bijective (X Y : C) : Function.Bijective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
  hF.homEquiv.bijective

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