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.
Instances For
@[simp]
theorem
CategoryTheory.yoneda_map_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
(x✝ : Cᵒᵖ)
(g :
{ obj := fun (Y : Cᵒᵖ) => Opposite.unop Y ⟶ X✝,
map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) (g : Opposite.unop X ⟶ X✝) => CategoryStruct.comp f.unop g, map_id := ⋯,
map_comp := ⋯ }.obj
x✝)
:
@[simp]
@[simp]
theorem
CategoryTheory.yoneda_obj_map
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
{X✝ Y✝ : Cᵒᵖ}
(f : X✝ ⟶ Y✝)
(g : Opposite.unop X✝ ⟶ X)
:
Variant of the Yoneda embedding which allows a raise in the universe level for the category of types.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.uliftYoneda_obj_map_down
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
{X✝ Y✝ : Cᵒᵖ}
(f : X✝ ⟶ Y✝)
(a✝ : uliftFunctor.{w, v₁}.obj ((yoneda.obj X).obj X✝))
:
@[simp]
@[simp]
theorem
CategoryTheory.uliftYoneda_map_app_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
(X : Cᵒᵖ)
(a✝ : uliftFunctor.{w, v₁}.obj ((yoneda.obj X✝).obj X))
:
If C is a category with [Category.{max w v₁} C], this is the isomorphism
uliftYoneda.{w} (C := C) ≅ yoneda.
Equations
- CategoryTheory.uliftYonedaIsoYoneda = CategoryTheory.NatIso.ofComponents (fun (x : C) => CategoryTheory.NatIso.ofComponents (fun (x_1 : Cᵒᵖ) => Equiv.ulift.toIso) ⋯) ⋯
Instances For
@[simp]
theorem
CategoryTheory.uliftYonedaIsoYoneda_inv_app_app_down
{C : Type u₁}
[Category.{max w v₁, u₁} C]
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : (yoneda.obj X).obj X✝)
:
@[simp]
theorem
CategoryTheory.uliftYonedaIsoYoneda_hom_app_app
{C : Type u₁}
[Category.{max w v₁, u₁} C]
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : (uliftYoneda.{w, max v₁ w, u₁}.obj X).obj X✝)
:
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.
Instances For
@[simp]
theorem
CategoryTheory.coyoneda_map_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X✝ Y✝ : Cᵒᵖ}
(f : X✝ ⟶ Y✝)
(x✝ : C)
(g :
{ obj := fun (Y : C) => Opposite.unop X✝ ⟶ Y,
map := fun {X Y : C} (f : X ⟶ Y) (g : Opposite.unop X✝ ⟶ X) => CategoryStruct.comp g f, map_id := ⋯,
map_comp := ⋯ }.obj
x✝)
:
@[simp]
@[simp]
theorem
CategoryTheory.coyoneda_obj_map
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Cᵒᵖ)
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
(g : Opposite.unop X ⟶ X✝)
:
theorem
CategoryTheory.Yoneda.obj_map_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : Opposite.op X ⟶ Opposite.op Y)
:
(yoneda.obj X).map f (CategoryStruct.id X) = (yoneda.map f.unop).app (Opposite.op Y) (CategoryStruct.id Y)
@[simp]
theorem
CategoryTheory.Yoneda.naturality
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(α : yoneda.obj X ⟶ yoneda.obj Y)
{Z Z' : C}
(f : Z ⟶ Z')
(h : Z' ⟶ X)
:
The Yoneda embedding is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Yoneda.fullyFaithful_preimage
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : yoneda.obj X ⟶ yoneda.obj Y)
:
The Yoneda embedding is full.
The Yoneda embedding is faithful.
def
CategoryTheory.Yoneda.ext
{C : Type u₁}
[Category.{v₁, u₁} C]
(X 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 (CategoryStruct.comp f g) = CategoryStruct.comp f (p g))
:
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.
Instances For
theorem
CategoryTheory.Yoneda.isIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
[IsIso (yoneda.map f)]
:
IsIso f
If yoneda.map f is an isomorphism, so was f.
When C is category such that Category.{v₁} C, then
the functor uliftYoneda.{w} : C ⥤ Cᵒᵖ ⥤ Type max w v₁ is fully faithful.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Coyoneda.naturality
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
(α : coyoneda.obj X ⟶ coyoneda.obj Y)
{Z Z' : C}
(f : Z' ⟶ Z)
(h : Opposite.unop X ⟶ Z')
:
The co-Yoneda embedding is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Coyoneda.fullyFaithful_preimage
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
(f : coyoneda.obj X ⟶ coyoneda.obj Y)
:
fullyFaithful.preimage f = Quiver.Hom.op (f.app (Opposite.unop X) (CategoryStruct.id (Opposite.unop X)))
def
CategoryTheory.Coyoneda.preimage
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
(f : coyoneda.obj X ⟶ coyoneda.obj Y)
:
The morphism X ⟶ Y corresponding to a natural transformation
coyoneda.obj X ⟶ coyoneda.obj Y.
Equations
Instances For
def
CategoryTheory.Coyoneda.ext
{C : Type u₁}
[Category.{v₁, u₁} C]
(X Y : C)
(p : {Z : C} → (X ⟶ Z) → (Y ⟶ Z))
(q : {Z : C} → (Y ⟶ Z) → (X ⟶ Z))
(h₁ : ∀ {Z : C} (f : X ⟶ Z), q (p f) = f)
(h₂ : ∀ {Z : C} (f : Y ⟶ Z), p (q f) = f)
(n : ∀ {Z Z' : C} (f : Y ⟶ Z) (g : Z ⟶ Z'), q (CategoryStruct.comp f g) = CategoryStruct.comp (q f) g)
:
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.
Instances For
theorem
CategoryTheory.Coyoneda.isIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
(f : X ⟶ Y)
[IsIso (coyoneda.map f)]
:
IsIso f
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.
Instances For
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) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Coyoneda.objOpOp_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : (coyoneda.obj (Opposite.op (Opposite.op X))).obj X✝)
:
@[simp]
theorem
CategoryTheory.Coyoneda.objOpOp_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : (yoneda.obj X).obj X✝)
:
Taking the unop of morphisms is a natural isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
CategoryTheory.Functor.RepresentableBy
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : 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.
the natural bijection
(X ⟶ Y) ≃ F.obj (op X).
Instances For
theorem
CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v)}
{Y : C}
(e : F.RepresentableBy Y)
{X X' : C}
(x : F.obj (Opposite.op X'))
(f : X ⟶ X')
:
def
CategoryTheory.Functor.RepresentableBy.ofIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{F F' : 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
Instances For
structure
CategoryTheory.Functor.CorepresentableBy
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : 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.
Instances For
theorem
CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
{X : C}
(e : F.CorepresentableBy X)
{Y Y' : C}
(y : F.obj Y)
(g : Y ⟶ Y')
:
def
CategoryTheory.Functor.CorepresentableBy.ofIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{F F' : 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
Instances For
theorem
CategoryTheory.Functor.RepresentableBy.homEquiv_eq
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v)}
{Y : C}
(e : F.RepresentableBy Y)
{X : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Functor.CorepresentableBy.homEquiv_eq
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
{X : C}
(e : F.CorepresentableBy X)
{Y : C}
(f : X ⟶ Y)
:
def
CategoryTheory.Functor.RepresentableBy.uniqueUpToIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v)}
{Y Y' : C}
(e : F.RepresentableBy Y)
(e' : F.RepresentableBy Y')
:
Representing objects are unique up to isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v)}
{Y Y' : C}
(e : F.RepresentableBy Y)
(e' : F.RepresentableBy Y')
:
@[simp]
theorem
CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v)}
{Y Y' : C}
(e : F.RepresentableBy Y)
(e' : F.RepresentableBy Y')
:
def
CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
{X X' : C}
(e : F.CorepresentableBy X)
(e' : F.CorepresentableBy X')
:
Corepresenting objects are unique up to isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
{X X' : C}
(e : F.CorepresentableBy X)
(e' : F.CorepresentableBy X')
:
@[simp]
theorem
CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
{X X' : C}
(e : F.CorepresentableBy X)
(e' : F.CorepresentableBy X')
:
theorem
CategoryTheory.Functor.RepresentableBy.ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v)}
{Y : C}
{e e' : F.RepresentableBy Y}
(h : e.homEquiv (CategoryStruct.id Y) = e'.homEquiv (CategoryStruct.id Y))
:
theorem
CategoryTheory.Functor.RepresentableBy.ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v)}
{Y : C}
{e e' : F.RepresentableBy Y}
:
theorem
CategoryTheory.Functor.CorepresentableBy.ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
{X : C}
{e e' : F.CorepresentableBy X}
(h : e.homEquiv (CategoryStruct.id X) = e'.homEquiv (CategoryStruct.id X))
:
theorem
CategoryTheory.Functor.CorepresentableBy.ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
{X : C}
{e e' : F.CorepresentableBy X}
:
def
CategoryTheory.Functor.representableByEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : 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.
Instances For
def
CategoryTheory.Functor.RepresentableBy.toIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v₁)}
{Y : C}
(e : F.RepresentableBy Y)
:
The isomorphism yoneda.obj Y ≅ F induced by e : F.RepresentableBy Y.
Equations
Instances For
def
CategoryTheory.Functor.corepresentableByEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v₁)}
{X : C}
:
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.
Instances For
def
CategoryTheory.Functor.CorepresentableBy.toIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v₁)}
{X : C}
(e : F.CorepresentableBy X)
:
The isomorphism coyoneda.obj (op X) ≅ F induced by e : F.CorepresentableBy X.
Equations
Instances For
class
CategoryTheory.Functor.IsRepresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor Cᵒᵖ (Type v))
:
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.
Instances
theorem
CategoryTheory.Functor.RepresentableBy.isRepresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v)}
{Y : C}
(e : F.RepresentableBy Y)
:
theorem
CategoryTheory.Functor.IsRepresentable.mk'
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor Cᵒᵖ (Type v₁)}
{X : C}
(e : yoneda.obj X ≅ F)
:
Alternative constructor for F.IsRepresentable, which takes as an input an
isomorphism yoneda.obj X ≅ F.
instance
CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
:
(yoneda.obj X).IsRepresentable
class
CategoryTheory.Functor.IsCorepresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type v))
:
A functor F : C ⥤ Type v₁ is corepresentable if there is object X so F ≅ coyoneda.obj X.
Instances
theorem
CategoryTheory.Functor.CorepresentableBy.isCorepresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
{X : C}
(e : F.CorepresentableBy X)
:
theorem
CategoryTheory.Functor.IsCorepresentable.mk'
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v₁)}
{X : C}
(e : coyoneda.obj (Opposite.op X) ≅ F)
:
Alternative constructor for F.IsCorepresentable, which takes as an input an
isomorphism coyoneda.obj (op X) ≅ F.
instance
CategoryTheory.Functor.instIsCorepresentableObjOppositeTypeCoyoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : Cᵒᵖ}
:
noncomputable def
CategoryTheory.Functor.reprX
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor Cᵒᵖ (Type v))
[hF : F.IsRepresentable]
:
C
The representing object for the representable functor F.
Instances For
noncomputable def
CategoryTheory.Functor.representableBy
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : 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
Instances For
noncomputable def
CategoryTheory.Functor.RepresentableBy.isoReprX
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor Cᵒᵖ (Type v))
[hF : F.IsRepresentable]
{Y : C}
(e : F.RepresentableBy Y)
:
Any representing object for a representable functor F is isomorphic to reprX F.
Equations
Instances For
noncomputable def
CategoryTheory.Functor.reprx
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : 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
Instances For
noncomputable def
CategoryTheory.Functor.reprW
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor Cᵒᵖ (Type v₁))
[F.IsRepresentable]
:
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
Instances For
theorem
CategoryTheory.Functor.reprW_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor Cᵒᵖ (Type v₁))
[F.IsRepresentable]
(X : Cᵒᵖ)
(f : Opposite.unop X ⟶ F.reprX)
:
noncomputable def
CategoryTheory.Functor.coreprX
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type v))
[hF : F.IsCorepresentable]
:
C
The representing object for the corepresentable functor F.
Instances For
noncomputable def
CategoryTheory.Functor.corepresentableBy
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type v))
[hF : F.IsCorepresentable]
:
A chosen term in F.CorepresentableBy (coreprX F) when F.IsCorepresentable holds.
Equations
- F.corepresentableBy = ⋯.some
Instances For
noncomputable def
CategoryTheory.Functor.CorepresentableBy.isoCoreprX
{C : Type u₁}
[Category.{v₁, u₁} C]
{F : Functor C (Type v)}
[hF : F.IsCorepresentable]
{Y : C}
(e : F.CorepresentableBy Y)
:
Any corepresenting object for a corepresentable functor F is isomorphic to coreprX F.
Equations
Instances For
noncomputable def
CategoryTheory.Functor.coreprx
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type v))
[hF : F.IsCorepresentable]
:
The representing element for the corepresentable functor F, sometimes called the universal
element of the functor.
Equations
Instances For
noncomputable def
CategoryTheory.Functor.coreprW
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type v₁))
[F.IsCorepresentable]
:
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
Instances For
theorem
CategoryTheory.Functor.coreprW_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type v₁))
[F.IsCorepresentable]
(X : C)
(f : F.coreprX ⟶ X)
:
theorem
CategoryTheory.isRepresentable_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor Cᵒᵖ (Type v₁))
{G : Functor Cᵒᵖ (Type v₁)}
(i : F ≅ G)
[F.IsRepresentable]
:
theorem
CategoryTheory.corepresentable_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type v₁))
{G : Functor C (Type v₁)}
(i : F ≅ G)
[F.IsCorepresentable]
:
Equations
Equations
def
CategoryTheory.yonedaEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor Cᵒᵖ (Type v₁)}
:
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.
Instances For
theorem
CategoryTheory.yonedaEquiv_apply
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor Cᵒᵖ (Type v₁)}
(f : yoneda.obj X ⟶ F)
:
@[simp]
theorem
CategoryTheory.yonedaEquiv_symm_app_apply
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor Cᵒᵖ (Type v₁)}
(x : F.obj (Opposite.op X))
(Y : Cᵒᵖ)
(f : Opposite.unop Y ⟶ X)
:
theorem
CategoryTheory.yonedaEquiv_naturality
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
{F : Functor Cᵒᵖ (Type v₁)}
(f : yoneda.obj X ⟶ F)
(g : Y ⟶ X)
:
See also yonedaEquiv_naturality' for a more general version.
theorem
CategoryTheory.yonedaEquiv_naturality'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
{F : Functor Cᵒᵖ (Type v₁)}
(f : yoneda.obj (Opposite.unop X) ⟶ F)
(g : X ⟶ Y)
:
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₁}
[Category.{v₁, u₁} C]
{X : C}
{F G : Functor Cᵒᵖ (Type v₁)}
(α : yoneda.obj X ⟶ F)
(β : F ⟶ G)
:
theorem
CategoryTheory.yonedaEquiv_yoneda_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.yonedaEquiv_symm_naturality_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{X X' : C}
(f : X' ⟶ X)
(F : Functor Cᵒᵖ (Type v₁))
(x : F.obj (Opposite.op X))
:
theorem
CategoryTheory.yonedaEquiv_symm_naturality_right
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
{F F' : Functor Cᵒᵖ (Type v₁)}
(f : F ⟶ F')
(x : F.obj (Opposite.op X))
:
theorem
CategoryTheory.map_yonedaEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
{F : Functor Cᵒᵖ (Type v₁)}
(f : yoneda.obj X ⟶ F)
(g : Y ⟶ X)
:
See also map_yonedaEquiv' for a more general version.
theorem
CategoryTheory.map_yonedaEquiv'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
{F : Functor Cᵒᵖ (Type v₁)}
(f : yoneda.obj (Opposite.unop X) ⟶ F)
(g : X ⟶ Y)
:
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₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
(f : X ⟶ Y)
{F : Functor Cᵒᵖ (Type v₁)}
(t : F.obj X)
:
theorem
CategoryTheory.hom_ext_yoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{P Q : Functor Cᵒᵖ (Type v₁)}
{f g : P ⟶ Q}
(h : ∀ (X : C) (p : yoneda.obj X ⟶ P), CategoryStruct.comp p f = CategoryStruct.comp p g)
:
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.
Equations
Instances For
@[simp]
theorem
CategoryTheory.yonedaEvaluation_map_down
(C : Type u₁)
[Category.{v₁, u₁} C]
(P Q : Cᵒᵖ × Functor Cᵒᵖ (Type v₁))
(α : P ⟶ Q)
(x : (yonedaEvaluation C).obj P)
:
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.
Instances For
@[simp]
theorem
CategoryTheory.yonedaPairing_map
(C : Type u₁)
[Category.{v₁, u₁} C]
(P Q : Cᵒᵖ × Functor Cᵒᵖ (Type v₁))
(α : P ⟶ Q)
(β : (yonedaPairing C).obj P)
:
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.
Instances For
The curried version of yoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The curried version of the Yoneda lemma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.yonedaOpCompYonedaObj
{C : Type u₁}
[Category.{v₁, u₁} C]
(P : Functor Cᵒᵖ (Type 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.
Instances For
The curried version of yoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.isIso_of_yoneda_map_bijective
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
(hf : ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryStruct.comp x f)
:
IsIso f
theorem
CategoryTheory.isIso_iff_yoneda_map_bijective
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.isIso_iff_isIso_yoneda_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
:
def
CategoryTheory.uliftYonedaEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor Cᵒᵖ (Type (max w v₁))}
:
Yoneda's lemma as a bijection (uliftYoneda.{w}.obj X ⟶ F) ≃ F.obj (op X)
for any presheaf of type F : Cᵒᵖ ⥤ Type (max w v₁) for some
auxiliary universe w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.uliftYonedaEquiv_apply
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor Cᵒᵖ (Type (max w v₁))}
(τ : uliftYoneda.{w, v₁, u₁}.obj X ⟶ F)
:
@[simp]
theorem
CategoryTheory.uliftYonedaEquiv_symm_apply_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor Cᵒᵖ (Type (max w v₁))}
(x : F.obj (Opposite.op X))
(Y : Cᵒᵖ)
(y : (uliftYoneda.{w, v₁, u₁}.obj X).obj Y)
:
@[deprecated CategoryTheory.uliftYonedaEquiv (since := "2025-08-04")]
def
CategoryTheory.yonedaCompUliftFunctorEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor Cᵒᵖ (Type (max w v₁))}
:
Alias of CategoryTheory.uliftYonedaEquiv.
Yoneda's lemma as a bijection (uliftYoneda.{w}.obj X ⟶ F) ≃ F.obj (op X)
for any presheaf of type F : Cᵒᵖ ⥤ Type (max w v₁) for some
auxiliary universe w.
Instances For
theorem
CategoryTheory.uliftYonedaEquiv_naturality
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
{F : Functor Cᵒᵖ (Type (max w v₁))}
(f : uliftYoneda.{w, v₁, u₁}.obj (Opposite.unop X) ⟶ F)
(g : X ⟶ Y)
:
F.map g (uliftYonedaEquiv f) = uliftYonedaEquiv (CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map g.unop) f)
theorem
CategoryTheory.uliftYonedaEquiv_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F G : Functor Cᵒᵖ (Type (max w v₁))}
(α : uliftYoneda.{w, v₁, u₁}.obj X ⟶ F)
(β : F ⟶ G)
:
theorem
CategoryTheory.uliftYonedaEquiv_symm_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
(f : X ⟶ Y)
{F : Functor Cᵒᵖ (Type (max w v₁))}
(t : F.obj X)
:
uliftYonedaEquiv.symm (F.map f t) = CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map f.unop) (uliftYonedaEquiv.symm t)
theorem
CategoryTheory.uliftYonedaEquiv_symm_map_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : Cᵒᵖ}
(f : X ⟶ Y)
{F : Functor Cᵒᵖ (Type (max w v₁))}
(t : F.obj X)
{Z : Functor Cᵒᵖ (Type (max w v₁))}
(h : F ⟶ Z)
:
CategoryStruct.comp (uliftYonedaEquiv.symm (F.map f t)) h = CategoryStruct.comp (uliftYoneda.{w, v₁, u₁}.map f.unop) (CategoryStruct.comp (uliftYonedaEquiv.symm t) h)
@[simp]
theorem
CategoryTheory.uliftYonedaEquiv_uliftYoneda_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.hom_ext_uliftYoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{P Q : Functor Cᵒᵖ (Type (max w v₁))}
{f g : P ⟶ Q}
(h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.obj X ⟶ P), CategoryStruct.comp p f = CategoryStruct.comp p g)
:
Two morphisms of presheaves of types P ⟶ Q coincide if the precompositions
with morphisms uliftYoneda.obj X ⟶ P agree.
def
CategoryTheory.coyonedaEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor C (Type v₁)}
:
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.
Instances For
theorem
CategoryTheory.coyonedaEquiv_apply
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor C (Type v₁)}
(f : coyoneda.obj (Opposite.op X) ⟶ F)
:
@[simp]
theorem
CategoryTheory.coyonedaEquiv_symm_app_apply
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F : Functor C (Type v₁)}
(x : F.obj X)
(Y : C)
(f : X ⟶ Y)
:
theorem
CategoryTheory.coyonedaEquiv_naturality
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
{F : Functor C (Type v₁)}
(f : coyoneda.obj (Opposite.op X) ⟶ F)
(g : X ⟶ Y)
:
theorem
CategoryTheory.coyonedaEquiv_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
{F G : Functor C (Type v₁)}
(α : coyoneda.obj (Opposite.op X) ⟶ F)
(β : F ⟶ G)
:
theorem
CategoryTheory.coyonedaEquiv_coyoneda_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.map_coyonedaEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
{F : Functor C (Type v₁)}
(f : coyoneda.obj (Opposite.op X) ⟶ F)
(g : X ⟶ Y)
:
theorem
CategoryTheory.coyonedaEquiv_symm_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
{F : Functor C (Type v₁)}
(t : F.obj X)
:
The "Coyoneda evaluation" functor, which sends X : C and F : C ⥤ Type
to F.obj X, functorially in both X and F.
Equations
Instances For
@[simp]
theorem
CategoryTheory.coyonedaEvaluation_map_down
(C : Type u₁)
[Category.{v₁, u₁} C]
(P Q : C × Functor C (Type v₁))
(α : P ⟶ Q)
(x : (coyonedaEvaluation C).obj P)
:
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.
Instances For
theorem
CategoryTheory.coyonedaPairingExt
(C : Type u₁)
[Category.{v₁, u₁} C]
{X : C × Functor C (Type v₁)}
{x y : (coyonedaPairing C).obj X}
(w : ∀ (Y : C), x.app Y = y.app Y)
:
theorem
CategoryTheory.coyonedaPairingExt_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C × Functor C (Type v₁)}
{x y : (coyonedaPairing C).obj X}
:
@[simp]
theorem
CategoryTheory.coyonedaPairing_map
(C : Type u₁)
[Category.{v₁, u₁} C]
(P Q : C × Functor C (Type v₁))
(α : P ⟶ Q)
(β : (coyonedaPairing C).obj P)
:
def
CategoryTheory.coyonedaCompUliftFunctorEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type (max v₁ w)))
(X : Cᵒᵖ)
:
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.
Instances For
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) ⋯
Instances For
The curried version of coyoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.largeCurriedCoyonedaLemma
{C : Type u₁}
[Category.{v₁, u₁} C]
:
coyoneda.rightOp.comp coyoneda ≅ (evaluation C (Type v₁)).comp
((Functor.whiskeringRight (Functor C (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁})
The curried version of the Coyoneda lemma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.coyonedaCompYonedaObj
{C : Type u₁}
[Category.{v₁, u₁} C]
(P : Functor C (Type 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.
Instances For
The curried version of coyoneda lemma when C is small.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.isIso_of_coyoneda_map_bijective
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
(hf : ∀ (T : C), Function.Bijective fun (x : Y ⟶ T) => CategoryStruct.comp f x)
:
IsIso f
theorem
CategoryTheory.isIso_iff_coyoneda_map_bijective
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(f : X ⟶ Y)
:
def
CategoryTheory.yonedaMap
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u_1}
[Category.{v₁, u_1} D]
(F : Functor C D)
(X : C)
:
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 := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.yonedaMap_app_apply
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u_1}
[Category.{v₁, u_1} D]
(F : Functor C D)
{Y : C}
{X : Cᵒᵖ}
(f : Opposite.unop X ⟶ Y)
:
def
CategoryTheory.uliftYonedaMap
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(X : C)
:
The natural transformation uliftYoneda.obj X ⟶ F.op ⋙ uliftYoneda.obj (F.obj X)
when F : C ⥤ D and X : C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.uliftYonedaMap_app_apply
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{Y : C}
{X : Cᵒᵖ}
(f : Opposite.unop X ⟶ Y)
:
def
CategoryTheory.Functor.sectionsEquivHom
{C : Type u₁}
[Category.{v₁, u₁} C]
(F : Functor C (Type u₂))
(X : Type u₂)
[Unique X]
:
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.
Instances For
theorem
CategoryTheory.Functor.sectionsEquivHom_naturality
{C : Type u₁}
[Category.{v₁, u₁} C]
{F G : Functor C (Type u₂)}
(f : F ⟶ G)
(X : Type u₂)
[Unique X]
(x : ↑F.sections)
:
(G.sectionsEquivHom X) ((sectionsFunctor C).map f x) = CategoryStruct.comp ((F.sectionsEquivHom X) x) f
theorem
CategoryTheory.Functor.sectionsEquivHom_naturality_symm
{C : Type u₁}
[Category.{v₁, u₁} C]
{F G : Functor C (Type u₂)}
(f : F ⟶ G)
(X : Type u₂)
[Unique X]
(τ : (const C).obj X ⟶ F)
:
(G.sectionsEquivHom X).symm (CategoryStruct.comp τ f) = (sectionsFunctor C).map f ((F.sectionsEquivHom X).symm τ)
noncomputable def
CategoryTheory.sectionsFunctorNatIsoCoyoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Type (max u₁ u₂))
[Unique X]
:
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) ⋯
Instances For
@[simp]
theorem
CategoryTheory.sectionsFunctorNatIsoCoyoneda_hom_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Type (max u₁ u₂))
[Unique X]
(X✝ : Functor C (Type (max u₁ u₂)))
(a✝ : (Functor.sectionsFunctor C).obj X✝)
(j : C)
(x : ((Functor.const C).obj X).obj j)
:
@[simp]
theorem
CategoryTheory.sectionsFunctorNatIsoCoyoneda_inv_app_coe
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Type (max u₁ u₂))
[Unique X]
(X✝ : Functor C (Type (max u₁ u₂)))
(a✝ : (coyoneda.obj (Opposite.op ((Functor.const C).obj X))).obj X✝)
(j : C)
:
def
CategoryTheory.Functor.FullyFaithful.homNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
:
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) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.homNatIso_hom_app_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : (F.op.comp ((yoneda.obj (F.obj X)).comp uliftFunctor.{v₁, v₂})).obj X✝)
:
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.homNatIso_inv_app_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝)
:
def
CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{max v₁ v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
:
FullyFaithful.homEquiv as a natural isomorphism.
Equations
- hF.homNatIsoMaxRight X = CategoryTheory.NatIso.ofComponents (fun (Y : Cᵒᵖ) => (hF.homEquiv.symm.trans Equiv.ulift.symm).toIso) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{max v₁ v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝)
:
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_hom_app_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{max v₁ v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : (F.op.comp (yoneda.obj (F.obj X))).obj X✝)
:
def
CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
:
F.comp
(yoneda.comp
(((whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₂)).obj F.op).comp
((Functor.whiskeringRight Cᵒᵖ (Type v₂) (Type (max v₂ v₁))).obj uliftFunctor.{v₁, v₂}))) ≅ yoneda.comp ((Functor.whiskeringRight Cᵒᵖ (Type v₁) (Type (max v₂ v₁))).obj uliftFunctor.{v₂, v₁})
FullyFaithful.homEquiv as a natural isomorphism.
Equations
- hF.compYonedaCompWhiskeringLeft = CategoryTheory.NatIso.ofComponents (fun (X : C) => hF.homNatIso X) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft_hom_app_app_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : (F.op.comp ((yoneda.obj (F.obj X)).comp uliftFunctor.{v₁, v₂})).obj X✝)
:
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft_inv_app_app_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝)
:
def
CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{max v₁ v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
:
FullyFaithful.homEquiv as a natural isomorphism.
Equations
- hF.compYonedaCompWhiskeringLeftMaxRight = CategoryTheory.NatIso.ofComponents (fun (X : C) => hF.homNatIsoMaxRight X) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{max v₁ v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : (F.op.comp (yoneda.obj (F.obj X))).obj X✝)
:
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_inv_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{max v₁ v₂, u₂} D]
{F : Functor C D}
(hF : F.FullyFaithful)
(X : C)
(X✝ : Cᵒᵖ)
(a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝)
: