κ-filtered categories and κ-directed poset

In this file, we formalize the proof by Deligne (SGA 4 I 8.1.6) that for any (small) filtered category J, there exists a final functor F : α ⥤ J where α is a directed partially ordered set (IsFiltered.exists_directed). The construction applies more generally to κ-filtered categories and κ-directed posets (IsCardinalFiltered.exists_cardinal_directed).

Note: the argument by Deligne is reproduced (without reference) in the book by Adámek and Rosický (theorem 1.5), but with a mistake: the construction by Deligne involves considering diagrams (see CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal) which are not necessarily subcategories (the class of morphisms W does not have to be multiplicative.)

References

• Alexander Grothendieck and Jean-Louis Verdier, Exposé I : Préfaisceaux, SGA 4 I 8.1.6
• Adámek, J. and Rosický, J., Locally presentable and accessible categories

Let J be a κ-filtered category. In order to construct a cofinal functor α ⥤ J with a κ-directed poset α, we first consider the case where there is no object m : J such that for any object j : J, there exists a map j ⟶ m. Under this assumption (hJ), the partially ordered type DiagramWithUniqueTerminal J κ of κ-bounded diagrams with a unique terminal object in J shall be a possible choice for α.

structure CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) : Type w

If κ is a cardinal, this structure contains the data of a κ-bounded diagram in a category J.

• W : MorphismProperty J

  the morphisms which belong to the diagram

• P : ObjectProperty J

  the objects in the diagram

• src {i j : J} {f : i ⟶ j} : self.W f → self.P i
• tgt {i j : J} {f : i ⟶ j} : self.W f → self.P j
• hW : self.W.HasCardinalLT κ
• hP : self.P.HasCardinalLT κ

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.ext_iff {J : Type w} {inst✝ : SmallCategory J} {κ : Cardinal.{w}} {x y : Diagram J κ} : x = y ↔ x.W = y.W ∧ x.P = y.P

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.ext {J : Type w} {inst✝ : SmallCategory J} {κ : Cardinal.{w}} {x y : Diagram J κ} (W : x.W = y.W) (P : x.P = y.P) : x = y

structure CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} (D : Diagram J κ) (e : J) : Type w

Given a κ-bounded diagram D in a category J, an object e : J is terminal if 𝟙 e belongs to D and for any object j of D, there is a unique morphism j ⟶ e in D, such that these unique morphisms are compatible with precomposition with morphisms in D.

• prop_id : D.W (CategoryStruct.id e)
• lift {j : J} (hj : D.P j) : j ⟶ e

  the unique map to the terminal object in the diagram

• hlift {j : J} (hj : D.P j) : D.W (self.lift hj)
• uniq {j : J} (hj : D.P j) {φ : j ⟶ e} (hφ : D.W φ) : self.lift hj = φ
• comm {i j : J} (f : i ⟶ j) (hf : D.W f) : CategoryStruct.comp f (self.lift ⋯) = self.lift ⋯

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.comm_assoc {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D : Diagram J κ} {e : J} (self : D.IsTerminal e) {i j : J} (f : i ⟶ j) (hf : D.W f) {Z : J} (h : e ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (self.lift ⋯) h) = CategoryStruct.comp (self.lift ⋯) h

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.prop {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D : Diagram J κ} {e : J} (h : D.IsTerminal e) : D.P e

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.lift_self {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D : Diagram J κ} {e : J} (h : D.IsTerminal e) : h.lift ⋯ = CategoryStruct.id e

instance CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.instSubsingleton {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D : Diagram J κ} {e : J} : Subsingleton (D.IsTerminal e)

noncomputable def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.ofExistsUnique {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D : Diagram J κ} {e : J} (prop_id : D.W (CategoryStruct.id e)) (h₁ : ∀ ⦃j : J⦄, D.P j → ∃ (lift : j ⟶ e), D.W lift) (h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂) (h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ (li : i ⟶ e) (lj : j ⟶ e), D.W li ∧ D.W lj ∧ CategoryStruct.comp f lj = li) : D.IsTerminal e

Constructor for Diagram.IsTerminal for which no data is provided, but only its existence.

Equations

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

structure CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) extends CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ : Type w

If κ is a cardinal, this structure contains the data of a κ-bounded diagram with a unique terminal object in a category J.

• W : MorphismProperty J
• P : ObjectProperty J
• src {i j : J} {f : i ⟶ j} : self.W f → self.P i
• tgt {i j : J} {f : i ⟶ j} : self.W f → self.P j
• hW : self.W.HasCardinalLT κ
• hP : self.P.HasCardinalLT κ
• top : J

  the terminal object

