freeYoneda — Mathlib

English

IsSeparator G iff the faithful property holds for the preadditive Yoneda object at G.

Русский

IsSeparator G тогда и только тогда, когда предадитивный Yoneda-объект в G верен.

LaTeX

$$$\mathrm{IsSeparator}(G) \iff (\text{preadditiveYonedaObj } G).\mathrm{Faithful}$$$

Lean4

/-- Given `X : C` and `M : A`, this is the presheaf `Cᵒᵖ ⥤ A` which sends
`Y : Cᵒᵖ` to the coproduct of copies of `M` indexed by `Y.unop ⟶ X`. -/
@[simps]
noncomputable def freeYoneda (X : C) (M : A) : Cᵒᵖ ⥤ A
    where
  obj Y := ∐ (fun (i : (yoneda.obj X).obj Y) ↦ M)
  map f := Sigma.map' ((yoneda.obj X).map f) (fun _ ↦ 𝟙 M)

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