IsRepresentedBy predicate

In this file we define the predicate IsRepresentedBy: A presheaf F is represented by X with universal element x : F.obj X if the natural transformation yoneda.obj X ⟶ F induced by x is an isomorphism.

For other declarations expressing a functor is representable, see also:

• CategoryTheory.Functor.RepresentableBy: Structure bundling an explicit natural isomorphism yoneda.obj X ⟶ F.
• CategoryTheory.Functor.IsRepresentable: Predicate asserting the existence of a representing object.

The relations to these other notions are given as CategoryTheory.Functor.IsRepresentable.iff_exists_isRepresentedBy and CategoryTheory.Functor.IsRepresentedBy.iff_exists_representableBy.

TODOs

• Dualize to IsCorepresentedBy.

structure CategoryTheory.Functor.IsRepresentedBy {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) {X : C} (x : F.obj (Opposite.op X)) : Prop

A presheaf F is represented by X with universal element x : F.obj X if the natural transformation yoneda.obj X ⟶ F induced by x is an isomorphism. For better universe generality, we state this manually as for every Y, the induced map (Y ⟶ X) → F.obj Y is bijective.

• map_bijective {Y : C} : Function.Bijective fun (f : Y ⟶ X) => F.map f.op x

theorem CategoryTheory.Functor.isRepresentedBy_iff {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) {X : C} (x : F.obj (Opposite.op X)) : F.IsRepresentedBy x ↔ ∀ {Y : C}, Function.Bijective fun (f : Y ⟶ X) => F.map f.op x

theorem CategoryTheory.Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} : F.IsRepresentedBy x ↔ IsIso (uliftYonedaEquiv.symm { down := x })

noncomputable def CategoryTheory.Functor.IsRepresentedBy.uliftYonedaIso {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} (h : F.IsRepresentedBy x) : uliftYoneda.{w, v, u}.obj X ≅ F.comp uliftFunctor.{v, w}

If F is represented by X with universal element x : F.obj X, modulo universe lifting, it is isomorphic to yoneda.obj X.

Equations

• h.uliftYonedaIso = CategoryTheory.asIso (CategoryTheory.uliftYonedaEquiv.symm { down := x })

@[simp]

theorem CategoryTheory.Functor.IsRepresentedBy.uliftYonedaIso_hom {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} (h : F.IsRepresentedBy x) : h.uliftYonedaIso.hom = uliftYonedaEquiv.symm { down := x }

noncomputable def CategoryTheory.Functor.IsRepresentedBy.representableBy {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} (h : F.IsRepresentedBy x) : F.RepresentableBy X

The canonical representation induced by the universal element x : F.obj X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.IsRepresentedBy.representableBy_homEquiv_apply {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} (h : F.IsRepresentedBy x) {Y : C} (f : Y ⟶ X) : h.representableBy.homEquiv f = F.map f.op x

theorem CategoryTheory.Functor.RepresentableBy.isRepresentedBy {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} (R : F.RepresentableBy X) : F.IsRepresentedBy (R.homEquiv (CategoryStruct.id X))

theorem CategoryTheory.Functor.IsRepresentedBy.iff_exists_representableBy {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} : F.IsRepresentedBy x ↔ ∃ (R : F.RepresentableBy X), R.homEquiv (CategoryStruct.id X) = x

theorem CategoryTheory.Functor.IsRepresentedBy.of_natIso {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} (h : F.IsRepresentedBy x) {F' : Functor Cᵒᵖ (Type w)} (e : F ≅ F') : F'.IsRepresentedBy (e.hom.app (Opposite.op X) x)

theorem CategoryTheory.Functor.IsRepresentedBy.iff_natIso {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} {F' : Functor Cᵒᵖ (Type w)} (e : F ≅ F') : F'.IsRepresentedBy (e.hom.app (Opposite.op X) x) ↔ F.IsRepresentedBy x

theorem CategoryTheory.Functor.IsRepresentedBy.of_isoObj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} (h : F.IsRepresentedBy x) {Y : C} (e : Y ≅ X) : F.IsRepresentedBy (F.map e.hom.op x)

theorem CategoryTheory.Functor.IsRepresentedBy.iff_of_isoObj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {X : C} {x : F.obj (Opposite.op X)} {Y : C} (e : Y ≅ X) : F.IsRepresentedBy (F.map e.hom.op x) ↔ F.IsRepresentedBy x

theorem CategoryTheory.Functor.IsRepresentedBy.of_isRepresentable {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} [F.IsRepresentable] : F.IsRepresentedBy F.reprx

theorem CategoryTheory.Functor.IsRepresentable.iff_exists_isRepresentedBy {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} : F.IsRepresentable ↔ ∃ (X : C) (x : F.obj (Opposite.op X)), F.IsRepresentedBy x