uliftYonedaEquiv_uliftYoneda_map — Mathlib

English

For any f: X ⟶ Y, uliftYonedaEquiv (uliftYoneda.map f) corresponds to the map sending X to f; i.e., Equiv toFunLike uses down/case: uliftYonedaEquiv maps uliftYoneda.map f to the corresponding ULift value f.

Русский

Для любого f: X ⟶ Y, uliftYonedaEquiv (uliftYoneda.map f) соответствует отображению X к f; т.е. отображение Equiv toFunLike задаёт значение с коэффициентом f.

LaTeX

$$$\mathrm{uliftYonedaEquiv} (\mathrm{uliftYoneda.map} f) = f$$$

Lean4

@[simp]
theorem uliftYonedaEquiv_uliftYoneda_map {X Y : C} (f : X ⟶ Y) :
    DFunLike.coe (β := fun _ ↦ ULift.{w} (X ⟶ Y)) uliftYonedaEquiv.{w} (uliftYoneda.map f) = ULift.up f := by
  simp [uliftYonedaEquiv, uliftYoneda]

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