yonedaULiftEquiv_naturality' — Mathlib

English

Variant of YonedaULiftNaturality with prime version; the equality follows from the standard naturativity.

Русский

Вариант натуральности ULift: равенство следует из стандартной натуральности.

LaTeX

$$$F.map\ g (J.yonedaULiftEquiv f) = J.yonedaULiftEquiv (J.yonedaULift.map g.unop ≫ f)$$$

Lean4

/-- Variant of `yonedaEquiv_naturality` with general `g`. This is technically strictly more general
than `yonedaEquiv_naturality`, but `yonedaEquiv_naturality` is sometimes preferable because it
can avoid the "motive is not type correct" error. -/
theorem yonedaULiftEquiv_naturality' {X Y : Cᵒᵖ} {F : Sheaf J (Type (max v v'))} (f : J.yonedaULift.obj (unop X) ⟶ F)
    (g : X ⟶ Y) : F.val.map g (J.yonedaULiftEquiv f) = J.yonedaULiftEquiv (J.yonedaULift.map g.unop ≫ f) :=
  J.yonedaULiftEquiv_naturality _ _

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