restrictedULiftYonedaHomEquiv' — Mathlib

English

The above equivalence extends to a canonical restricted ULift Yoneda equivalence for all E.

Русский

Указанная эквивалентность распространяется на каноническое restricted ULift Yoneda эквивалентность для всех E.

LaTeX

$$$\text{restrictedULiftYonedaHomEquiv}\ A\ P\ E : (L.obj P \to E) \simeq (P \to ( restrictedULiftYoneda A).obj E)$$$

Lean4

/-- Auxiliary definition for `restrictedULiftYonedaHomEquiv`. -/
def restrictedULiftYonedaHomEquiv' (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)) (E : ℰ) :
    (CostructuredArrow.proj uliftYoneda.{max w v₂} P ⋙ A ⟶
        (Functor.const (CostructuredArrow uliftYoneda.{max w v₂} P)).obj E) ≃
      (P ⟶ (restrictedULiftYoneda.{max w v₁} A).obj E)
    where
  toFun
    f :=
    { app _ x := ULift.up (f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)))
      naturality _ _
        g := by
        ext x
        let φ :
          CostructuredArrow.mk (uliftYonedaEquiv.{max w v₂}.symm (P.map g x)) ⟶
            CostructuredArrow.mk (uliftYonedaEquiv.symm x) :=
          CostructuredArrow.homMk g.unop
            (by
              dsimp
              rw [uliftYonedaEquiv_symm_map])
        dsimp
        congr 1
        simpa using (f.naturality φ).symm }
  invFun
    g :=
    { app y := (uliftYonedaEquiv.{max w v₂} (y.hom ≫ g)).down
      naturality y y'
        f := by
        dsimp
        rw [comp_id, ← CostructuredArrow.w f, assoc, map_comp_uliftYonedaEquiv_down] }
  left_inv
    f := by
    ext X
    let e : CostructuredArrow.mk (uliftYonedaEquiv.{max w v₂}.symm (X.hom.app (op X.left) ⟨𝟙 X.left⟩)) ≅ X :=
      CostructuredArrow.isoMk (Iso.refl _)
        (by
          ext Y x
          dsimp
          rw [← FunctorToTypes.naturality]
          congr)
    simpa [e] using f.naturality e.inv
  right_inv
    g := by
    ext X x
    apply ULift.down_injective
    simp [uliftYonedaEquiv]

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