restrictedULiftYonedaHomEquiv — Mathlib

English

Symmetry of the restricted ULift Yoneda equivalence for all P, E.

Русский

Симметрия эквивалентности restricted ULift Yoneda для всех P, E.

LaTeX

$$$\text{restrictedULiftYonedaHomEquiv}'\ A\ P\ E \;\text{symm}$$$

Lean4

/-- Auxiliary definition for `uliftYonedaAdjunction`. -/
noncomputable def restrictedULiftYonedaHomEquiv (P : Cᵒᵖ ⥤ Type max w v₁ v₂) (E : ℰ) :
    (L.obj P ⟶ E) ≃ (P ⟶ (restrictedULiftYoneda.{max w v₁} A).obj E) :=
  (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension _ α P).homEquiv.trans (restrictedULiftYonedaHomEquiv' A P E)

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