map_yonedaULiftEquiv' — Mathlib

English

Left naturality of symm for ULift equivalence: the equality holds by injectivity and prior lemmas.

Русский

Левая натуральность симм для эквивалентности ULift: равенство следует из инъективности и предыдущих лемм.

LaTeX

$$$J.yonedaULiftEquiv.map f \;\; \gg = \cdot$$$

Lean4

/-- Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
can avoid the "motive is not type correct" error. -/
theorem map_yonedaULiftEquiv' {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) = f.val.app Y ⟨g.unop⟩ := by
  rw [yonedaULiftEquiv_naturality', yonedaULiftEquiv_comp, yonedaULiftEquiv_yonedaULift_map]

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