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 #
@[simp]
theorem
CategoryTheory.yoneda_obj_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
(Y : Cᵒᵖ)
:
(CategoryTheory.yoneda.obj X).obj Y = (Opposite.unop Y ⟶ X)
@[simp]
theorem
CategoryTheory.yoneda_map_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
∀ {X Y : C} (f : X ⟶ Y) (x : Cᵒᵖ)
(g :
((fun (X : C) =>
{ obj := fun (Y : Cᵒᵖ) => Opposite.unop Y ⟶ X,
map := fun {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y) (g : (fun (Y : Cᵒᵖ) => Opposite.unop Y ⟶ X) X_1) =>
CategoryTheory.CategoryStruct.comp f.unop g,
map_id := ⋯, map_comp := ⋯ })
X).obj
x),
(CategoryTheory.yoneda.map f).app x g = CategoryTheory.CategoryStruct.comp g f
@[simp]
theorem
CategoryTheory.yoneda_obj_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
:
∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y) (g : Opposite.unop X_1 ⟶ X),
(CategoryTheory.yoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp f.unop g
The Yoneda embedding, as a functor from C into presheaves on C.
See https://stacks.math.columbia.edu/tag/001O.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.coyoneda_obj_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : Cᵒᵖ)
(Y : C)
:
(CategoryTheory.coyoneda.obj X).obj Y = (Opposite.unop X ⟶ Y)
@[simp]
theorem
CategoryTheory.coyoneda_map_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : C)
(g :
((fun (X : Cᵒᵖ) =>
{ obj := fun (Y : C) => Opposite.unop X ⟶ Y,
map := fun {X_1 Y : C} (f : X_1 ⟶ Y) (g : (fun (Y : C) => Opposite.unop X ⟶ Y) X_1) =>
CategoryTheory.CategoryStruct.comp g f,
map_id := ⋯, map_comp := ⋯ })
X).obj
x),
(CategoryTheory.coyoneda.map f).app x g = CategoryTheory.CategoryStruct.comp f.unop g
@[simp]
theorem
CategoryTheory.coyoneda_obj_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : Cᵒᵖ)
:
∀ {X_1 Y : C} (f : X_1 ⟶ Y) (g : Opposite.unop X ⟶ X_1),
(CategoryTheory.coyoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp g f
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.
theorem
CategoryTheory.Yoneda.obj_map_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : Opposite.op X ⟶ Opposite.op Y)
:
(CategoryTheory.yoneda.obj X).map f (CategoryTheory.CategoryStruct.id X) = (CategoryTheory.yoneda.map f.unop).app (Opposite.op Y) (CategoryTheory.CategoryStruct.id Y)
@[simp]
theorem
CategoryTheory.Yoneda.naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(α : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y)
{Z : C}
{Z' : C}
(f : Z ⟶ Z')
(h : Z' ⟶ X)
:
CategoryTheory.CategoryStruct.comp f (α.app (Opposite.op Z') h) = α.app (Opposite.op Z) (CategoryTheory.CategoryStruct.comp f h)
def
CategoryTheory.Yoneda.fullyFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.yoneda.FullyFaithful
The Yoneda embedding is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Yoneda.fullyFaithful_preimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y)
:
CategoryTheory.Yoneda.fullyFaithful.preimage f = f.app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)
instance
CategoryTheory.Yoneda.yoneda_full
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.yoneda.Full
The Yoneda embedding is full.
See https://stacks.math.columbia.edu/tag/001P.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Yoneda.yoneda_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.yoneda.Faithful
The Yoneda embedding is faithful.
See https://stacks.math.columbia.edu/tag/001P.
Equations
- ⋯ = ⋯
def
CategoryTheory.Yoneda.ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
(Y : C)
(p : {Z : C} → (Z ⟶ X) → (Z ⟶ Y))
(q : {Z : C} → (Z ⟶ Y) → (Z ⟶ X))
(h₁ : ∀ {Z : C} (f : Z ⟶ X), q (p f) = f)
(h₂ : ∀ {Z : C} (f : Z ⟶ Y), p (q f) = f)
(n : ∀ {Z Z' : C} (f : Z' ⟶ Z) (g : Z ⟶ X),
p (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f (p g))
:
X ≅ Y
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.
theorem
CategoryTheory.Yoneda.isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsIso (CategoryTheory.yoneda.map f)]
:
If yoneda.map f is an isomorphism, so was f.
@[simp]
theorem
CategoryTheory.Coyoneda.naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(α : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y)
{Z : C}
{Z' : C}
(f : Z' ⟶ Z)
(h : Opposite.unop X ⟶ Z')
:
CategoryTheory.CategoryStruct.comp (α.app Z' h) f = α.app Z (CategoryTheory.CategoryStruct.comp h f)
def
CategoryTheory.Coyoneda.fullyFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.coyoneda.FullyFaithful
The co-Yoneda embedding is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Coyoneda.fullyFaithful_preimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(f : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y)
:
CategoryTheory.Coyoneda.fullyFaithful.preimage f = Quiver.Hom.op (f.app (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X)))
def
CategoryTheory.Coyoneda.preimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(f : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y)
:
X ⟶ Y
The morphism X ⟶ Y corresponding to a natural transformation
coyoneda.obj X ⟶ coyoneda.obj Y.
Equations
instance
CategoryTheory.Coyoneda.coyoneda_full
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.coyoneda.Full
Equations
- ⋯ = ⋯
instance
CategoryTheory.Coyoneda.coyoneda_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.coyoneda.Faithful
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Coyoneda.isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(f : X ⟶ Y)
[CategoryTheory.IsIso (CategoryTheory.coyoneda.map f)]
:
If coyoneda.map f is an isomorphism, so was f.
def
CategoryTheory.Coyoneda.punitIso :
CategoryTheory.coyoneda.obj (Opposite.op PUnit.{v₁ + 1} ) ≅ CategoryTheory.Functor.id (Type v₁)
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.
@[simp]
theorem
CategoryTheory.Coyoneda.objOpOp_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
(X : Cᵒᵖ)
:
∀ (a : (CategoryTheory.yoneda.obj X✝).obj X),
(CategoryTheory.Coyoneda.objOpOp X✝).inv.app X a = (CategoryTheory.opEquiv (Opposite.op X✝) X).symm a
@[simp]
theorem
CategoryTheory.Coyoneda.objOpOp_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
(X : Cᵒᵖ)
:
∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X✝))).obj X),
(CategoryTheory.Coyoneda.objOpOp X✝).hom.app X a = (CategoryTheory.opEquiv (Opposite.op X✝) X) a
def
CategoryTheory.Coyoneda.objOpOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
:
CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X)) ≅ CategoryTheory.yoneda.obj X
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) ⋯
structure
CategoryTheory.Functor.RepresentableBy
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(Y : C)
:
Type (max (max u₁ v) v₁)
The data which expresses that a functor F : Cᵒᵖ ⥤ Type v is representable by Y : C.
- homEquiv : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X)
the natural bijection
(X ⟶ Y) ≃ F.obj (op X). - homEquiv_comp : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = F.map f.op (self.homEquiv g)
theorem
CategoryTheory.Functor.RepresentableBy.homEquiv_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v)}
{Y : C}
(self : F.RepresentableBy Y)
{X : C}
{X' : C}
(f : X ⟶ X')
(g : X' ⟶ Y)
:
self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = F.map f.op (self.homEquiv g)
def
CategoryTheory.Functor.RepresentableBy.ofIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v)}
{F' : CategoryTheory.Functor Cᵒᵖ (Type v)}
{Y : C}
(e : F.RepresentableBy Y)
(e' : F ≅ F')
:
F'.RepresentableBy Y
If F ≅ F', and F is representable, then F' is representable.
Equations
- e.ofIso e' = { homEquiv := fun {X : C} => e.homEquiv.trans (e'.app (Opposite.op X)).toEquiv, homEquiv_comp := ⋯ }
structure
CategoryTheory.Functor.CorepresentableBy
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v))
(X : C)
:
Type (max (max u₁ v) v₁)
The data which expresses that a functor F : C ⥤ Type v is corepresentable by X : C.
the natural bijection
(X ⟶ Y) ≃ F.obj Y.- homEquiv_comp : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = F.map g (self.homEquiv f)
theorem
CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v)}
{X : C}
(self : F.CorepresentableBy X)
{Y : C}
{Y' : C}
(g : Y ⟶ Y')
(f : X ⟶ Y)
:
self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = F.map g (self.homEquiv f)
def
CategoryTheory.Functor.CorepresentableBy.ofIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v)}
{F' : CategoryTheory.Functor C (Type v)}
{X : C}
(e : F.CorepresentableBy X)
(e' : F ≅ F')
:
F'.CorepresentableBy X
If F ≅ F', and F is corepresentable, then F' is corepresentable.
Equations
- e.ofIso e' = { homEquiv := fun {X_1 : C} => e.homEquiv.trans (e'.app X_1).toEquiv, homEquiv_comp := ⋯ }
theorem
CategoryTheory.Functor.RepresentableBy.homEquiv_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v)}
{Y : C}
(e : F.RepresentableBy Y)
{X : C}
(f : X ⟶ Y)
:
e.homEquiv f = F.map f.op (e.homEquiv (CategoryTheory.CategoryStruct.id Y))
theorem
CategoryTheory.Functor.CorepresentableBy.homEquiv_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v)}
{X : C}
(e : F.CorepresentableBy X)
{Y : C}
(f : X ⟶ Y)
:
e.homEquiv f = F.map f (e.homEquiv (CategoryTheory.CategoryStruct.id X))
theorem
CategoryTheory.Functor.RepresentableBy.ext_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v)}
{Y : C}
{e : F.RepresentableBy Y}
{e' : F.RepresentableBy Y}
:
e = e' ↔ e.homEquiv (CategoryTheory.CategoryStruct.id Y) = e'.homEquiv (CategoryTheory.CategoryStruct.id Y)
theorem
CategoryTheory.Functor.RepresentableBy.ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v)}
{Y : C}
{e : F.RepresentableBy Y}
{e' : F.RepresentableBy Y}
(h : e.homEquiv (CategoryTheory.CategoryStruct.id Y) = e'.homEquiv (CategoryTheory.CategoryStruct.id Y))
:
e = e'
theorem
CategoryTheory.Functor.CorepresentableBy.ext_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v)}
{X : C}
{e : F.CorepresentableBy X}
{e' : F.CorepresentableBy X}
:
e = e' ↔ e.homEquiv (CategoryTheory.CategoryStruct.id X) = e'.homEquiv (CategoryTheory.CategoryStruct.id X)
theorem
CategoryTheory.Functor.CorepresentableBy.ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v)}
{X : C}
{e : F.CorepresentableBy X}
{e' : F.CorepresentableBy X}
(h : e.homEquiv (CategoryTheory.CategoryStruct.id X) = e'.homEquiv (CategoryTheory.CategoryStruct.id X))
:
e = e'
def
CategoryTheory.Functor.representableByEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{Y : C}
:
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.
def
CategoryTheory.Functor.RepresentableBy.toIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{Y : C}
(e : F.RepresentableBy Y)
:
CategoryTheory.yoneda.obj Y ≅ F
The isomorphism yoneda.obj Y ≅ F induced by e : F.RepresentableBy Y.
Equations
- e.toIso = CategoryTheory.Functor.representableByEquiv e
def
CategoryTheory.Functor.corepresentableByEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v₁)}
{X : C}
:
F.CorepresentableBy X ≃ (CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F)
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.
def
CategoryTheory.Functor.CorepresentableBy.toIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v₁)}
{X : C}
(e : F.CorepresentableBy X)
:
CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F
The isomorphism coyoneda.obj (op X) ≅ F induced by e : F.CorepresentableBy X.
Equations
- e.toIso = CategoryTheory.Functor.corepresentableByEquiv e
class
CategoryTheory.Functor.IsRepresentable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
A functor F : Cᵒᵖ ⥤ Type v is representable if there is oan bject 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.
See https://stacks.math.columbia.edu/tag/001Q.
- has_representation : ∃ (Y : C), Nonempty (F.RepresentableBy Y)
Instances
theorem
CategoryTheory.Functor.IsRepresentable.has_representation
{C : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} [self : F.IsRepresentable],
∃ (Y : C), Nonempty (F.RepresentableBy Y)
@[deprecated CategoryTheory.Functor.IsRepresentable]
def
CategoryTheory.Functor.Representable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
Alias of CategoryTheory.Functor.IsRepresentable.
A functor F : Cᵒᵖ ⥤ Type v is representable if there is oan bject 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.
theorem
CategoryTheory.Functor.RepresentableBy.isRepresentable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v)}
{Y : C}
(e : F.RepresentableBy Y)
:
F.IsRepresentable
theorem
CategoryTheory.Functor.IsRepresentable.mk'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{X : C}
(e : CategoryTheory.yoneda.obj X ≅ F)
:
F.IsRepresentable
Alternative constructure for F.IsRepresentable, which takes as an input an
isomorphism yoneda.obj X ≅ F.
instance
CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
(CategoryTheory.yoneda.obj X).IsRepresentable
Equations
- ⋯ = ⋯
class
CategoryTheory.Functor.IsCorepresentable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v))
:
A functor F : C ⥤ Type v₁ is corepresentable if there is object X so F ≅ coyoneda.obj X.
See https://stacks.math.columbia.edu/tag/001Q.
- has_corepresentation : ∃ (X : C), Nonempty (F.CorepresentableBy X)
Instances
theorem
CategoryTheory.Functor.IsCorepresentable.has_corepresentation
{C : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {F : CategoryTheory.Functor C (Type v)} [self : F.IsCorepresentable],
∃ (X : C), Nonempty (F.CorepresentableBy X)
@[deprecated CategoryTheory.Functor.IsCorepresentable]
def
CategoryTheory.Functor.Corepresentable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v))
:
Alias of CategoryTheory.Functor.IsCorepresentable.
A functor F : C ⥤ Type v₁ is corepresentable if there is object X so F ≅ coyoneda.obj X.
theorem
CategoryTheory.Functor.CorepresentableBy.isCorepresentable
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v)}
{X : C}
(e : F.CorepresentableBy X)
:
F.IsCorepresentable
theorem
CategoryTheory.Functor.IsCorepresentable.mk'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{F : CategoryTheory.Functor C (Type v₁)}
{X : C}
(e : CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F)
:
F.IsCorepresentable
Alternative constructure for F.IsCorepresentable, which takes as an input an
isomorphism coyoneda.obj (op X) ≅ F.
instance
CategoryTheory.Functor.instIsCorepresentableObjOppositeTypeCoyoneda
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ}
:
(CategoryTheory.coyoneda.obj X).IsCorepresentable
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.Functor.reprX
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
[hF : F.IsRepresentable]
:
C
The representing object for the representable functor F.
Equations
- F.reprX = ⋯.choose
noncomputable def
CategoryTheory.Functor.representableBy
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
[hF : F.IsRepresentable]
:
F.RepresentableBy F.reprX
A chosen term in F.RepresentableBy (reprX F) when F.IsRepresentable holds.
Equations
- F.representableBy = ⋯.some
noncomputable def
CategoryTheory.Functor.reprx
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
[hF : F.IsRepresentable]
:
F.obj (Opposite.op F.reprX)
The representing element for the representable functor F, sometimes called the universal
element of the functor.
Equations
- F.reprx = F.representableBy.homEquiv (CategoryTheory.CategoryStruct.id F.reprX)
noncomputable def
CategoryTheory.Functor.reprW
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v₁))
[F.IsRepresentable]
:
CategoryTheory.yoneda.obj F.reprX ≅ F
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
theorem
CategoryTheory.Functor.reprW_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v₁))
[F.IsRepresentable]
(X : Cᵒᵖ)
(f : Opposite.unop X ⟶ F.reprX)
:
F.reprW.hom.app X f = F.map f.op F.reprx
noncomputable def
CategoryTheory.Functor.coreprX
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v))
[hF : F.IsCorepresentable]
:
C
The representing object for the corepresentable functor F.
Equations
- F.coreprX = ⋯.choose
noncomputable def
CategoryTheory.Functor.corepresentableBy
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v))
[hF : F.IsCorepresentable]
:
F.CorepresentableBy F.coreprX
A chosen term in F.CorepresentableBy (coreprX F) when F.IsCorepresentable holds.
Equations
- F.corepresentableBy = ⋯.some
noncomputable def
CategoryTheory.Functor.coreprx
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v))
[hF : F.IsCorepresentable]
:
F.obj F.coreprX
The representing element for the corepresentable functor F, sometimes called the universal
element of the functor.
Equations
- F.coreprx = F.corepresentableBy.homEquiv (CategoryTheory.CategoryStruct.id F.coreprX)
noncomputable def
CategoryTheory.Functor.coreprW
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v₁))
[F.IsCorepresentable]
:
CategoryTheory.coyoneda.obj (Opposite.op F.coreprX) ≅ F
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
- F.coreprW = F.corepresentableBy.toIso
theorem
CategoryTheory.Functor.coreprW_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v₁))
[F.IsCorepresentable]
(X : C)
(f : F.coreprX ⟶ X)
:
F.coreprW.hom.app X f = F.map f F.coreprx
theorem
CategoryTheory.isRepresentable_of_natIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v₁))
{G : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(i : F ≅ G)
[F.IsRepresentable]
:
G.IsRepresentable
theorem
CategoryTheory.corepresentable_of_natIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type v₁))
{G : CategoryTheory.Functor C (Type v₁)}
(i : F ≅ G)
[F.IsCorepresentable]
:
G.IsCorepresentable
instance
CategoryTheory.instIsCorepresentableIdType :
(CategoryTheory.Functor.id (Type v₁)).IsCorepresentable
Equations
Equations
Equations
def
CategoryTheory.yonedaEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
:
(CategoryTheory.yoneda.obj X ⟶ F) ≃ F.obj (Opposite.op X)
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.
theorem
CategoryTheory.yonedaEquiv_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(f : CategoryTheory.yoneda.obj X ⟶ F)
:
CategoryTheory.yonedaEquiv f = f.app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)
@[simp]
theorem
CategoryTheory.yonedaEquiv_symm_app_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(x : F.obj (Opposite.op X))
(Y : Cᵒᵖ)
(f : Opposite.unop Y ⟶ X)
:
(CategoryTheory.yonedaEquiv.symm x).app Y f = F.map f.op x
theorem
CategoryTheory.yonedaEquiv_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(f : CategoryTheory.yoneda.obj X ⟶ F)
(g : Y ⟶ X)
:
F.map g.op (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) f)
See also yonedaEquiv_naturality' for a more general version.
theorem
CategoryTheory.yonedaEquiv_naturality'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F)
(g : X ⟶ Y)
:
F.map g (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g.unop) f)
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.
theorem
CategoryTheory.yonedaEquiv_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{G : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(α : CategoryTheory.yoneda.obj X ⟶ F)
(β : F ⟶ G)
:
CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app (Opposite.op X) (CategoryTheory.yonedaEquiv α)
theorem
CategoryTheory.yonedaEquiv_yoneda_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.yonedaEquiv (CategoryTheory.yoneda.map f) = f
theorem
CategoryTheory.map_yonedaEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(f : CategoryTheory.yoneda.obj X ⟶ F)
(g : Y ⟶ X)
:
F.map g.op (CategoryTheory.yonedaEquiv f) = f.app (Opposite.op Y) g
See also map_yonedaEquiv' for a more general version.
theorem
CategoryTheory.map_yonedaEquiv'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F)
(g : X ⟶ Y)
:
F.map g (CategoryTheory.yonedaEquiv f) = f.app Y g.unop
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.
theorem
CategoryTheory.yonedaEquiv_symm_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(f : X ⟶ Y)
{F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
(t : F.obj X)
:
CategoryTheory.yonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f.unop) (CategoryTheory.yonedaEquiv.symm t)
theorem
CategoryTheory.hom_ext_yoneda
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{f : P ⟶ Q}
{g : P ⟶ Q}
(h : ∀ (X : C) (p : CategoryTheory.yoneda.obj X ⟶ P),
CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g)
:
f = g
Two morphisms of presheaves of types P ⟶ Q coincide if the precompositions
with morphisms yoneda.obj X ⟶ P agree.
def
CategoryTheory.yonedaEvaluation
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type (max u₁ v₁))
The "Yoneda evaluation" functor, which sends X : Cᵒᵖ and F : Cᵒᵖ ⥤ Type
to F.obj X, functorially in both X and F.
Equations
@[simp]
theorem
CategoryTheory.yonedaEvaluation_map_down
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(P : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))
(Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))
(α : P ⟶ Q)
(x : (CategoryTheory.yonedaEvaluation C).obj P)
:
((CategoryTheory.yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
def
CategoryTheory.yonedaPairing
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type (max u₁ v₁))
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.
theorem
CategoryTheory.yonedaPairingExt_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{x : (CategoryTheory.yonedaPairing C).obj X}
{y : (CategoryTheory.yonedaPairing C).obj X}
:
theorem
CategoryTheory.yonedaPairingExt
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
{X : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)}
{x : (CategoryTheory.yonedaPairing C).obj X}
{y : (CategoryTheory.yonedaPairing C).obj X}
(w : ∀ (Y : Cᵒᵖ), x.app Y = y.app Y)
:
x = y
@[simp]
theorem
CategoryTheory.yonedaPairing_map
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(P : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))
(Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))
(α : P ⟶ Q)
(β : (CategoryTheory.yonedaPairing C).obj P)
:
(CategoryTheory.yonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map α.1.unop) (CategoryTheory.CategoryStruct.comp β α.2)
def
CategoryTheory.yonedaCompUliftFunctorEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ w)))
(X : C)
:
((CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v₁} ⟶ F) ≃ F.obj (Opposite.op X)
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.
See https://stacks.math.columbia.edu/tag/001P.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.curriedYonedaLemma
{C : Type u₁}
[CategoryTheory.SmallCategory C]
:
CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda ≅ CategoryTheory.evaluation Cᵒᵖ (Type u₁)
The curried version of yoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.largeCurriedYonedaLemma
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation Cᵒᵖ (Type v₁)).comp
((CategoryTheory.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj
CategoryTheory.uliftFunctor.{u₁, v₁} )
The curried version of the Yoneda lemma.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.yonedaOpCompYonedaObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
:
CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj P) ≅ P.comp CategoryTheory.uliftFunctor.{u₁, v₁}
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.
def
CategoryTheory.curriedYonedaLemma'
{C : Type u₁}
[CategoryTheory.SmallCategory C]
:
CategoryTheory.yoneda.comp
((CategoryTheory.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type u₁))ᵒᵖ (Type u₁)).obj
CategoryTheory.yoneda.op) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type u₁))
The curried version of yoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.isIso_of_yoneda_map_bijective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryTheory.CategoryStruct.comp x f)
:
theorem
CategoryTheory.isIso_iff_yoneda_map_bijective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.IsIso f ↔ ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryTheory.CategoryStruct.comp x f
theorem
CategoryTheory.isIso_iff_isIso_yoneda_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.IsIso f ↔ ∀ (c : C), CategoryTheory.IsIso ((CategoryTheory.yoneda.map f).app (Opposite.op c))
def
CategoryTheory.coyonedaEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{F : CategoryTheory.Functor C (Type v₁)}
:
(CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) ≃ F.obj X
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.
theorem
CategoryTheory.coyonedaEquiv_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{F : CategoryTheory.Functor C (Type v₁)}
(f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F)
:
CategoryTheory.coyonedaEquiv f = f.app X (CategoryTheory.CategoryStruct.id X)
@[simp]
theorem
CategoryTheory.coyonedaEquiv_symm_app_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{F : CategoryTheory.Functor C (Type v₁)}
(x : F.obj X)
(Y : C)
(f : X ⟶ Y)
:
(CategoryTheory.coyonedaEquiv.symm x).app Y f = F.map f x
theorem
CategoryTheory.coyonedaEquiv_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{F : CategoryTheory.Functor C (Type v₁)}
(f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F)
(g : X ⟶ Y)
:
F.map g (CategoryTheory.coyonedaEquiv f) = CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map g.op) f)
theorem
CategoryTheory.coyonedaEquiv_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{F : CategoryTheory.Functor C (Type v₁)}
{G : CategoryTheory.Functor C (Type v₁)}
(α : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F)
(β : F ⟶ G)
:
CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app X (CategoryTheory.coyonedaEquiv α)
theorem
CategoryTheory.coyonedaEquiv_coyoneda_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.coyonedaEquiv (CategoryTheory.coyoneda.map f.op) = f
theorem
CategoryTheory.map_coyonedaEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{F : CategoryTheory.Functor C (Type v₁)}
(f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F)
(g : X ⟶ Y)
:
F.map g (CategoryTheory.coyonedaEquiv f) = f.app Y g
theorem
CategoryTheory.coyonedaEquiv_symm_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{F : CategoryTheory.Functor C (Type v₁)}
(t : F.obj X)
:
CategoryTheory.coyonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map f.op) (CategoryTheory.coyonedaEquiv.symm t)
def
CategoryTheory.coyonedaEvaluation
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.Functor (C × CategoryTheory.Functor C (Type v₁)) (Type (max u₁ v₁))
The "Coyoneda evaluation" functor, which sends X : C and F : C ⥤ Type
to F.obj X, functorially in both X and F.
Equations
@[simp]
theorem
CategoryTheory.coyonedaEvaluation_map_down
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(P : C × CategoryTheory.Functor C (Type v₁))
(Q : C × CategoryTheory.Functor C (Type v₁))
(α : P ⟶ Q)
(x : (CategoryTheory.coyonedaEvaluation C).obj P)
:
((CategoryTheory.coyonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
def
CategoryTheory.coyonedaPairing
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.Functor (C × CategoryTheory.Functor C (Type v₁)) (Type (max u₁ v₁))
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.
theorem
CategoryTheory.coyonedaPairingExt_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C × CategoryTheory.Functor C (Type v₁)}
{x : (CategoryTheory.coyonedaPairing C).obj X}
{y : (CategoryTheory.coyonedaPairing C).obj X}
:
theorem
CategoryTheory.coyonedaPairingExt
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
{X : C × CategoryTheory.Functor C (Type v₁)}
{x : (CategoryTheory.coyonedaPairing C).obj X}
{y : (CategoryTheory.coyonedaPairing C).obj X}
(w : ∀ (Y : C), x.app Y = y.app Y)
:
x = y
@[simp]
theorem
CategoryTheory.coyonedaPairing_map
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(P : C × CategoryTheory.Functor C (Type v₁))
(Q : C × CategoryTheory.Functor C (Type v₁))
(α : P ⟶ Q)
(β : (CategoryTheory.coyonedaPairing C).obj P)
:
(CategoryTheory.coyonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map α.1.op) (CategoryTheory.CategoryStruct.comp β α.2)
def
CategoryTheory.coyonedaCompUliftFunctorEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(F : CategoryTheory.Functor C (Type (max v₁ w)))
(X : Cᵒᵖ)
:
((CategoryTheory.coyoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v₁} ⟶ F) ≃ F.obj (Opposite.unop X)
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.
See https://stacks.math.columbia.edu/tag/001P.
Equations
- CategoryTheory.coyonedaLemma C = CategoryTheory.NatIso.ofComponents (fun (x : C × CategoryTheory.Functor C (Type ?u.25)) => (CategoryTheory.coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯
def
CategoryTheory.curriedCoyonedaLemma
{C : Type u₁}
[CategoryTheory.SmallCategory C]
:
CategoryTheory.coyoneda.rightOp.comp CategoryTheory.coyoneda ≅ CategoryTheory.evaluation C (Type u₁)
The curried version of coyoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.largeCurriedCoyonedaLemma
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
CategoryTheory.coyoneda.rightOp.comp CategoryTheory.coyoneda ≅ (CategoryTheory.evaluation C (Type v₁)).comp
((CategoryTheory.whiskeringRight (CategoryTheory.Functor C (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj
CategoryTheory.uliftFunctor.{u₁, v₁} )
The curried version of the Coyoneda lemma.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.coyonedaCompYonedaObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(P : CategoryTheory.Functor C (Type v₁))
:
CategoryTheory.coyoneda.rightOp.comp (CategoryTheory.yoneda.obj P) ≅ P.comp CategoryTheory.uliftFunctor.{u₁, v₁}
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.
def
CategoryTheory.curriedCoyonedaLemma'
{C : Type u₁}
[CategoryTheory.SmallCategory C]
:
CategoryTheory.yoneda.comp
((CategoryTheory.whiskeringLeft C (CategoryTheory.Functor C (Type u₁))ᵒᵖ (Type u₁)).obj
CategoryTheory.coyoneda.rightOp) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor C (Type u₁))
The curried version of coyoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.isIso_of_coyoneda_map_bijective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : ∀ (T : C), Function.Bijective fun (x : Y ⟶ T) => CategoryTheory.CategoryStruct.comp f x)
:
theorem
CategoryTheory.isIso_iff_coyoneda_map_bijective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.IsIso f ↔ ∀ (T : C), Function.Bijective fun (x : Y ⟶ T) => CategoryTheory.CategoryStruct.comp f x
theorem
CategoryTheory.isIso_iff_isIso_coyoneda_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.IsIso f ↔ ∀ (c : C), CategoryTheory.IsIso ((CategoryTheory.coyoneda.map f.op).app c)
def
CategoryTheory.yonedaMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{v₁, u_1} D]
(F : CategoryTheory.Functor C D)
(X : C)
:
CategoryTheory.yoneda.obj X ⟶ F.op.comp (CategoryTheory.yoneda.obj (F.obj X))
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 := ⋯ }
@[simp]
theorem
CategoryTheory.yonedaMap_app_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{v₁, u_1} D]
(F : CategoryTheory.Functor C D)
{Y : C}
{X : Cᵒᵖ}
(f : Opposite.unop X ⟶ Y)
:
(CategoryTheory.yonedaMap F Y).app X f = F.map f
def
CategoryTheory.Functor.FullyFaithful.homNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
(X : C)
:
F.op.comp ((CategoryTheory.yoneda.obj (F.obj X)).comp CategoryTheory.uliftFunctor.{v₁, v₂} ) ≅ (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{v₂, v₁}
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) ⋯
def
CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{max v₁ v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
(X : C)
:
F.op.comp (CategoryTheory.yoneda.obj (F.obj X)) ≅ (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{v₂, v₁}
FullyFaithful.homEquiv as a natural isomorphism.
Equations
- hF.homNatIsoMaxRight X = CategoryTheory.NatIso.ofComponents (fun (Y : Cᵒᵖ) => (hF.homEquiv.symm.trans Equiv.ulift.symm).toIso) ⋯