Parallel pairs of natural transformations between ind-objects

We show that if A and B are ind-objects and f and g are natural transformations between A and B, then there is a small filtered category I such that A, B, f and g are commonly presented by diagrams and natural transformations in I ⥤ C.

References

• [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], Proposition 6.1.15 (though our proof is more direct).

structure CategoryTheory.IndParallelPairPresentation {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) : Type (max u₁ (v₁ + 1))

Structure containing data exhibiting two parallel natural transformations f and g between presheaves A and B as induced by a natural transformation in a functor category exhibiting A and B as ind-objects.

• I : Type v₁

  The indexing category.

• ℐ : SmallCategory self.I

  Category instance on the indexing category.

• hI : IsFiltered self.I
• F₁ : Functor self.I C

  The diagram presenting A.

• F₂ : Functor self.I C

  The diagram presenting B.

• ι₁ : self.F₁.comp yoneda ⟶ (Functor.const self.I).obj A

  The cocone on F₁ with apex A.

• isColimit₁ : Limits.IsColimit { pt := A, ι := self.ι₁ }

  The cocone on F₁ with apex A is a colimit cocone.

• ι₂ : self.F₂.comp yoneda ⟶ (Functor.const self.I).obj B

  The cocone on F₂ with apex B.

• isColimit₂ : Limits.IsColimit { pt := B, ι := self.ι₂ }

  The cocone on F₂ with apex B is a colimit cocone.

• φ : self.F₁ ⟶ self.F₂

  The natural transformation presenting f.

• ψ : self.F₁ ⟶ self.F₂

  The natural transformation presenting g.

• hf : f = self.isColimit₁.map { pt := B, ι := self.ι₂ } (Functor.whiskerRight self.φ yoneda)

  f is in fact presented by φ.

• hg : g = self.isColimit₁.map { pt := B, ι := self.ι₂ } (Functor.whiskerRight self.ψ yoneda)

  g is in fact presented by ψ.

@[implicit_reducible]

instance CategoryTheory.instSmallCategoryI {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B} (P : IndParallelPairPresentation f g) : SmallCategory P.I

instance CategoryTheory.instIsFilteredI {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B} (P : IndParallelPairPresentation f g) : IsFiltered P.I

@[reducible, inline]

abbrev CategoryTheory.NonemptyParallelPairPresentationAux.K {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : Type v₁

Implementation; see nonempty_indParallelPairPresentation.

@[reducible, inline]

abbrev CategoryTheory.NonemptyParallelPairPresentationAux.F₁ {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : Functor (K f g P₁ P₂) C

Implementation; see nonempty_indParallelPairPresentation.

@[reducible, inline]

abbrev CategoryTheory.NonemptyParallelPairPresentationAux.F₂ {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : Functor (K f g P₁ P₂) C

Implementation; see nonempty_indParallelPairPresentation.

@[reducible, inline]

abbrev CategoryTheory.NonemptyParallelPairPresentationAux.ι₁ {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : (F₁ f g P₁ P₂).comp yoneda ⟶ (Functor.const (K f g P₁ P₂)).obj A

Implementation; see nonempty_indParallelPairPresentation.

@[reducible, inline]

noncomputable abbrev CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁ {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : Limits.IsColimit { pt := A, ι := ι₁ f g P₁ P₂ }

Implementation; see nonempty_indParallelPairPresentation.

@[reducible, inline]

abbrev CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : (F₂ f g P₁ P₂).comp yoneda ⟶ (Functor.const (K f g P₁ P₂)).obj B

Implementation; see nonempty_indParallelPairPresentation.

@[reducible, inline]

noncomputable abbrev CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₂ {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : Limits.IsColimit { pt := B, ι := ι₂ f g P₁ P₂ }

Implementation; see nonempty_indParallelPairPresentation.

def CategoryTheory.NonemptyParallelPairPresentationAux.ϕ {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : F₁ f g P₁ P₂ ⟶ F₂ f g P₁ P₂

Implementation; see nonempty_indParallelPairPresentation.

theorem CategoryTheory.NonemptyParallelPairPresentationAux.hf {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : f = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (Functor.whiskerRight (ϕ f g P₁ P₂) yoneda)

def CategoryTheory.NonemptyParallelPairPresentationAux.ψ {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : F₁ f g P₁ P₂ ⟶ F₂ f g P₁ P₂

Implementation; see nonempty_indParallelPairPresentation.

theorem CategoryTheory.NonemptyParallelPairPresentationAux.hg {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : g = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (Functor.whiskerRight (ψ f g P₁ P₂) yoneda)

noncomputable def CategoryTheory.NonemptyParallelPairPresentationAux.presentation {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : Limits.IndObjectPresentation A) (P₂ : Limits.IndObjectPresentation B) : IndParallelPairPresentation f g

Implementation; see nonempty_indParallelPairPresentation.

theorem CategoryTheory.nonempty_indParallelPairPresentation {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} (hA : Limits.IsIndObject A) (hB : Limits.IsIndObject B) (f g : A ⟶ B) : Nonempty (IndParallelPairPresentation f g)

noncomputable def CategoryTheory.IndParallelPairPresentation.parallelPairIsoParallelPairCompYoneda {C : Type u₁} [Category.{v₁, u₁} C] {A B : Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B} (P : IndParallelPairPresentation f g) : Limits.parallelPair f g ≅ (Limits.parallelPair P.φ P.ψ).comp (((Functor.whiskeringRight P.I C (Functor Cᵒᵖ (Type v₁))).obj yoneda).comp Limits.colim)

Given an IndParallelPairPresentation f g, we can understand the parallel pair (f, g) as the colimit of (P.φ, P.ψ) in Cᵒᵖ ⥤ Type v.