yonedaULiftEquiv_symm_naturality_left

English

Symmetry naturality on the left for ULift: equivalence respects left precomposition with f.

Русский

Симметрия натуральности слева для ULift: эквивариантность сохраняет левое префиксирование.

LaTeX

$$$J.yoneda.map f ≫ J.yonedaULiftEquiv.symm x = J.yonedaULiftEquiv.symm ((F.map f.op) x)$$$

Lean4

theorem yonedaULiftEquiv_symm_naturality_left {X X' : C} (f : X' ⟶ X) (F : Sheaf J (Type (max v v')))
    (x : F.val.obj ⟨X⟩) :
    J.yonedaULift.map f ≫ J.yonedaULiftEquiv.symm x = J.yonedaULiftEquiv.symm ((F.val.map f.op) x) :=
  by
  apply J.yonedaULiftEquiv.injective
  simp only [yonedaULiftEquiv_comp, Equiv.apply_symm_apply]
  rw [yonedaULiftEquiv_yonedaULift_map]
  rfl

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