CategoryTheory.IsCofilteredOrEmpty.of_equivalence
theorem CategoryTheory.IsCofilteredOrEmpty.of_equivalence :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C]
{D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D], (C ≌ D) → CategoryTheory.IsCofilteredOrEmpty D
This theorem states that, in the context of category theory, if a category `C` is either cofiltered or empty, and there exists an equivalence of categories between `C` and another category `D`, then `D` is also either cofiltered or empty. This property of being cofiltered or empty is preserved under equivalence of categories.
More concisely: If categories `C` and `D` are equivalent, and `C` is cofiltered or empty, then so is `D`.
|
CategoryTheory.IsFiltered.toSup_commutes
theorem CategoryTheory.IsFiltered.toSup_commutes :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] (O : Finset C)
(H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) {X Y : C} (mX : X ∈ O) (mY : Y ∈ O)
{f : X ⟶ Y},
⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H →
CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.toSup O H mY) =
CategoryTheory.IsFiltered.toSup O H mX
The theorem `CategoryTheory.IsFiltered.toSup_commutes` states that in any category `C` that is filtered, for any finite set `O` of objects in `C`, and for any finite set `H` of morphisms between pairs of objects in `O`, if `f` is a morphism from object `X` to object `Y` in `H`, and both `X` and `Y` are in `O`, then composing `f` with the morphism from `Y` to the supremum of `O` and `H` is the same as the morphism from `X` to the supremum. In other words, every triangle formed by a morphism in `H` and the maps to the supremum of `O` and `H` commutes. This theorem is a key property in the theory of filtered categories, which are categories with certain "directedness" properties.
More concisely: In a filtered category, for any finite set of objects and morphisms between them, the composition of a morphism in the set with the morphism to the supremum of the set is equal to the morphism from the source object to the supremum.
|
CategoryTheory.IsFiltered.of_equivalence
theorem CategoryTheory.IsFiltered.of_equivalence :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D], (C ≌ D) → CategoryTheory.IsFiltered D
This theorem states that the property of being filtered is preserved by equivalence of categories. More concretely, given two types `C` and `D` with their respective categories and an equivalence of categories between `C` and `D`, if `C` is filtered, then `D` is also filtered. This means, in the context of category theory, that any finite diagram in `D` has a cocone, based on the fact that the corresponding finite diagram in `C` (due to the category equivalence) has a cocone because `C` is filtered.
More concisely: Given an equivalence of categories between filtered categories `C` and `D`, `D` is filtered.
|
CategoryTheory.IsCofiltered.cone_nonempty
theorem CategoryTheory.IsCofiltered.cone_nonempty :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] {J : Type w}
[inst_2 : CategoryTheory.SmallCategory J] [inst_3 : CategoryTheory.FinCategory J]
(F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cone F)
The theorem `CategoryTheory.IsCofiltered.cone_nonempty` states that for any type `C` that is a category and is cofiltered, and for any type `J` that is a small category and a finitely small category, if we have a functor `F` from `J` to `C`, then there exists a cone over `F`. Here, a cone over a functor is a natural transformation from a constant functor to the given functor. This theorem is a key result in category theory related to the existence of limits and the constructibility of certain diagrams.
More concisely: For any small and finitely small category `J` and any cofiltered category `C`, if `F` is a functor from `J` to `C`, then there exists a cone over `F`.
|
CategoryTheory.IsFilteredOrEmpty.cocone_maps
theorem CategoryTheory.IsFilteredOrEmpty.cocone_maps :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.IsFilteredOrEmpty C] ⦃X Y : C⦄
(f g : X ⟶ Y), ∃ Z h, CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
The theorem `CategoryTheory.IsFilteredOrEmpty.cocone_maps` states that in any category `C` which is filtered or empty, for any two parallel morphisms `f` and `g` from an object `X` to an object `Y` (denoted `f, g : X ⟶ Y`), there exists an object `Z` and a morphism `h` from `Y` to `Z` such that the following condition holds: the composition of `f` and `h` is equal to the composition of `g` and `h`. In other words, there exists a morphism `h` to the right of `f` and `g` such that it makes the two composed paths, `f` followed by `h` and `g` followed by `h`, equal.
More concisely: In a filtered or empty category, given any two parallel morphisms from an object to another, there exists an object and a morphism making them equal when composed.
|
CategoryTheory.IsFilteredOrEmpty.cocone_objs
theorem CategoryTheory.IsFilteredOrEmpty.cocone_objs :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.IsFilteredOrEmpty C] (X Y : C),
∃ Z x x, True
This theorem states that in the context of Category Theory, for any category `C` that is either filtered or empty, and for any two objects `X` and `Y` in `C`, there exists another object `Z` in `C`, along with two morphisms `x` and `x` (which could be different morphisms), such that no further conditions are placed on `Z` and these morphisms. In other words, it ensures the existence of an object "to the right" of any pair of objects in a filtered or empty category.
More concisely: In any filtered or empty category `C`, for any pair of objects `X` and `Y` in `C`, there exist objects `Z` and morphisms `f : X -> Z` and `g : Y -> Z`.
|
CategoryTheory.isFilteredOrEmpty_of_isCofilteredOrEmpty_op
theorem CategoryTheory.isFilteredOrEmpty_of_isCofilteredOrEmpty_op :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ],
CategoryTheory.IsFilteredOrEmpty C
This theorem states that for any category `C`, if the opposite category `Cᵒᵖ` is either cofiltered or empty, then `C` is either filtered or empty. In the context of category theory, a category is said to be filtered if any finite diagram (a graph where the objects are sets and the morphisms are functions) has a cocone, and it is said to be cofiltered if its opposite is filtered. Therefore, this theorem essentially provides a connection between the properties of a category and its opposite.
More concisely: If the opposite category of a category is cofiltered or empty, then the original category is filtered or empty.
|
CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint
theorem CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C]
{D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}, (L ⊣ R) → CategoryTheory.IsCofilteredOrEmpty D
The theorem `CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint` states that if we have a category `C` that is either cofiltered or empty, and a functor `L` from `C` to another category `D` which has a right adjoint, then `D` is also either cofiltered or empty. Here, "cofiltered" refers to a property of a category that generalizes the notion of a directed set from order theory.
More concisely: If `C` is a cofiltered or empty category and `L : C -> D` has a right adjoint, then `D` is also cofiltered or empty.
|
CategoryTheory.IsFiltered.span
theorem CategoryTheory.IsFiltered.span :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {i j j' : C}
(f : i ⟶ j) (f' : i ⟶ j'),
∃ k g g', CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
This theorem, named `CategoryTheory.IsFiltered.span`, states that in any category `C` that is either filtered or empty, given any three objects `i`, `j`, `j'` in `C` that forms a span, i.e., two morphisms `f : i ⟶ j` and `f' : i ⟶ j'` exist, then there exists a cocone, which is a pair of morphisms `g : j ⟶ k` and `g' : j' ⟶ k` for some object `k` in `C`, such that the diagram involving `f`, `f'`, `g`, and `g'` commutes. In other words, the composite of `f` and `g` is the same as the composite of `f'` and `g'`. This theorem is a fundamental property in category theory related to the concept of filtered categories.
More concisely: In any filtered or empty category, given a span between objects i, j, and j' (with morphisms f : i ⟶ j and f' : i ⟶ j'), there exists an object k and morphisms g : j ⟶ k and g' : j' ⟶ k such that the diagram commutes: f ∘ g = g' ∘ f'.
|
CategoryTheory.IsFiltered.bowtie
theorem CategoryTheory.IsFiltered.bowtie :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C]
{j₁ j₂ k₁ k₂ : C} (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂),
∃ s α β,
CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧
CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β
The theorem `CategoryTheory.IsFiltered.bowtie` states that in any filtered category `C`, given a "bowtie" configuration of morphisms from objects `j₁` and `j₂` to objects `k₁` and `k₂`, there exists an object `s` and two morphisms `α` and `β` from `k₁` and `k₂` to `s` respectively. This configuration ensures that the two squares in the "bowtie" commute, meaning that the composition of morphisms along any path from `j₁` or `j₂` to `s` gives the same result. In more formal terms, the composition of `f₁` with `α` equals the composition of `g₁` with `β`, and the composition of `f₂` with `α` equals the composition of `g₂` with `β`.
More concisely: In a filtered category, given morphisms from objects `j₁` and `j₂` to `k₁` and `k₂` with commuting squares, there exists an object `s` and morphisms `α: k₁ -> s` and `β: k₂ -> s` such that `f₁ ∘ α = g₁ ∘ β` and `f₂ ∘ α = g₂ ∘ β`.
|
CategoryTheory.IsCofiltered.of_isLeftAdjoint
theorem CategoryTheory.IsCofiltered.of_isLeftAdjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D] (L : CategoryTheory.Functor C D)
[inst : CategoryTheory.IsLeftAdjoint L], CategoryTheory.IsCofiltered D
This theorem asserts that if a category `C` is cofiltered, and there exists a left adjoint functor `L` from `C` to another category `D`, then the category `D` is also cofiltered. Here, cofiltered refers to a property of a category that guarantees the existence of certain limits, while a left adjoint functor is a functor that has a counterpart (right adjoint) with which it satisfies certain properties.
More concisely: If `C` is a cofiltered category and `L : C -> D` is a left adjoint functor, then `D` is also a cofiltered category.
|
CategoryTheory.IsFilteredOrEmpty.of_right_adjoint
theorem CategoryTheory.IsFilteredOrEmpty.of_right_adjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor D C} {R : CategoryTheory.Functor C D},
(L ⊣ R) → CategoryTheory.IsFilteredOrEmpty D
The theorem `CategoryTheory.IsFilteredOrEmpty.of_right_adjoint` states that for any categories `C` and `D`, where `C` is either filtered or empty, if we have a functor `R : C ⥤ D` that has a left adjoint, then the category `D` is also either filtered or empty. In essence, this theorem shows that the property of being filtered or empty is preserved under the existence of a left adjoint.
More concisely: If `C` is a filtered or empty category and `R : C ⥤ D` has a left adjoint, then `D` is also filtered or empty.
|
CategoryTheory.isFiltered_of_isCofiltered_op
theorem CategoryTheory.isFiltered_of_isCofiltered_op :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered Cᵒᵖ],
CategoryTheory.IsFiltered C
This theorem states that if we have a category `C` and its opposite `Cᵒᵖ` is cofiltered, then `C` is filtered. In mathematics, a category is said to be filtered if it satisfies certain conditions which make cocones possible, while a category is said to be cofiltered if its opposite category is filtered. So, this theorem is establishing the correlation between filtered categories and the cofiltered nature of their opposite categories.
More concisely: If the opposite category of a category is cofiltered, then the original category is filtered.
|
CategoryTheory.IsFiltered.sup_objs_exists
theorem CategoryTheory.IsFiltered.sup_objs_exists :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] (O : Finset C),
∃ S, ∀ {X : C}, X ∈ O → Nonempty (X ⟶ S)
This theorem states that for any finite collection of objects in a filtered category, there exists an object to the 'right' of all objects in the collection. Here, an object 'to the right' of another means that there exists a morphism from the latter to the former. Specifically, if `C` is a category that is filtered and `O` is a finite set of objects in `C`, then there exists an object `S` in `C` such that for any object `X` in `O`, there is a morphism from `X` to `S`.
More concisely: In a filtered category `C`, given any finite set `O` of objects, there exists an object `S` such that for every `X` in `O`, there is a morphism from `X` to `S`.
|
CategoryTheory.IsFilteredOrEmpty.of_equivalence
theorem CategoryTheory.IsFilteredOrEmpty.of_equivalence :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D], (C ≌ D) → CategoryTheory.IsFilteredOrEmpty D
The theorem `CategoryTheory.IsFilteredOrEmpty.of_equivalence` states that for any two types 'C' and 'D' that are categories, if 'C' is a category that is either filtered or empty, and there exists an equivalence of categories between 'C' and 'D', then 'D' is also a category that is either filtered or empty. In other words, the property of being filtered or being empty is preserved under an equivalence of categories.
More concisely: If C is a filtered or empty category and there exists an equivalence of categories from C to D, then D is also a filtered or empty category.
|
CategoryTheory.IsCofiltered.nonempty
theorem CategoryTheory.IsCofiltered.nonempty :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.IsCofiltered C], Nonempty C := by
sorry
This theorem states that for any type `C`, if `C` has a category structure and is cofiltered, then `C` must be nonempty. In the language of category theory, a category is said to be cofiltered if it has nonempty finite limits, and for any two objects in the category, there is a third object from which there are morphisms to the two objects. This theorem ensures that such a category cannot be empty.
More concisely: In Lean 4, a cofiltered category with a type `C` having finite limits is nonempty.
|
CategoryTheory.IsCofiltered.eq_condition
theorem CategoryTheory.IsCofiltered.eq_condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {j j' : C}
(f f' : j ⟶ j'),
CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f'
The theorem `CategoryTheory.IsCofiltered.eq_condition` asserts that for any category `C` (that is either cofiltered or empty) and for any pair of morphisms `f` and `f'` from an object `j` to an object `j'` in `C`, the composition of the morphism `eqHom f f'` (which is an arbitrary choice of morphism) with `f` is the same as the composition of `eqHom f f'` with `f'`. In other words, it states that `eqHom f f' ≫ f = eqHom f f' ≫ f'`, where `≫` denotes the composition of morphisms. This condition is guaranteed by the property of the category `C` being cofiltered.
More concisely: In any cofiltered category, for any pair of morphisms from object `j` to object `j'`, the commutativity of `eqHom f f'` with their compositions holds: `eqHom f f' ≫ f = eqHom f f' ≫ f'`.
|
CategoryTheory.IsFiltered.of_isRightAdjoint
theorem CategoryTheory.IsFiltered.of_isRightAdjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D] (R : CategoryTheory.Functor C D)
[inst : CategoryTheory.IsRightAdjoint R], CategoryTheory.IsFiltered D
This theorem states that if a category `C` is filtered and there exists a right adjoint functor `R` from `C` to another category `D`, then `D` is also filtered. In other words, it shows that the property of being filtered—meaning all finite diagrams have a cocone—is preserved under right adjoint functors.
More concisely: If `C` is a filtered category and `R : C -> D` is a right adjoint functor, then category `D` is filtered.
|
CategoryTheory.IsFilteredOrEmpty.of_isRightAdjoint
theorem CategoryTheory.IsFilteredOrEmpty.of_isRightAdjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D] (R : CategoryTheory.Functor C D)
[inst : CategoryTheory.IsRightAdjoint R], CategoryTheory.IsFilteredOrEmpty D
This theorem states that if the category `C` is either filtered or empty, and there exists a right adjoint functor `R` from `C` to another category `D`, then the category `D` is also either filtered or empty. In essence, the property of being filtered or empty is preserved through a right adjoint functor.
More concisely: If functor `R` has a right adjoint and categories `C` and `D` are filtered or empty, then category `D` is also filtered or empty.
|
CategoryTheory.IsFiltered.nonempty
theorem CategoryTheory.IsFiltered.nonempty :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.IsFiltered C], Nonempty C := by
sorry
This theorem states that for any type `C` that forms a category (symbolized by `CategoryTheory.Category.{v, u} C`) and is also a filtered category (symbolized by `CategoryTheory.IsFiltered C`), `C` must be nonempty. In other words, a category can't be filtered unless it has at least one object. This is a fundamental property of filtered categories in category theory.
More concisely: A filtered category in Lean 4 is a nonempty category.
|
CategoryTheory.IsCofiltered.cospan
theorem CategoryTheory.IsCofiltered.cospan :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C]
{i j j' : C} (f : j ⟶ i) (f' : j' ⟶ i),
∃ k g g', CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp g' f'
The theorem `CategoryTheory.IsCofiltered.cospan` states that in any category `C` that is either cofiltered or empty, for any three objects `i`, `j`, and `j'` and any two morphisms `f` from `j` to `i` and `f'` from `j'` to `i` (forming a cospan `j ⟶ i ⟵ j'`), there exists an object `k` and two morphisms `g` from `j` to `k` and `g'` from `j'` to `k` such that the square formed by `f`, `f'`, `g`, and `g'` commutes. In other words, the composition of `g` and `f` equals the composition of `g'` and `f'`. This is written in Lean as `CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp g' f'`.
More concisely: In any cofiltered or empty category, given any cospan `j ⟶ i ⟵ j'` with morphisms `f: j ⟶ i` and `f': j' ⟶ i`, there exists an object `k` and morphisms `g: j ⟶ k` and `g': j' ⟶ k` such that `g * f = f' * g'`.
|
CategoryTheory.IsFiltered.sup_exists
theorem CategoryTheory.IsFiltered.sup_exists :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] (O : Finset C)
(H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))),
∃ S T,
∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → CategoryTheory.CategoryStruct.comp f (T mY) = T mX
This theorem states that given any `Finset` (a finite set) of objects `{X, ...}` and an indexed collection of `Finset`s of morphisms `{f, ...}` in a category `C`, there exists an object `S` and a morphism `T X : X ⟶ S` from each object `X`, such that the composition of morphisms form commutative triangles: `f ≫ T Y = T X`, for each morphism `f : X ⟶ Y` in the `Finset`. This essentially describes the universal property of co-limits in a category, and `CategoryTheory.IsFiltered` is a class of categories where any finite diagram has a co-cone.
More concisely: Given any finite diagram in a category with the filtered colimit property, there exists an object and a morphism from each object in the diagram such that the composition with the morphisms from other objects forms commutative triangles, i.e., the diagram is a colimit cone.
|
CategoryTheory.IsCofilteredOrEmpty.of_isLeftAdjoint
theorem CategoryTheory.IsCofilteredOrEmpty.of_isLeftAdjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C]
{D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (L : CategoryTheory.Functor C D)
[inst : CategoryTheory.IsLeftAdjoint L], CategoryTheory.IsCofilteredOrEmpty D
This theorem states that if we have a category `C` that is either cofiltered or empty, and there exists a left adjoint functor `L` from `C` to `D`, then the category `D` is also either cofiltered or empty. In other words, the property of being cofiltered or empty is preserved under the action of a left adjoint functor from one category to another.
More concisely: If `C` is a cofiltered or empty category and `L: C ↦ D` is a left adjoint functor, then category `D` is also cofiltered or empty.
|
CategoryTheory.IsFiltered.coeq_condition
theorem CategoryTheory.IsFiltered.coeq_condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j j' : C}
(f f' : j ⟶ j'),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeqHom f f') =
CategoryTheory.CategoryStruct.comp f' (CategoryTheory.IsFiltered.coeqHom f f')
The theorem `CategoryTheory.IsFiltered.coeq_condition` asserts that for any category `C` (that is either filtered or empty), any two morphisms `f` and `f'` from `j` to `j'` in `C`, the composition of `f` with the coequalizer homomorphism of `f` and `f'` is equal to the composition of `f'` with the same coequalizer homomorphism. In mathematical terms, it states that `f ≫ coeqHom f f' = f' ≫ coeqHom f f'` holds in the category `C`. This equality is essentially the defining property of a coequalizer in category theory.
More concisely: In any filtered or empty category `C`, the coequalizer homomorphism of morphisms `f` and `f'` commutes with both `f` and `f'`, i.e., `f ∘ coeqHom f f' = f' ∘ coeqHom f f'`.
|
CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op
theorem CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty Cᵒᵖ],
CategoryTheory.IsCofilteredOrEmpty C
This theorem states that for any type `C`, if `C` when viewed as a category is either filtered or empty when considering its opposite category `Cᵒᵖ`, then `C` itself is cofiltered or empty. This concept is from category theory, where categories have dual ("opposite") versions, and properties like being filtered or cofiltered can be transferred to these dual versions.
More concisely: If category `C` is either filtered or empty in its opposite category `Cᵒᵖ`, then `C` is cofiltered or empty.
|
CategoryTheory.IsFiltered.of_right_adjoint
theorem CategoryTheory.IsFiltered.of_right_adjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor D C} {R : CategoryTheory.Functor C D},
(L ⊣ R) → CategoryTheory.IsFiltered D
This theorem states that if we have a mathematical structure `C` that is filtered, along with a functor `R : C ⥤ D` that has a left adjoint, then the structure `D` is also filtered. In terms of category theory, this theorem demonstrates a property related to the concept of adjoint functors and filtered categories. Essentially, the "filteredness" property can be transferred from one category to another via a functor with a left adjoint.
More concisely: If `C` is a filtered category and `R : C ⥤ D` has a left adjoint, then `D` is also a filtered category.
|
CategoryTheory.IsCofilteredOrEmpty.cone_maps
theorem CategoryTheory.IsCofilteredOrEmpty.cone_maps :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.IsCofilteredOrEmpty C] ⦃X Y : C⦄
(f g : X ⟶ Y), ∃ W h, CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
This theorem states that in any category theory context (denoted by `CategoryTheory.IsCofilteredOrEmpty C`), given any two parallel morphisms (`f` and `g`) from one object `X` to another object `Y`, there exists an object `W` and a morphism `h` from `W` to `X` such that the composition of `h` and `f` equals the composition of `h` and `g`. In symbols, this is saying that if we have two morphisms `f: X → Y` and `g: X → Y`, then there exists a morphism `h: W → X` such that `h ∘ f = h ∘ g`. This property is important in the theory of categories, as it provides a form of commutativity for morphisms.
More concisely: In any cocomplete category, given two parallel morphisms between objects, there exists a common right inverse.
|
CategoryTheory.IsCofiltered.of_left_adjoint
theorem CategoryTheory.IsCofiltered.of_left_adjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C},
(L ⊣ R) → CategoryTheory.IsCofiltered D
The theorem states that if we have a category `C` that is cofiltered, and a functor `L` from `C` to another category `D` that has a right adjoint `R`, then the category `D` is also cofiltered. In other words, cofilteredness is preserved under a functor from a cofiltered category to any other category, provided the functor has a right adjoint.
More concisely: If `C` is a cofiltered category and `L : C -> D` has a right adjoint `R : D -> C`, then `D` is also cofiltered.
|
CategoryTheory.IsCofilteredOrEmpty.cone_objs
theorem CategoryTheory.IsCofilteredOrEmpty.cone_objs :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.IsCofilteredOrEmpty C] (X Y : C),
∃ W x x, True
This theorem states that in the context of category theory, for any given category `C` that is either cofiltered or empty, and for any pair of objects `X` and `Y` in this category, there exists another object `W` and two morphisms `x`, `x` (from `W` to `X` and `Y` respectively). The condition `True` simply indicates that there are no additional constraints on the morphisms or the objects in this theorem.
More concisely: In any cofiltered or empty category `C`, for every pair of objects `X` and `Y`, there exists an object `W` and morphisms `f : W -> X` and `g : W -> Y`.
|
CategoryTheory.IsCofiltered.inf_exists
theorem CategoryTheory.IsCofiltered.inf_exists :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] (O : Finset C)
(H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))),
∃ S T,
∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → CategoryTheory.CategoryStruct.comp (T mX) f = T mY
This theorem states that in a cofiltered category `C`, given any finite set (`Finset`) `O` of objects and a finite set `H` of morphisms such that each morphism is between two objects in `O`, there exists an object `S` and a function `T` that assigns to each object `X` in `O` a morphism `T X` from `S` to `X`, in such a way that for any pair of objects `X` and `Y` in `O` and any morphism `f` from `X` to `Y` that is in `H`, the diagram involving `T X`, `T Y`, and `f` commutes. This means that for such `X`, `Y`, and `f`, the composition of `T X` and `f` equals `T Y`.
More concisely: In a cofiltered category, given a finite set of objects and morphisms between them, there exists an object and a function assigning morphisms to objects such that the diagrams commute for all morphisms in the set.
|
CategoryTheory.IsFiltered.cocone_nonempty
theorem CategoryTheory.IsFiltered.cocone_nonempty :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] {J : Type w}
[inst_2 : CategoryTheory.SmallCategory J] [inst_3 : CategoryTheory.FinCategory J]
(F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cocone F)
This theorem states that if we are given a category `C` that is filtered (i.e., satisfies certain properties related to the existence of co-limits), then for any functor `F` from a small, finite category `J` to `C`, there exists a cocone over `F`. In other words, we can find a universal cocone (a particular type of diagram in category theory) in `C` with a vertex object such that all diagrams in `J` can be mapped to it via `F`.
More concisely: Given a filtered category `C` and a small, finite category `J`, every functor `F` from `J` to `C` has a cocone with universal property.
|
CategoryTheory.IsCofiltered.of_equivalence
theorem CategoryTheory.IsCofiltered.of_equivalence :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] {D : Type u₁}
[inst_2 : CategoryTheory.Category.{v₁, u₁} D], (C ≌ D) → CategoryTheory.IsCofiltered D
This theorem states that the property of being cofiltered is preserved by equivalence of categories in category theory. In other words, if we have a category `C` that is cofiltered, and we have another category `D` such that `C` is equivalent to `D` (denoted `C ≌ D`), then `D` is also cofiltered.
More concisely: If categories `C` and `D` are equivalent (`C ≌ D`), and `C` is cofiltered, then `D` is also cofiltered.
|
CategoryTheory.IsCofiltered.inf_objs_exists
theorem CategoryTheory.IsCofiltered.inf_objs_exists :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] (O : Finset C),
∃ S, ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)
This theorem states that in any cofiltered category, given any finite set of objects, there exists an object in the category that has a morphism to every object in the given set. In other words, for any finite collection of objects in a cofiltered category, there is an object "to the left" of all those objects, meaning that there are arrows (or morphisms) going from this object to each object in the collection.
More concisely: In a cofiltered category, for any finite set of objects, there exists an object with a morphism to each object in the set.
|
CategoryTheory.IsFiltered.tulip
theorem CategoryTheory.IsFiltered.tulip :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty 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 α β γ,
CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧
CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp f₃ γ ∧
CategoryTheory.CategoryStruct.comp f₄ γ = CategoryTheory.CategoryStruct.comp g₂ β
The theorem `CategoryTheory.IsFiltered.tulip` states that for any filtered category `C`, given a configuration of objects and morphisms shaped like a "tulip" (where `j₁`, `j₂`, `j₃`, `k₁`, `k₂`, and `l` are objects, `f₁`, `f₂`, `f₃`, `f₄`, `g₁`, `g₂` are morphisms as arranged in the diagram), there exists an object `s` and three morphisms `α`, `β`, `γ` from `k₁`, `k₂` and `l` to `s` such that the resulting squares commute. This means that the compositions of the morphisms along the different paths in the diagram from the objects `j₁`, `j₂`, `j₃` to the object `s` are equal. Specifically, `f₁ ≫ α = g₁ ≫ β`, `f₂ ≫ α = f₃ ≫ γ`, and `f₄ ≫ γ = g₂ ≫ β`.
More concisely: Given a filtered category `C` and objects `j₁, j₂, j₃, k₁, k₂, l` along with morphisms `f₁, f₂, f₃, f₄, g₁, g₂` arranged in a tulip shape, there exists an object `s` and morphisms `α, β, γ` making the squares commute, i.e., `f₁ ∘ α = g₁ ∘ β`, `f₂ ∘ α = f₃ ∘ γ`, and `f₄ ∘ γ = g₂ ∘ β`.
|
CategoryTheory.IsCofiltered.infTo_commutes
theorem CategoryTheory.IsCofiltered.infTo_commutes :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C] (O : Finset C)
(H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) {X Y : C} (mX : X ∈ O) (mY : Y ∈ O)
{f : X ⟶ Y},
⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H →
CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.infTo O H mX) f =
CategoryTheory.IsCofiltered.infTo O H mY
The theorem `CategoryTheory.IsCofiltered.infTo_commutes` states that in the context of a category `C` that is cofiltered, given two objects `X` and `Y` in a finset `O` and a morphism `f` from `X` to `Y` that is a member of a finset `H`, the composition of the morphism `f` with the morphism from the infimum of `O` and `H` to `X` is equal to the morphism from the infimum of `O` and `H` to `Y`. In other words, for any triangle formed by a morphism in `H` and the maps from the infimum of `O` and `H`, the triangle commutes.
More concisely: In a cofiltered category, for any objects X, Y in a finset, and morphism f from X to Y in a finset H, the diagram commutes: inf(O, H) -> X -> Y = inf(O, H) -> Y, where O is the finset containing X and Y.
|
CategoryTheory.isCofiltered_of_isFiltered_op
theorem CategoryTheory.isCofiltered_of_isFiltered_op :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered Cᵒᵖ],
CategoryTheory.IsCofiltered C
This theorem states that for any category `C`, if the opposite category `Cᵒᵖ` is filtered, then the original category `C` is cofiltered. In categorical theory, a filtered category has certain limits, and a cofiltered category has certain colimits. So, this theorem essentially describes a relationship between the limiting properties of a category and its opposite.
More concisely: If the opposite category of a category is filtered, then the original category is cofiltered.
|