restrictedULiftYonedaHomEquiv'_symm_naturality_right

English

The inverse of restrictedULiftYonedaHomEquiv' is compatible with composition.

Русский

Обратное restrictedULiftYonedaHomEquiv' совместимо с композицией.

LaTeX

$$$\big(\mathrm{restrictedULiftYonedaHomEquiv}'\ A\ P\ E \big)^{\, -1} (f \circ g) = \big(\mathrm{restrictedULiftYonedaHomEquiv}'\ A\ Q\ E \big)^{\, -1} g \circ f$$$

Lean4

@[reassoc]
theorem restrictedULiftYonedaHomEquiv'_symm_naturality_right (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)) {E E' : ℰ} (g : E ⟶ E')
    (f : (P ⟶ (restrictedULiftYoneda.{max w v₁} A).obj E)) :
    (restrictedULiftYonedaHomEquiv' A P E').symm (f ≫ (restrictedULiftYoneda A).map g) =
      (restrictedULiftYonedaHomEquiv' A P E).symm f ≫ (Functor.const _).map g :=
  by rfl

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