map_comp_uliftYonedaEquiv_down — Mathlib

English

There exists a natural equivalence relating restricted ULift Yoneda data to presheaf morphisms.

Русский

Существует естественное эквивалентность, связывающая данные restricted ULift Yoneda и морфизмы прешефа.

LaTeX

$$$\text{restrictedULiftYonedaHomEquiv}'\ A\ P\ E : (P^{\mathrm{op}} \to \mathrm{Type}) \\to (P \to (\mathrm{restrictedULiftYoneda}\;A).\mathrm{obj} E)$$$

Lean4

@[reassoc]
theorem map_comp_uliftYonedaEquiv_down (E : ℰ) {X Y : C} (f : X ⟶ Y)
    (g : uliftYoneda.{max w v₂}.obj Y ⟶ (restrictedULiftYoneda.{max w v₁} A).obj E) :
    A.map f ≫ (uliftYonedaEquiv g).down = (uliftYonedaEquiv (uliftYoneda.map f ≫ g)).down :=
  by
  have this := congr_fun (g.naturality f.op) (ULift.up (𝟙 Y))
  dsimp [uliftYonedaEquiv, uliftYoneda] at this ⊢
  simp only [comp_id] at this
  simp [id_comp, this]

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