mathlib3 documentation

category_theory.filtered

Filtered categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A category is filtered if every finite diagram admits a cocone. We give a simple characterisation of this condition as

  1. for every pair of objects there exists another object "to the right",
  2. for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal, and
  3. there exists some object.

Filtered colimits are often better behaved than arbitrary colimits. See category_theory/limits/types for some details.

Filtered categories are nice because colimits indexed by filtered categories tend to be easier to describe than general colimits (and more often preserved by functors).

In this file we show that any functor from a finite category to a filtered category admits a cocone:

Furthermore, we give special support for two diagram categories: The bowtie and the tulip. This is because these shapes show up in the proofs that forgetful functors of algebraic categories (e.g. Mon, CommRing, ...) preserve filtered colimits.

All of the above API, except for the bowtie and the tulip, is also provided for cofiltered categories.

See also #

In category_theory.limits.filtered_colimit_commutes_finite_limit we show that filtered colimits commute with finite limits.

source
@[class]
structure category_theory.is_filtered_or_empty (C : Type u) [category_theory.category C] :
Prop

A category is_filtered_or_empty if

  1. for every pair of objects there exists another object "to the right", and
  2. for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal.
Instances of this typeclass
source
@[class]
structure category_theory.is_filtered (C : Type u) [category_theory.category C] :
Prop

A category is_filtered if

  1. for every pair of objects there exists another object "to the right",
  2. for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal, and
  3. there exists some object.

See https://stacks.math.columbia.edu/tag/002V. (They also define a diagram being filtered.)

