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} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasCoproducts A] (X : C) (M : A) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasCoproducts A] (X : C) (M : A) (Y : Cᵒᵖ) : (CategoryTheory.Presheaf.freeYoneda X M).obj Y = ∐ fun (i : (CategoryTheory.yoneda.obj X).obj Y) => M

@[simp]

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

noncomputable def CategoryTheory.Presheaf.freeYonedaHomEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasCoproducts A] {X : C} {M : A} {F : CategoryTheory.Functor Cᵒᵖ A} : (CategoryTheory.Presheaf.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} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasCoproducts A] {X : C} {M : A} {F G : CategoryTheory.Functor Cᵒᵖ A} (α : CategoryTheory.Presheaf.freeYoneda X M ⟶ F) (f : F ⟶ G) : CategoryTheory.Presheaf.freeYonedaHomEquiv (CategoryTheory.CategoryStruct.comp α f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.freeYonedaHomEquiv α) (f.app (Opposite.op X))

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

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

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

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

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

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