uliftYonedaAdjunction_unit_app_app

English

The unit component of the Yoneda adjunction is computed by a standard formula.

Русский

Единичный компонент адъекции Янеда вычисляется по стандартной формуле.

LaTeX

$$$((\mathrm{uliftYonedaAdjunction} \ L \ \alpha).\mathrm{unit}.\mathrm{app} P).\mathrm{app} Z\; z = \mathrm{ULift.up}(\alpha.app Z.unop \circ L.map (\mathrm{uliftYonedaEquiv}.symm z))$$$

Lean4

@[simp]
theorem uliftYonedaAdjunction_unit_app_app (P : Cᵒᵖ ⥤ Type max w v₁ v₂) {Z : Cᵒᵖ} (z : P.obj Z) :
    ((uliftYonedaAdjunction.{w} L α).unit.app P).app Z z = ULift.up (α.app Z.unop ≫ L.map (uliftYonedaEquiv.symm z)) :=
  by
  have h₁ := (uliftYonedaAdjunction.{w} L α).homEquiv_unit P _ (𝟙 _)
  simp only [Functor.comp_obj, Functor.map_id, comp_id] at h₁
  simp [← h₁]

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