yonedaULiftEquiv_naturality — Mathlib

English

Natural transformation in yonedaULift: F.map g.op (yonedaULiftEquiv f) = yonedaULiftEquiv (yonedaULift.map g ≫ f).

Русский

Натуральность перехода через yonedaULift: F.map g.op (yonedaULiftEquiv f) = yonedaULiftEquiv (yonedaULift.map g ≫ f).

LaTeX

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

Lean4

/-- See also `yonedaEquiv_naturality'` for a more general version. -/
theorem yonedaULiftEquiv_naturality {X Y : C} {F : Sheaf J (Type (max v v'))} (f : J.yonedaULift.obj X ⟶ F)
    (g : Y ⟶ X) : F.val.map g.op (J.yonedaULiftEquiv f) = J.yonedaULiftEquiv (J.yonedaULift.map g ≫ f) :=
  by
  change (f.val.app (op X) ≫ F.val.map g.op) ⟨𝟙 X⟩ = f.val.app (op Y) ⟨𝟙 Y ≫ g⟩
  rw [← f.val.naturality]
  simp [yonedaULift]

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