pushforwardCompCoyonedaFreeYonedaCorepresentableBy

English

For any X, the pullback object constructed via the free yoneda corepresentable is well defined.

Русский

Для любого X конструкция пуллбек объекта через свободную yoneda корректна и определена.

LaTeX

$$$\\text{pullbackObjIsDefined }(\\varphi, (\\mathrm{free} S).\\mathrm{obj}(\\mathrm{yoneda}.\\mathrm{obj} X))$$$

Lean4

/-- Given a morphism of presheaves of rings `φ : S ⟶ F.op ⋙ R`, where `F : C ⥤ D`,
`S : Cᵒᵖ ⥤ RingCat`, `R : Dᵒᵖ ⥤ RingCat` and `X : C`, the (partial) left adjoint
functor of `pushforward φ` is defined on the object `(free S).obj (yoneda.obj X)`:
this object shall be mapped to `(free R).obj (yoneda.obj (F.obj X))`. -/
noncomputable def pushforwardCompCoyonedaFreeYonedaCorepresentableBy (X : C) :
    (pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).CorepresentableBy
      ((free R).obj (yoneda.obj (F.obj X)))
    where
  homEquiv {M} := (freeYonedaEquiv).trans (freeYonedaEquiv (M := (pushforward φ).obj M)).symm
  homEquiv_comp {M N} g
    f :=
    freeYonedaEquiv.injective
      (by
        dsimp
        erw [Equiv.apply_symm_apply, freeYonedaEquiv_comp]
        conv_rhs => erw [freeYonedaEquiv_comp]
        erw [Equiv.apply_symm_apply]
        rfl)

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