uliftYonedaEquiv_symm_map — Mathlib

English

For X,Y in C^op and f: X ⟶ Y, and F, the symm-map formula: uliftYonedaEquiv.{w}.symm (F.map f t) = uliftYoneda.map f.unop ≫ uliftYonedaEquiv.symm t.

Русский

Для X,Y в C^op и f: X ⟶ Y, и F: , выполняется: uliftYonedaEquiv.{w}.symm (F.map f t) = uliftYoneda.map f.unop ≫ uliftYonedaEquiv.symm t.

LaTeX

$$$uliftYonedaEquiv.{w}.symm (F.map f t) = uliftYoneda.map f.unop \gg uliftYonedaEquiv.symm t$$$

Lean4

@[reassoc]
theorem uliftYonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Cᵒᵖ ⥤ Type max w v₁} (t : F.obj X) :
    uliftYonedaEquiv.{w}.symm (F.map f t) = uliftYoneda.map f.unop ≫ uliftYonedaEquiv.symm t :=
  by
  obtain ⟨u, rfl⟩ := uliftYonedaEquiv.surjective t
  rw [uliftYonedaEquiv_naturality]
  simp

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