• isTerminal : self.IsTerminal self.top

  top is terminal

• uniq_terminal (j : J) (hj : self.IsTerminal j) : j = self.top

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.ext (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) {D₁ D₂ : DiagramWithUniqueTerminal J κ} (hW : D₁.W = D₂.W) (hP : D₁.P = D₂.P) : D₁ = D₂

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.ext_iff {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D₁ D₂ : DiagramWithUniqueTerminal J κ} : D₁ = D₂ ↔ D₁.W = D₂.W ∧ D₁.P = D₂.P

instance CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.instPartialOrderDiagramWithUniqueTerminal (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) : PartialOrder (DiagramWithUniqueTerminal J κ)

Equations

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

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D₁ D₂ : DiagramWithUniqueTerminal J κ} (h : D₁ ≤ D₂) : D₁.top ⟶ D₂.top

Auxiliary definition for functor.

Equations

• CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap h = D₂.isTerminal.lift ⋯

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_id {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} (D : DiagramWithUniqueTerminal J κ) : functorMap ⋯ = CategoryStruct.id D.top

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_comp {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D₁ D₂ D₃ : DiagramWithUniqueTerminal J κ} (h₁₂ : D₁ ≤ D₂) (h₂₃ : D₂ ≤ D₃) : CategoryStruct.comp (functorMap h₁₂) (functorMap h₂₃) = functorMap ⋯

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_comp_assoc {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} {D₁ D₂ D₃ : DiagramWithUniqueTerminal J κ} (h₁₂ : D₁ ≤ D₂) (h₂₃ : D₂ ≤ D₃) {Z : J} (h : D₃.top ⟶ Z) : CategoryStruct.comp (functorMap h₁₂) (CategoryStruct.comp (functorMap h₂₃) h) = CategoryStruct.comp (functorMap ⋯) h

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) : Functor (DiagramWithUniqueTerminal J κ) J

The functor which sends a κ-bounded diagram with a unique terminal object to its terminal object.

Equations

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

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor_obj (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) (D : DiagramWithUniqueTerminal J κ) : (functor J κ).obj D = D.top

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor_map (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) {X✝ Y✝ : DiagramWithUniqueTerminal J κ} (h : X✝ ⟶ Y✝) : (functor J κ).map h = functorMap ⋯

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (j : J) : Diagram J κ

The diagram containing a single object (and its identity morphism).

Equations

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

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single_W {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (j : J) : (single j).W = MorphismProperty.ofHoms fun (x : Unit) => CategoryStruct.id j

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single_P {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (j a✝ : J) : (single j).P a✝ = ObjectProperty.ofObj (fun (x : Unit) => j) a✝

instance CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.instFiniteSubtypePSingle (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) [Fact κ.IsRegular] (j : J) : Finite (Subtype (Diagram.single j).P)

noncomputable def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.single {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (j : J) : DiagramWithUniqueTerminal J κ

The diagram with a unique terminal object containing a single object (and its identity morphism).

Equations

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

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type u_1} (D : ι → Diagram J κ) (hι : HasCardinalLT ι κ) : Diagram J κ

The union of a κ-bounded family of κ-bounded diagrams.

Equations

• CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup D hι = { W := ⨆ (i : ι), (D i).W, P := ⨆ (i : ι), (D i).P, src := ⋯, tgt := ⋯, hW := ⋯, hP := ⋯ }

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_W {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type u_1} (D : ι → Diagram J κ) (hι : HasCardinalLT ι κ) : (iSup D hι).W = ⨆ (i : ι), (D i).W

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_P {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type u_1} (D : ι → Diagram J κ) (hι : HasCardinalLT ι κ) (a✝ : J) : (iSup D hι).P a✝ = (⨆ (i : ι), (D i).P) a✝

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D₁ D₂ : Diagram J κ) : Diagram J κ

The union of two κ-bounded diagrams.

Equations

• D₁.sup D₂ = { W := D₁.W ⊔ D₂.W, P := D₁.P ⊔ D₂.P, src := ⋯, tgt := ⋯, hW := ⋯, hP := ⋯ }

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_P {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D₁ D₂ : Diagram J κ) (a✝ : J) : (D₁.sup D₂).P a✝ = Max.max D₁.P D₂.P a✝

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_W {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D₁ D₂ : Diagram J κ) : (D₁.sup D₂).W = D₁.W ⊔ D₂.W

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J κ] (hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty (m ⟶ e)) {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) : ∃ (m : J) (u : (i : ι) → (D i).top ⟶ m), (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧ ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j), CategoryStruct.comp ((D i₁).isTerminal.lift hj₁) (u i₁) = CategoryStruct.comp ((D i₂).isTerminal.lift hj₂) (u i₂)

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁ {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) (m : J) : Diagram J κ

