English
Equivalent restatement: IsIso f iff ∀ c ∈ C, IsIso ((yoneda.map f).app ⟨c⟩).
Русский
Эквивалентное утверждение: IsIso f эквивалентно тому, что для всех объектов c в C IsIso ((yoneda.map f).app ⟨c⟩).
LaTeX
$$IsIso f ↔ ∀ c : C, IsIso ((yoneda.map f).app ⟨c⟩)$$
Lean4
/-- Yoneda's lemma as a bijection `(uliftYoneda.{w}.obj X ⟶ F) ≃ F.obj (op X)`
for any presheaf of type `F : Cᵒᵖ ⥤ Type (max w v₁)` for some
auxiliary universe `w`. -/
@[simps! -isSimp]
def uliftYonedaEquiv {X : C} {F : Cᵒᵖ ⥤ Type (max w v₁)} : (uliftYoneda.{w}.obj X ⟶ F) ≃ F.obj (op X)
where
toFun τ := τ.app (op X) (ULift.up (𝟙 _))
invFun x := { app Y y := F.map y.down.op x }
left_inv
τ := by
ext ⟨Y⟩ ⟨y⟩
simp [uliftYoneda, ← FunctorToTypes.naturality]
right_inv x := by simp
