Generators in the category of presheaves

In this file, we show that if A is a category with zero morphisms that has a separator (and suitable coproducts), then the category of presheaves Cᵒᵖ ⥤ A also has a separator.

noncomputable def CategoryTheory.Presheaf.freeYoneda {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] (X : C) (M : A) : Functor Cᵒᵖ A

Given X : C and M : A, this is the presheaf Cᵒᵖ ⥤ A which sends Y : Cᵒᵖ to the coproduct of copies of M indexed by Y.unop ⟶ X.

Equations

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

@[simp]

theorem CategoryTheory.Presheaf.freeYoneda_obj {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] (X : C) (M : A) (Y : Cᵒᵖ) : (freeYoneda X M).obj Y = ∐ fun (i : (yoneda.obj X).obj Y) => M

@[simp]

theorem CategoryTheory.Presheaf.freeYoneda_map {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] (X : C) (M : A) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (freeYoneda X M).map f = Limits.Sigma.map' ((yoneda.obj X).map f) fun (x : (yoneda.obj X).obj X✝) => CategoryStruct.id M

noncomputable def CategoryTheory.Presheaf.freeYonedaHomEquiv {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] {X : C} {M : A} {F : Functor Cᵒᵖ A} : (freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (Opposite.op X))

The bijection (Presheaf.freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X)).

Equations

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

theorem CategoryTheory.Presheaf.freeYonedaHomEquiv_comp {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] {X : C} {M : A} {F G : Functor Cᵒᵖ A} (α : freeYoneda X M ⟶ F) (f : F ⟶ G) : freeYonedaHomEquiv (CategoryStruct.comp α f) = CategoryStruct.comp (freeYonedaHomEquiv α) (f.app (Opposite.op X))

theorem CategoryTheory.Presheaf.freeYonedaHomEquiv_comp_assoc {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] {X : C} {M : A} {F G : Functor Cᵒᵖ A} (α : freeYoneda X M ⟶ F) (f : F ⟶ G) {Z : A} (h : G.obj (Opposite.op X) ⟶ Z) : CategoryStruct.comp (freeYonedaHomEquiv (CategoryStruct.comp α f)) h = CategoryStruct.comp (freeYonedaHomEquiv α) (CategoryStruct.comp (f.app (Opposite.op X)) h)

theorem CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_comp {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] {X : C} {M : A} {F G : Functor Cᵒᵖ A} (α : M ⟶ F.obj (Opposite.op X)) (f : F ⟶ G) : CategoryStruct.comp (freeYonedaHomEquiv.symm α) f = freeYonedaHomEquiv.symm (CategoryStruct.comp α (f.app (Opposite.op X)))

theorem CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_comp_assoc {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] {X : C} {M : A} {F G : Functor Cᵒᵖ A} (α : M ⟶ F.obj (Opposite.op X)) (f : F ⟶ G) {Z : Functor Cᵒᵖ A} (h : G ⟶ Z) : CategoryStruct.comp (freeYonedaHomEquiv.symm α) (CategoryStruct.comp f h) = CategoryStruct.comp (freeYonedaHomEquiv.symm (CategoryStruct.comp α (f.app (Opposite.op X)))) h

theorem CategoryTheory.Presheaf.isSeparating (C : Type u) [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) : IsSeparating (Set.range fun (x : C × ι) => match x with | (X, i) => freeYoneda X (S i))

theorem CategoryTheory.Presheaf.isSeparator (C : Type u) [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasCoproducts A] {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) [Limits.HasCoproduct fun (x : C × ι) => match x with | (X, i) => freeYoneda X (S i)] [Limits.HasZeroMorphisms A] : IsSeparator (∐ fun (x : C × ι) => match x with | (X, i) => freeYoneda X (S i))

instance CategoryTheory.Presheaf.hasSeparator (C : Type u) [Category.{v, u} C] (A : Type u') [Category.{v', u'} A] [Limits.HasCoproducts A] [HasSeparator A] [Limits.HasZeroMorphisms A] [Limits.HasCoproducts A] : HasSeparator (Functor Cᵒᵖ A)