Instances of this typeclass
source
@[protected, instance]
def category_theory.is_filtered_or_empty_of_semilattice_sup (α : Type u) [semilattice_sup α] :
category_theory.is_filtered_or_empty α
source
@[protected, instance]
def category_theory.is_filtered_of_semilattice_sup_nonempty (α : Type u) [semilattice_sup α] [nonempty α] :
category_theory.is_filtered α
source
@[protected, instance]
def category_theory.is_filtered_or_empty_of_directed_le (α : Type u) [preorder α] [is_directed α has_le.le] :
category_theory.is_filtered_or_empty α
source
@[protected, instance]
def category_theory.is_filtered_of_directed_le_nonempty (α : Type u) [preorder α] [is_directed α has_le.le] [nonempty α] :
category_theory.is_filtered α
source
@[protected, instance]
def category_theory.discrete.is_filtered  :
category_theory.is_filtered (category_theory.discrete punit)
source
theorem category_theory.is_filtered.cocone_objs {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] (X Y : C) :
∃ (Z : C) (f : X ⟶ Z) (g : Y ⟶ Z), true
source
theorem category_theory.is_filtered.cocone_maps {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] ⦃X Y : C⦄ (f g : X ⟶ Y) :
∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h
source
noncomputable def category_theory.is_filtered.max {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] (j j' : C) :
C

max j j' is an arbitrary choice of object to the right of both j and j', whose existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.left_to_max {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] (j j' : C) :
j ⟶ category_theory.is_filtered.max j j'

left_to_max j j' is an arbitrary choice of morphism from j to max j j', whose existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.right_to_max {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] (j j' : C) :
j' ⟶ category_theory.is_filtered.max j j'

right_to_max j j' is an arbitrary choice of morphism from j' to max j j', whose existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.coeq {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j j' : C} (f f' : j ⟶ j') :
C

coeq f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of object which admits a morphism coeq_hom f f' : j' ⟶ coeq f f' such that coeq_condition : f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'. Its existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.coeq_hom {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j j' : C} (f f' : j ⟶ j') :
j' ⟶ category_theory.is_filtered.coeq f f'

coeq_hom f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of morphism coeq_hom f f' : j' ⟶ coeq f f' such that coeq_condition : f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'. Its existence is ensured by is_filtered.

Equations
source
@[simp]
theorem category_theory.is_filtered.coeq_condition {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j j' : C} (f f' : j ⟶ j') :
f ≫ category_theory.is_filtered.coeq_hom f f' = f' ≫ category_theory.is_filtered.coeq_hom f f'

coeq_condition f f', for morphisms f f' : j ⟶ j', is the proof that f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'.

source
@[simp]
theorem category_theory.is_filtered.coeq_condition_assoc {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j j' : C} (f f' : j ⟶ j') {X' : C} (f'_1 : category_theory.is_filtered.coeq f f' ⟶ X') :
f ≫ category_theory.is_filtered.coeq_hom f f' ≫ f'_1 = f' ≫ category_theory.is_filtered.coeq_hom f f' ≫ f'_1
source
theorem category_theory.is_filtered.sup_objs_exists {C : Type u} [category_theory.category C] [category_theory.is_filtered C] (O : finset C) :
∃ (S : C), ∀ {X : C}, X ∈ O → nonempty (X ⟶ S)

Any finite collection of objects in a filtered category has an object "to the right".

source
theorem category_theory.is_filtered.sup_exists {C : Type u} [category_theory.category C] [category_theory.is_filtered C] (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) :
∃ (S : C) (T : Π {X : C}, X ∈ O → (X ⟶ S)), ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ T mY = T mX

Given any finset of objects {X, ...} and indexed collection of finsets of morphisms {f, ...} in C, there exists an object S, with a morphism T X : X ⟶ S from each X, such that the triangles commute: f ≫ T Y = T X, for f : X ⟶ Y in the finset.

source
noncomputable def category_theory.is_filtered.sup {C : Type u} [category_theory.category C] [category_theory.is_filtered C] (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) :
C

An arbitrary choice of object "to the right" of a finite collection of objects O and morphisms H, making all the triangles commute.

Equations
source
noncomputable def category_theory.is_filtered.to_sup {C : Type u} [category_theory.category C] [category_theory.is_filtered C] (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) {X : C} (m : X ∈ O) :
X ⟶ category_theory.is_filtered.sup O H

The morphisms to sup O H.

Equations
source
theorem category_theory.is_filtered.to_sup_commutes {C : Type u} [category_theory.category C] [category_theory.is_filtered C] (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y} (mf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H) :
f ≫ category_theory.is_filtered.to_sup O H mY = category_theory.is_filtered.to_sup O H mX

The triangles of consisting of a morphism in H and the maps to sup O H commute.

source
theorem category_theory.is_filtered.cocone_nonempty {C : Type u} [category_theory.category C] [category_theory.is_filtered C] {J : Type v} [category_theory.small_category J] [category_theory.fin_category J] (F : J ⥤ C) :
nonempty (category_theory.limits.cocone F)

If we have is_filtered C, then for any functor F : J ⥤ C with fin_category J, there exists a cocone over F.

source
noncomputable def category_theory.is_filtered.cocone {C : Type u} [category_theory.category C] [category_theory.is_filtered C] {J : Type v} [category_theory.small_category J] [category_theory.fin_category J] (F : J ⥤ C) :
category_theory.limits.cocone F

An arbitrary choice of cocone over F : J ⥤ C, for fin_category J and is_filtered C.

Equations
source
theorem category_theory.is_filtered.of_right_adjoint {C : Type u} [category_theory.category C] [category_theory.is_filtered C] {D : Type u₁} [category_theory.category D] {L : D ⥤ C} {R : C ⥤ D} (h : L ⊣ R) :
category_theory.is_filtered D

If C is filtered, and we have a functor R : C ⥤ D with a left adjoint, then D is filtered.

source
theorem category_theory.is_filtered.of_is_right_adjoint {C : Type u} [category_theory.category C] [category_theory.is_filtered C] {D : Type u₁} [category_theory.category D] (R : C ⥤ D) [category_theory.is_right_adjoint R] :
category_theory.is_filtered D

If C is filtered, and we have a right adjoint functor R : C ⥤ D, then D is filtered.

source
theorem category_theory.is_filtered.of_equivalence {C : Type u} [category_theory.category C] [category_theory.is_filtered C] {D : Type u₁} [category_theory.category D] (h : C ≌ D) :
category_theory.is_filtered D

Being filtered is preserved by equivalence of categories.

source
noncomputable def category_theory.is_filtered.max₃ {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] (j₁ j₂ j₃ : C) :
C

max₃ j₁ j₂ j₃ is an arbitrary choice of object to the right of j₁, j₂ and j₃, whose existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.first_to_max₃ {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] (j₁ j₂ j₃ : C) :
j₁ ⟶ category_theory.is_filtered.max₃ j₁ j₂ j₃

first_to_max₃ j₁ j₂ j₃ is an arbitrary choice of morphism from j₁ to max₃ j₁ j₂ j₃, whose existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.second_to_max₃ {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] (j₁ j₂ j₃ : C) :
j₂ ⟶ category_theory.is_filtered.max₃ j₁ j₂ j₃

second_to_max₃ j₁ j₂ j₃ is an arbitrary choice of morphism from j₂ to max₃ j₁ j₂ j₃, whose existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.third_to_max₃ {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] (j₁ j₂ j₃ : C) :
j₃ ⟶ category_theory.is_filtered.max₃ j₁ j₂ j₃

third_to_max₃ j₁ j₂ j₃ is an arbitrary choice of morphism from j₃ to max₃ j₁ j₂ j₃, whose existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.coeq₃ {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) :
C

coeq₃ f g h, for morphisms f g h : j₁ ⟶ j₂, is an arbitrary choice of object which admits a morphism coeq₃_hom f g h : j₂ ⟶ coeq₃ f g h such that coeq₃_condition₁, coeq₃_condition₂ and coeq₃_condition₃ are satisfied. Its existence is ensured by is_filtered.

Equations
source
noncomputable def category_theory.is_filtered.coeq₃_hom {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) :
j₂ ⟶ category_theory.is_filtered.coeq₃ f g h

coeq₃_hom f g h, for morphisms f g h : j₁ ⟶ j₂, is an arbitrary choice of morphism j₂ ⟶ coeq₃ f g h such that coeq₃_condition₁, coeq₃_condition₂ and coeq₃_condition₃ are satisfied. Its existence is ensured by is_filtered.

Equations
source
theorem category_theory.is_filtered.coeq₃_condition₁ {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) :
f ≫ category_theory.is_filtered.coeq₃_hom f g h = g ≫ category_theory.is_filtered.coeq₃_hom f g h
source
theorem category_theory.is_filtered.coeq₃_condition₂ {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) :
g ≫ category_theory.is_filtered.coeq₃_hom f g h = h ≫ category_theory.is_filtered.coeq₃_hom f g h
source
theorem category_theory.is_filtered.coeq₃_condition₃ {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) :
f ≫ category_theory.is_filtered.coeq₃_hom f g h = h ≫ category_theory.is_filtered.coeq₃_hom f g h
source
theorem category_theory.is_filtered.span {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {i j j' : C} (f : i ⟶ j) (f' : i ⟶ j') :
∃ (k : C) (g : j ⟶ k) (g' : j' ⟶ k), f ≫ g = f' ≫ g'

For every span j ⟵ i ⟶ j', there exists a cocone j ⟶ k ⟵ j' such that the square commutes.

source
theorem category_theory.is_filtered.bowtie {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j₁ j₂ k₁ k₂ : C} (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂) :
∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Given a "bowtie" of morphisms

 j₁   j₂
 |\  /|
 | \/ |
 | /\ |
 |/  \∣
 vv  vv
 k₁  k₂

in a filtered category, we can construct an object s and two morphisms from k₁ and k₂ to s, making the resulting squares commute.

source
theorem category_theory.is_filtered.tulip {C : Type u} [category_theory.category C] [category_theory.is_filtered_or_empty C] {j₁ j₂ j₃ k₁ k₂ l : C} (f₁ : j₁ ⟶ k₁) (f₂ : j₂ ⟶ k₁) (f₃ : j₂ ⟶ k₂) (f₄ : j₃ ⟶ k₂) (g₁ : j₁ ⟶ l) (g₂ : j₃ ⟶ l) :
∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Given a "tulip" of morphisms

 j₁    j₂    j₃
 |\   / \   / |
 | \ /   \ /  |
 |  vv    vv  |
 \  k₁    k₂ /
  \         /
   \       /
    \     /
     \   /
      v v
       l

in a filtered category, we can construct an object s and three morphisms from k₁, k₂ and l to s, making the resulting squares commute.

source
@[class]
structure category_theory.is_cofiltered_or_empty (C : Type u) [category_theory.category C] :
Prop

A category is_cofiltered_or_empty if

  1. for every pair of objects there exists another object "to the left", and
  2. for every pair of parallel morphisms there exists a morphism to the left so the compositions are equal.
Instances of this typeclass
source
@[class]
structure category_theory.is_cofiltered (C : Type u) [category_theory.category C] :
Prop

A category is_cofiltered if

  1. for every pair of objects there exists another object "to the left",
  2. for every pair of parallel morphisms there exists a morphism to the left so the compositions are equal, and
  3. there exists some object.

See https://stacks.math.columbia.edu/tag/04AZ.

Instances of this typeclass
source
@[protected, instance]
def category_theory.is_cofiltered_or_empty_of_semilattice_inf (α : Type u) [semilattice_inf α] :
category_theory.is_cofiltered_or_empty α
source
@[protected, instance]
def category_theory.is_cofiltered_of_semilattice_inf_nonempty (α : Type u) [semilattice_inf α] [nonempty α] :
category_theory.is_cofiltered α
source
@[protected, instance]
def category_theory.is_cofiltered_or_empty_of_directed_ge (α : Type u) [preorder α] [is_directed α ge] :
category_theory.is_cofiltered_or_empty α
source
@[protected, instance]
def category_theory.is_cofiltered_of_directed_ge_nonempty (α : Type u) [preorder α] [is_directed α ge] [nonempty α] :
category_theory.is_cofiltered α
source
@[protected, instance]
def category_theory.discrete.is_cofiltered  :
category_theory.is_cofiltered (category_theory.discrete punit)
source
theorem category_theory.is_cofiltered.cone_objs {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] (X Y : C) :
∃ (W : C) (f : W ⟶ X) (g : W ⟶ Y), true
source
theorem category_theory.is_cofiltered.cone_maps {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] ⦃X Y : C⦄ (f g : X ⟶ Y) :
∃ (W : C) (h : W ⟶ X), h ≫ f = h ≫ g
source
noncomputable def category_theory.is_cofiltered.min {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] (j j' : C) :
C

min j j' is an arbitrary choice of object to the left of both j and j', whose existence is ensured by is_cofiltered.

Equations
source
noncomputable def category_theory.is_cofiltered.min_to_left {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] (j j' : C) :
category_theory.is_cofiltered.min j j' ⟶ j

min_to_left j j' is an arbitrary choice of morphism from min j j' to j, whose existence is ensured by is_cofiltered.

Equations
source
noncomputable def category_theory.is_cofiltered.min_to_right {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] (j j' : C) :
category_theory.is_cofiltered.min j j' ⟶ j'

min_to_right j j' is an arbitrary choice of morphism from min j j' to j', whose existence is ensured by is_cofiltered.

Equations
source
noncomputable def category_theory.is_cofiltered.eq {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] {j j' : C} (f f' : j ⟶ j') :
C

eq f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of object which admits a morphism eq_hom f f' : eq f f' ⟶ j such that eq_condition : eq_hom f f' ≫ f = eq_hom f f' ≫ f'. Its existence is ensured by is_cofiltered.

Equations
source
noncomputable def category_theory.is_cofiltered.eq_hom {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] {j j' : C} (f f' : j ⟶ j') :
category_theory.is_cofiltered.eq f f' ⟶ j

eq_hom f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of morphism eq_hom f f' : eq f f' ⟶ j such that eq_condition : eq_hom f f' ≫ f = eq_hom f f' ≫ f'. Its existence is ensured by is_cofiltered.

Equations
source
@[simp]
theorem category_theory.is_cofiltered.eq_condition_assoc {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] {j j' : C} (f f' : j ⟶ j') {X' : C} (f'_1 : j' ⟶ X') :
category_theory.is_cofiltered.eq_hom f f' ≫ f ≫ f'_1 = category_theory.is_cofiltered.eq_hom f f' ≫ f' ≫ f'_1
source
@[simp]
theorem category_theory.is_cofiltered.eq_condition {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] {j j' : C} (f f' : j ⟶ j') :
category_theory.is_cofiltered.eq_hom f f' ≫ f = category_theory.is_cofiltered.eq_hom f f' ≫ f'

eq_condition f f', for morphisms f f' : j ⟶ j', is the proof that eq_hom f f' ≫ f = eq_hom f f' ≫ f'.

source
theorem category_theory.is_cofiltered.cospan {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] {i j j' : C} (f : j ⟶ i) (f' : j' ⟶ i) :
∃ (k : C) (g : k ⟶ j) (g' : k ⟶ j'), g ≫ f = g' ≫ f'

For every cospan j ⟶ i ⟵ j', there exists a cone j ⟵ k ⟶ j' such that the square commutes.

source
theorem category_theory.functor.ranges_directed {C : Type u} [category_theory.category C] [category_theory.is_cofiltered_or_empty C] (F : C ⥤ Type u_1) (j : C) :
directed superset (λ (f : Σ' (i : C), i ⟶ j), set.range (F.map f.snd))
source
theorem category_theory.is_cofiltered.inf_objs_exists {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] (O : finset C) :
∃ (S : C), ∀ {X : C}, X ∈ O → nonempty (S ⟶ X)

Any finite collection of objects in a cofiltered category has an object "to the left".

source
theorem category_theory.is_cofiltered.inf_exists {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) :
∃ (S : C) (T : Π {X : C}, X ∈ O → (S ⟶ X)), ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → T mX ≫ f = T mY

Given any finset of objects {X, ...} and indexed collection of finsets of morphisms {f, ...} in C, there exists an object S, with a morphism T X : S ⟶ X from each X, such that the triangles commute: T X ≫ f = T Y, for f : X ⟶ Y in the finset.

source
noncomputable def category_theory.is_cofiltered.inf {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) :
C

An arbitrary choice of object "to the left" of a finite collection of objects O and morphisms H, making all the triangles commute.

Equations
source
noncomputable def category_theory.is_cofiltered.inf_to {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) {X : C} (m : X ∈ O) :
category_theory.is_cofiltered.inf O H ⟶ X

The morphisms from inf O H.

Equations
source
theorem category_theory.is_cofiltered.inf_to_commutes {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] (O : finset C) (H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y)) {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y} (mf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H) :
category_theory.is_cofiltered.inf_to O H mX ≫ f = category_theory.is_cofiltered.inf_to O H mY

The triangles consisting of a morphism in H and the maps from inf O H commute.

source
theorem category_theory.is_cofiltered.cone_nonempty {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] {J : Type w} [category_theory.small_category J] [category_theory.fin_category J] (F : J ⥤ C) :
nonempty (category_theory.limits.cone F)

If we have is_cofiltered C, then for any functor F : J ⥤ C with fin_category J, there exists a cone over F.

source
noncomputable def category_theory.is_cofiltered.cone {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] {J : Type w} [category_theory.small_category J] [category_theory.fin_category J] (F : J ⥤ C) :
category_theory.limits.cone F

An arbitrary choice of cone over F : J ⥤ C, for fin_category J and is_cofiltered C.

Equations
source
theorem category_theory.is_cofiltered.of_left_adjoint {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] {D : Type u₁} [category_theory.category D] {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R) :
category_theory.is_cofiltered D

If C is cofiltered, and we have a functor L : C ⥤ D with a right adjoint, then D is cofiltered.

source
theorem category_theory.is_cofiltered.of_is_left_adjoint {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] {D : Type u₁} [category_theory.category D] (L : C ⥤ D) [category_theory.is_left_adjoint L] :
category_theory.is_cofiltered D

If C is cofiltered, and we have a left adjoint functor L : C ⥤ D, then D is cofiltered.

source
theorem category_theory.is_cofiltered.of_equivalence {C : Type u} [category_theory.category C] [category_theory.is_cofiltered C] {D : Type u₁} [category_theory.category D] (h : C ≌ D) :
category_theory.is_cofiltered D

Being cofiltered is preserved by equivalence of categories.

source
@[protected, instance]
def category_theory.is_cofiltered_op_of_is_filtered (C : Type u) [category_theory.category C] [category_theory.is_filtered C] :
category_theory.is_cofiltered Cᵒᵖ
source
@[protected, instance]
def category_theory.is_filtered_op_of_is_cofiltered (C : Type u) [category_theory.category C] [category_theory.is_cofiltered C] :
category_theory.is_filtered Cᵒᵖ
source
@[protected, instance]
def category_theory.ulift.is_filtered (C : Type u) [category_theory.category C] [category_theory.is_filtered C] :
category_theory.is_filtered (ulift C)
source
@[protected, instance]
def category_theory.ulift.is_cofiltered (C : Type u) [category_theory.category C] [category_theory.is_cofiltered C] :
category_theory.is_cofiltered (ulift C)
source
@[protected, instance]
def category_theory.ulift_hom.is_filtered (C : Type u) [category_theory.category C] [category_theory.is_filtered C] :
category_theory.is_filtered (category_theory.ulift_hom C)
source
@[protected, instance]
def category_theory.ulift_hom.is_cofiltered (C : Type u) [category_theory.category C] [category_theory.is_cofiltered C] :
category_theory.is_cofiltered (category_theory.ulift_hom C)
source
@[protected, instance]
def category_theory.as_small.is_filtered (C : Type u) [category_theory.category C] [category_theory.is_filtered C] :
category_theory.is_filtered (category_theory.as_small C)
source
@[protected, instance]
def category_theory.as_small.is_cofiltered (C : Type u) [category_theory.category C] [category_theory.is_cofiltered C] :
category_theory.is_cofiltered (category_theory.as_small C)