yonedaULiftEquiv_symm_naturality_right

English

Right-hand symmetry naturality: symmetry on the right with morphism f yields the expected equality.

Русский

Правая симметрия натуральности: правая симметрия с морфизмом f дает ожидаемое равенство.

LaTeX

$$$J.yonedaEquiv.symm x ≫ f = J.yonedaEquiv.symm (f.val.app ⟨X⟩ x)$$$

Lean4

theorem yonedaULiftEquiv_symm_naturality_right (X : C) {F F' : Sheaf J (Type (max v v'))} (f : F ⟶ F')
    (x : F.val.obj ⟨X⟩) : J.yonedaULiftEquiv.symm x ≫ f = J.yonedaULiftEquiv.symm (f.val.app ⟨X⟩ x) :=
  by
  apply J.yonedaULiftEquiv.injective
  simp [yonedaULiftEquiv_comp]

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