κ-filtered categories and κ-directed poset

In this file, we shall 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 (TODO). The construction applies more generally to κ-filtered categories and κ-directed posets (TODO).

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][sga-4-tome-1]
• Adámek, J. and Rosický, J., Locally presentable and accessible categories

Let J is 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 belongs 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_P {J : Type w} [SmallCategory J] {κ : Cardinal.{w}} [Fact κ.IsRegular] (j a✝ : J) : (single j).P a✝ = ObjectProperty.ofObj (fun (x : Unit) => j) a✝

@[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

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