yonedaULiftEquiv_comp — Mathlib

English

Naturality of yonedaULift with composition; equality expresses compatibility with composition of maps.

Русский

Натуральность YonedaULift по композиции; равенство выражает совместимость с композицией отображений.

LaTeX

$$$J.yonedaULiftEquiv (\alpha \ggg \beta) = \beta.\val.app\ _ (J.yonedaULiftEquiv\alpha)$$$

Lean4

theorem yonedaULiftEquiv_comp {X : C} {F G : Sheaf J (Type (max v v'))} (α : J.yonedaULift.obj X ⟶ F) (β : F ⟶ G) :
    J.yonedaULiftEquiv (α ≫ β) = β.val.app _ (J.yonedaULiftEquiv α) :=
  rfl

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