The Yoneda embedding #
The Yoneda embedding as a functor yoneda : C ⥤ (Cᵒᵖ ⥤ Type v₁),
along with an instance that it is FullyFaithful.
Also the Yoneda lemma, yonedaLemma : (yoneda_pairing C) ≅ (yoneda_evaluation C).
References #
The Yoneda embedding, as a functor from C into presheaves on C.
Equations
- One or more equations did not get rendered due to their size.
The co-Yoneda embedding, as a functor from Cᵒᵖ into co-presheaves on C.
Equations
- One or more equations did not get rendered due to their size.
The Yoneda embedding is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
The Yoneda embedding is full.
The Yoneda embedding is faithful.
Extensionality via Yoneda. The typical usage would be
-- Goal is `X ≅ Y`
apply Yoneda.ext
-- Goals are now functions `(Z ⟶ X) → (Z ⟶ Y)`, `(Z ⟶ Y) → (Z ⟶ X)`, and the fact that these
-- functions are inverses and natural in `Z`.
Equations
- One or more equations did not get rendered due to their size.
If yoneda.map f is an isomorphism, so was f.
The co-Yoneda embedding is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
The morphism X ⟶ Y corresponding to a natural transformation
coyoneda.obj X ⟶ coyoneda.obj Y.
Equations
Extensionality via Coyoneda. The typical usage would be
-- Goal is `X ≅ Y`
apply Coyoneda.ext
-- Goals are now functions `(X ⟶ Z) → (Y ⟶ Z)`, `(Y ⟶ Z) → (X ⟶ Z)`, and the fact that these
-- functions are inverses and natural in `Z`.
Equations
- One or more equations did not get rendered due to their size.
If coyoneda.map f is an isomorphism, so was f.
The identity functor on Type is isomorphic to the coyoneda functor coming from PUnit.
Equations
- One or more equations did not get rendered due to their size.
Taking the unop of morphisms is a natural isomorphism.
Equations
- CategoryTheory.Coyoneda.objOpOp X = CategoryTheory.NatIso.ofComponents (fun (x : Cᵒᵖ) => (CategoryTheory.opEquiv (Opposite.unop (Opposite.op (Opposite.op X))) x).toIso) ⋯
Taking the unop of morphisms is a natural isomorphism.
Equations
- One or more equations did not get rendered due to their size.
The data which expresses that a functor F : Cᵒᵖ ⥤ Type v is representable by Y : C.
the natural bijection
(X ⟶ Y) ≃ F.obj (op X).
If F ≅ F', and F is representable, then F' is representable.
The data which expresses that a functor F : C ⥤ Type v is corepresentable by X : C.
the natural bijection
(X ⟶ Y) ≃ F.obj Y.
If F ≅ F', and F is corepresentable, then F' is corepresentable.
Representing objects are unique up to isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Corepresenting objects are unique up to isomorphism.
Equations
- One or more equations did not get rendered due to their size.
The obvious bijection F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F)
when F : Cᵒᵖ ⥤ Type v₁ and [Category.{v₁} C].
Equations
- One or more equations did not get rendered due to their size.
The isomorphism yoneda.obj Y ≅ F induced by e : F.RepresentableBy Y.
Equations
The obvious bijection F.CorepresentableBy X ≃ (yoneda.obj Y ≅ F)
when F : C ⥤ Type v₁ and [Category.{v₁} C].
Equations
- One or more equations did not get rendered due to their size.
The isomorphism coyoneda.obj (op X) ≅ F induced by e : F.CorepresentableBy X.
Equations
A functor F : Cᵒᵖ ⥤ Type v is representable if there is an object Y with a structure
F.RepresentableBy Y, i.e. there is a natural bijection (X ⟶ Y) ≃ F.obj (op X),
which may also be rephrased as a natural isomorphism yoneda.obj X ≅ F when Category.{v} C.
Alternative constructor for F.IsRepresentable, which takes as an input an
isomorphism yoneda.obj X ≅ F.
A functor F : C ⥤ Type v₁ is corepresentable if there is object X so F ≅ coyoneda.obj X.
Alternative constructor for F.IsCorepresentable, which takes as an input an
isomorphism coyoneda.obj (op X) ≅ F.
The representing object for the representable functor F.
A chosen term in F.RepresentableBy (reprX F) when F.IsRepresentable holds.
Equations
- F.representableBy = ⋯.some
Any representing object for a representable functor F is isomorphic to reprX F.
Equations
The representing element for the representable functor F, sometimes called the universal
element of the functor.
Equations
An isomorphism between a representable F and a functor of the
form C(-, F.reprX). Note the components F.reprW.app X
definitionally have type (X.unop ⟶ F.reprX) ≅ F.obj X.
Equations
- F.reprW = F.representableBy.toIso
The representing object for the corepresentable functor F.
A chosen term in F.CorepresentableBy (coreprX F) when F.IsCorepresentable holds.
Equations
- F.corepresentableBy = ⋯.some
Any corepresenting object for a corepresentable functor F is isomorphic to coreprX F.
Equations
The representing element for the corepresentable functor F, sometimes called the universal
element of the functor.
Equations
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.
Equations
Equations
Equations
We have a type-level equivalence between natural transformations from the yoneda embedding
and elements of F.obj X, without any universe switching.
Equations
- One or more equations did not get rendered due to their size.
See also yonedaEquiv_naturality' for a more general version.
Variant of yonedaEquiv_naturality with general g. This is technically strictly more general
than yonedaEquiv_naturality, but yonedaEquiv_naturality is sometimes preferable because it
can avoid the "motive is not type correct" error.
See also map_yonedaEquiv' for a more general version.
Variant of map_yonedaEquiv with general g. This is technically strictly more general
than map_yonedaEquiv, but map_yonedaEquiv is sometimes preferable because it
can avoid the "motive is not type correct" error.
Two morphisms of presheaves of types P ⟶ Q coincide if the precompositions
with morphisms yoneda.obj X ⟶ P agree.
The "Yoneda evaluation" functor, which sends X : Cᵒᵖ and F : Cᵒᵖ ⥤ Type
to F.obj X, functorially in both X and F.
The "Yoneda pairing" functor, which sends X : Cᵒᵖ and F : Cᵒᵖ ⥤ Type
to yoneda.op.obj X ⟶ F, functorially in both X and F.
Equations
- One or more equations did not get rendered due to their size.
A bijection (yoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (op X) which is a variant
of yonedaEquiv with heterogeneous universes.
Equations
- One or more equations did not get rendered due to their size.
The Yoneda lemma asserts that the Yoneda pairing
(X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F)
is naturally isomorphic to the evaluation (X, F) ↦ F.obj X.
Equations
- One or more equations did not get rendered due to their size.
The curried version of yoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
The curried version of the Yoneda lemma.
Equations
- One or more equations did not get rendered due to their size.
Version of the Yoneda lemma where the presheaf is fixed but the argument varies.
Equations
- One or more equations did not get rendered due to their size.
The curried version of yoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
We have a type-level equivalence between natural transformations from the coyoneda embedding
and elements of F.obj X.unop, without any universe switching.
Equations
- One or more equations did not get rendered due to their size.
The "Coyoneda evaluation" functor, which sends X : C and F : C ⥤ Type
to F.obj X, functorially in both X and F.
The "Coyoneda pairing" functor, which sends X : C and F : C ⥤ Type
to coyoneda.rightOp.obj X ⟶ F, functorially in both X and F.
Equations
- One or more equations did not get rendered due to their size.
A bijection (coyoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (unop X) which is a variant
of coyonedaEquiv with heterogeneous universes.
Equations
- One or more equations did not get rendered due to their size.
The Coyoneda lemma asserts that the Coyoneda pairing
(X : C, F : C ⥤ Type) ↦ (coyoneda.obj X ⟶ F)
is naturally isomorphic to the evaluation (X, F) ↦ F.obj X.
Equations
- CategoryTheory.coyonedaLemma C = CategoryTheory.NatIso.ofComponents (fun (x : C × CategoryTheory.Functor C (Type ?u.20)) => (CategoryTheory.coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯
The curried version of coyoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
The curried version of the Coyoneda lemma.
Equations
- One or more equations did not get rendered due to their size.
Version of the Coyoneda lemma where the presheaf is fixed but the argument varies.
Equations
- One or more equations did not get rendered due to their size.
The curried version of coyoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
The natural transformation yoneda.obj X ⟶ F.op ⋙ yoneda.obj (F.obj X)
when F : C ⥤ D and X : C.
Equations
- CategoryTheory.yonedaMap F X = { app := fun (x : Cᵒᵖ) (f : (CategoryTheory.yoneda.obj X).obj x) => F.map f, naturality := ⋯ }
A type-level equivalence between sections of a functor and morphisms from a terminal functor to it. We use the constant functor on a given singleton type here as a specific choice of terminal functor.
Equations
- One or more equations did not get rendered due to their size.
A natural isomorphism between the sections functor (C ⥤ Type _) ⥤ Type _ and the co-Yoneda
embedding of a terminal functor, specifically a constant functor on a given singleton type X.
Equations
- CategoryTheory.sectionsFunctorNatIsoCoyoneda X = CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor C (Type (max ?u.35 ?u.34))) => (F.sectionsEquivHom X).toIso) ⋯
FullyFaithful.homEquiv as a natural isomorphism.
Equations
- hF.homNatIso X = CategoryTheory.NatIso.ofComponents (fun (Y : Cᵒᵖ) => (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso) ⋯
FullyFaithful.homEquiv as a natural isomorphism.
Equations
- hF.homNatIsoMaxRight X = CategoryTheory.NatIso.ofComponents (fun (Y : Cᵒᵖ) => (hF.homEquiv.symm.trans Equiv.ulift.symm).toIso) ⋯
FullyFaithful.homEquiv as a natural isomorphism.
Equations
- hF.compYonedaCompWhiskeringLeft = CategoryTheory.NatIso.ofComponents (fun (X : C) => hF.homNatIso X) ⋯
FullyFaithful.homEquiv as a natural isomorphism.
Equations
- hF.compYonedaCompWhiskeringLeftMaxRight = CategoryTheory.NatIso.ofComponents (fun (X : C) => hF.homNatIsoMaxRight X) ⋯