Documentation

Mathlib.CategoryTheory.Generator.Presheaf

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.

source
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.
Instances For
    source
    @[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
    source
    @[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' ⇑(ConcreteCategory.hom ((yoneda.obj X).map f)) fun (x : (yoneda.obj X).obj X✝) => CategoryStruct.id M
    source
    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.
    Instances For
      source
      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))
      source
      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)
      source
      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)))
      source
      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
      source
      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 : (ObjectProperty.ofObj S).IsSeparating) :
      (ObjectProperty.ofObj fun (x : C × ι) => match x with | (X, i) => freeYoneda X (S i)).IsSeparating
      source
      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 : (ObjectProperty.ofObj S).IsSeparating) [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))
      source
      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)