Auxiliary definition for isCardinalFiltered.

Equations

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

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) (m : J) : (D₁ D hι m).W = (⨆ (i : ι), (D i).W) ⊔ MorphismProperty.ofHoms fun (x : Unit) => CategoryStruct.id m

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_P {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) (m a✝ : J) : (D₁ D hι m).P a✝ = ((∃ (a : ι), (D a).P a✝) ∨ m = a✝)

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂ {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) {m : J} (u : (i : ι) → (D i).top ⟶ m) : Diagram J κ

Auxiliary definition for isCardinalFiltered.

Equations

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

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_P {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) {m : J} (u : (i : ι) → (D i).top ⟶ m) (a✝ : J) : (D₂ D hι u).P a✝ = ((∃ (a : ι), (D a).P a✝) ∨ m = a✝)

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) {m : J} (u : (i : ι) → (D i).top ⟶ m) : (D₂ D hι u).W = ((⨆ (i : ι), (D i).W) ⊔ MorphismProperty.ofHoms fun (x : Unit) => CategoryStruct.id m) ⊔ MorphismProperty.ofHoms fun (x : (i : ι) × Subtype (D i).P) => CategoryStruct.comp ((D x.fst).isTerminal.lift ⋯) (u x.fst)

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.eq_id_of_D₂_W {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) {m : J} (u : (i : ι) → (D i).top ⟶ m) (hD : ∀ {i : ι}, ¬(D i).P m) {f : m ⟶ m} (hf : (D₂ D hι u).W f) : f = CategoryStruct.id m

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J κ] (hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty (m ⟶ e)) : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃ {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D : DiagramWithUniqueTerminal J κ) (m₁ : J) : Diagram J κ

Auxiliary definition for final_functor.

Equations

• CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃ D m₁ = D.sup (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single m₁)

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_P {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D : DiagramWithUniqueTerminal J κ) (m₁ a✝ : J) : (D₃ D m₁).P a✝ = (D.P a✝ ∨ m₁ = a✝)

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_W {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D : DiagramWithUniqueTerminal J κ) (m₁ : J) : (D₃ D m₁).W = D.W ⊔ MorphismProperty.ofHoms fun (x : Unit) => CategoryStruct.id m₁

def CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄ {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D : DiagramWithUniqueTerminal J κ) {m₁ : J} (φ : (x : Subtype D.P) → ↑x ⟶ m₁) : Diagram J κ

Auxiliary definition for final_functor.

Equations

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

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_P {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D : DiagramWithUniqueTerminal J κ) {m₁ : J} (φ : (x : Subtype D.P) → ↑x ⟶ m₁) (a✝ : J) : (D₄ D φ).P a✝ = (D.P a✝ ∨ m₁ = a✝)

@[simp]

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (D : DiagramWithUniqueTerminal J κ) {m₁ : J} (φ : (x : Subtype D.P) → ↑x ⟶ m₁) : (D₄ D φ).W = (D.W ⊔ MorphismProperty.ofHoms fun (x : Unit) => CategoryStruct.id m₁) ⊔ MorphismProperty.ofHoms φ

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.final_functor (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J κ] (hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty (m ⟶ e)) : (functor J κ).Final

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.aux (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J κ] (hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty (m ⟶ e)) : ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : Functor α J), F.Final

The previous lemma IsCardinalFiltered.exists_cardinal_directed.aux is the particular case of the main lemma IsCardinalFiltered.exists_cardinal_directed below in the particular case the κ-filtered category J has no object m : J such that for any object j : J, there exists a map j ⟶ m.

The general case is obtained by applying the previous result to the cartesian product J × κ.ord.toType.

theorem CategoryTheory.IsCardinalFiltered.exists_cardinal_directed (J : Type w) [SmallCategory J] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J κ] : ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : Functor α J), F.Final

Stacks Tag 0032

theorem CategoryTheory.IsFiltered.exists_directed (J : Type w) [SmallCategory J] [IsFiltered J] : ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) => x1 ≤ x2) (_ : Nonempty α) (F : Functor α J), F.Final

Stacks Tag 0032