coreprW — Mathlib

English

The component at X of coreprW applied to a morphism f equals F.map f to coreprx.

Русский

Компонента coreprW на X применена к гомоморфизму f равна F.map f на coreprx.

LaTeX

$$$ F.coreprW.hom.app X f = F.map f F.coreprx $$$

Lean4

/-- An isomorphism between a corepresentable `F` and a functor of the form
`C(F.corepr X, -)`. Note the components `F.coreprW.app X`
definitionally have type `F.corepr_X ⟶ X ≅ F.obj X`.
-/
noncomputable def coreprW (F : C ⥤ Type v₁) [F.IsCorepresentable] : coyoneda.obj (op F.coreprX) ≅ F :=
  F.corepresentableBy.toIso

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