CategoryTheory.Limits.Cotrident.app_one
theorem CategoryTheory.Limits.Cotrident.app_one :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
(s : CategoryTheory.Limits.Cotrident f) (j : J),
CategoryTheory.CategoryStruct.comp (f j) (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.one) =
s.ι.app CategoryTheory.Limits.WalkingParallelFamily.zero
The theorem `CategoryTheory.Limits.Cotrident.app_one` states that for any category `C` with objects `X` and `Y`, and any function `f` from some type `J` to the set of morphisms from `X` to `Y`, if we have a cotrident `s` on `f`, then for any element `j` of `J`, the composition of the morphism `f j` and the morphism from the tip of the cotrident to the object corresponding to `one` in the walking parallel family is equal to the morphism from the tip of the cotrident to the object corresponding to `zero` in the walking parallel family. In category theory, this principle is often referred to as the universal property of cotridents.
More concisely: For any category C, given a cotrident s on a function f from type J to the morphisms from X to Y in C, for all j in J, we have f j ∘ s.top = s.top\_0, where s.top is the morphism from the tip of the cotrident to an object in C corresponding to one, and s.top\_0 is the morphism from the tip to an object corresponding to zero in the walking parallel family.
|
CategoryTheory.Limits.Trident.IsLimit.homIso_natural
theorem CategoryTheory.Limits.Trident.IsLimit.homIso_natural :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
[inst_1 : Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) {Z Z' : C}
(q : Z' ⟶ Z) (k : Z ⟶ t.pt),
↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) =
CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k)
The theorem `CategoryTheory.Limits.Trident.IsLimit.homIso_natural` states that for any category `C`, given objects `X`, `Y`, and `Z` in `C`, a function `f` from some type `J` to the set of morphisms from `X` to `Y`, and a trident `t` on `f` that is a limit, the bijection provided by `Trident.IsLimit.homIso` is natural in `Z`. In other words, for any two objects `Z` and `Z'` in the category and morphisms `q : Z' ⟶ Z` and `k : Z ⟶ t.pt`, the composition of `q` and `k` followed by applying `Trident.IsLimit.homIso` to the result is the same as first applying `Trident.IsLimit.homIso` to `k` and then composing with `q`. In terms of category theory, this expresses a certain commutativity property of the diagram involving the mentioned morphisms and objects.
More concisely: Given a limit trident `t` on a function `f : J ↪ C(X, Y)` in a category `C`, the naturality of the bijection `Trident.IsLimit.homIso t` implies that for any morphisms `q : Z' ⟶ Z` and `k : Z ⟶ t.pt`, the diagram commutes: `q ∘ k ≅ Trident.IsLimit.homIso t ∘ k`.
|
CategoryTheory.Limits.Trident.equalizer_ext
theorem CategoryTheory.Limits.Trident.equalizer_ext :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
[inst_1 : Nonempty J] (s : CategoryTheory.Limits.Trident f) {W : C} {k l : W ⟶ s.pt},
CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι →
∀ (j : CategoryTheory.Limits.WalkingParallelFamily J),
CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
The theorem `CategoryTheory.Limits.Trident.equalizer_ext` states that, given a category `C` with objects `X`, `Y`, and `W`, a family of morphisms `f : J → (X ⟶ Y)` forming a trident, and two morphisms `k, l : W ⟶ s.pt` where `s` is a cone over the `f` family, if `k` and `l` are equal after composition with the universal morphism of the trident `s.ι`, then for all `j` in `J`, `k` after composition with `s.π.app j` is equal to `l` after composition with `s.π.app j`. In other words, to check whether two morphisms are equalized by every morphism in a trident, it suffices to check if they are equalized by the universal morphism of the trident.
More concisely: Given a trident (category, cone, family of morphisms) in a category, if two morphisms are equalized by the universal morphism of the trident, then they are equalized by every morphism in the family.
|
CategoryTheory.Limits.Cotrident.coequalizer_ext
theorem CategoryTheory.Limits.Cotrident.coequalizer_ext :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
[inst_1 : Nonempty J] (s : CategoryTheory.Limits.Cotrident f) {W : C} {k l : s.pt ⟶ W},
CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l →
∀ (j : CategoryTheory.Limits.WalkingParallelFamily J),
CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l
This theorem states that: In the context of a category theory, specifically for a type `C` that forms a category with objects `X`, `Y`, and `W`, and a family of morphisms `f` from type `J` to the hom-set from `X` to `Y`, and given a cotrident `s` on `f` and two morphisms `k` and `l` from the point of `s` to `W`, if the composition of `s`'s cocone map and `k` is equal to the composition of `s`'s cocone map and `l`, then for any element `j` in the parallel family formed by `J`, the composition of the natural transformation at `j` and `k` is also equal to the composition of the natural transformation at `j` and `l`. In simpler terms, if two maps are coequalized by the cocone map of a cotrident, then they are also coequalized by each of the maps in the cotrident's natural transformation.
More concisely: If two morphisms in a category are coequalized by the cocone map of a cotriple, then they are coequalized by each morphism in the cotriple's natural transformation.
|
CategoryTheory.Limits.wideCoequalizer.hom_ext
theorem CategoryTheory.Limits.wideCoequalizer.hom_ext :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
[inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] [inst_2 : Nonempty J] {W : C}
{k l : CategoryTheory.Limits.wideCoequalizer f ⟶ W},
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) k =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) l →
k = l
This theorem in Category Theory states that for any category `C` and any two objects `X` and `Y` in `C`, if `f` is a family of morphisms from `X` to `Y` indexed by a non-empty type `J` and has a wide coequalizer in `C`, then any two morphisms `k` and `l` from the wide coequalizer of `f` to any object `W` in `C` are the same if and only if their compositions with the coequalizer morphism of `f` are the same. In other words, if two morphisms from the wide coequalizer are the same after composing with the coequalizer morphism, then both original morphisms are equal.
More concisely: Given a category `C`, objects `X`, `Y`, and a non-empty index type `J`, a family `f` of morphisms from `X` to `Y` with a wide coequalizer, and morphisms `k` and `l` from its coequalizer to an object `W`, if `k ∘ coeq(f) = l ∘ coeq(f)`, then `k = l`.
|
CategoryTheory.Limits.epi_of_isColimit_parallelFamily
theorem CategoryTheory.Limits.epi_of_isColimit_parallelFamily :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
[inst_1 : Nonempty J] {c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.parallelFamily f)},
CategoryTheory.Limits.IsColimit c →
CategoryTheory.Epi (c.ι.app CategoryTheory.Limits.WalkingParallelFamily.one)
This theorem asserts that for any type `J` and category `C` with objects of type `C`, given objects `X` and `Y` in `C`, and a function `f` from `J` to the hom-set from `X` to `Y`, if `J` is nonempty and `c` is a colimit cocone of the diagram formed by the parallel family of morphisms defined by `f`, then the morphism from `c` to the object represented by the "one" element of the walking parallel family (which is part of the diagram) is an epimorphism. In other words, in any category, the morphism from a colimit cocone to a particular object defined by a parallel family of morphisms is always epic (i.e., right-cancellative).
More concisely: In any category, the morphism from a colimit cocone to a specific object in the diagram formed by a parallel family of morphisms is an epimorphism.
|
CategoryTheory.Limits.mono_of_isLimit_parallelFamily
theorem CategoryTheory.Limits.mono_of_isLimit_parallelFamily :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
[inst_1 : Nonempty J] {c : CategoryTheory.Limits.Cone (CategoryTheory.Limits.parallelFamily f)},
CategoryTheory.Limits.IsLimit c → CategoryTheory.Mono (CategoryTheory.Limits.Trident.ι c)
This theorem states that in the context of category theory, for any type `J`, any category `C`, and any objects `X` and `Y` in `C`, if `f` is a function from `J` to the hom-set `X ⟶ Y`, and `c` is a limit cone of the parallel family defined by `f`, then the wide equalizer morphism of the cone `c` is a monomorphism. Essentially, it says that the limit of a parallel family of morphisms in a category ensures that the connecting morphism of the associated cone is always a monomorphism.
More concisely: In category theory, the wide equalizer morphism of a limit cone over a family of morphisms is a monomorphism.
|
CategoryTheory.Limits.hasWideCoequalizers_of_hasColimit_parallelFamily
theorem CategoryTheory.Limits.hasWideCoequalizers_of_hasColimit_parallelFamily :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 :
∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)},
CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelFamily f)],
CategoryTheory.Limits.HasWideCoequalizers C
The theorem `CategoryTheory.Limits.hasWideCoequalizers_of_hasColimit_parallelFamily` states that for any category `C`, if `C` has all colimits of diagrams formed by a `parallelFamily` of morphisms `f` (i.e., a family of morphisms from some object `X` to some object `Y` indexed by a type `J`), then `C` also has all wide coequalizers. In other words, if a category has all colimits of a certain form (parallel families), it also has coequalizers for a wide range of objects.
In mathematical terms, a wide coequalizer is a generalized version of a coequalizer where we consider more than two parallel morphisms. A coequalizer is a universal construct in category theory that captures the notion of the 'simplest' object through which all the morphisms in a parallel pair 'factor through'—and a wide coequalizer generalizes this to an arbitrary family of parallel morphisms. This theorem, therefore, establishes a connection between the existence of specific types of colimits (those associated with parallel families of morphisms) and the existence of wide coequalizers.
More concisely: If a category has all colimits of parallel families of morphisms, then it has all wide coequalizers.
|
CategoryTheory.Limits.wideEqualizer.hom_ext
theorem CategoryTheory.Limits.wideEqualizer.hom_ext :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
[inst_1 : CategoryTheory.Limits.HasWideEqualizer f] [inst_2 : Nonempty J] {W : C}
{k l : W ⟶ CategoryTheory.Limits.wideEqualizer f},
CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.wideEqualizer.ι f) =
CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.wideEqualizer.ι f) →
k = l
The theorem `CategoryTheory.Limits.wideEqualizer.hom_ext` states that for any category `C`, any objects `X` and `Y` in `C`, any parallel family of morphisms `f` from `X` to `Y`, and any object `W` in `C`, if there exists a wide equalizer of `f` and if two morphisms `k` and `l` from `W` to the wide equalizer of `f` satisfy that their compositions with the inclusion map from the wide equalizer to `X` are equivalent, then `k` and `l` themselves must be equivalent. This theorem formalizes the uniqueness property of maps into equalizers in category theory.
More concisely: If in a category, two morphisms have equivalent compositions with the inclusion into the wide equalizer of a parallel family of morphisms, then they are equivalent.
|
CategoryTheory.Limits.hasWideEqualizers_of_hasLimit_parallelFamily
theorem CategoryTheory.Limits.hasWideEqualizers_of_hasLimit_parallelFamily :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 :
∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)},
CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelFamily f)],
CategoryTheory.Limits.HasWideEqualizers C
This theorem states that in any category `C`, if `C` possesses all limits of diagrams formed by families of parallel morphisms (i.e., if for any objects `X` and `Y` in `C` and any indexed family of morphisms `f` from `J` to the hom-set from `X` to `Y`, there exists a limit of the diagram formed by the parallel family `f`), then `C` has all wide equalizers. In category theory, a wide equalizer of a family of morphisms is an object that maps to every object in the family in such a way that the composition of each morphism in the family with this map results in the same morphism. This theorem is essentially saying that the existence of specific types of limits (those of parallel families of morphisms) ensures the existence of wide equalizers in the category.
More concisely: In a limit-preserving category, the existence of limits of parallel families of morphisms implies the existence of wide equalizers.
|
CategoryTheory.Limits.Trident.app_zero
theorem CategoryTheory.Limits.Trident.app_zero :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
(s : CategoryTheory.Limits.Trident f) (j : J),
CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero) (f j) =
s.π.app CategoryTheory.Limits.WalkingParallelFamily.one
The theorem `CategoryTheory.Limits.Trident.app_zero` states that for any category `C`, and any objects `X` and `Y` in `C`, given a function `f` from some type `J` to the Hom-set `Hom(X, Y)`, and given a trident structure `s` on `f`, for any element `j` of `J`, the composition of the morphism at the 'zero' position in the trident with `f(j)` is equal to the morphism at the 'one' position in the trident. In other words, in the context of category theory, this theorem asserts a particular commutative property of a trident structure on a parallel family of morphisms.
More concisely: For any category C, given a trident structure on a family of morphisms f from an index type J to Hom(X, Y), the composition of the morphism at the 'zero' position with f(j) equals the morphism at the 'one' position for all j in J.
|
CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural
theorem CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
[inst_1 : Nonempty J] {t : CategoryTheory.Limits.Cotrident f} {Z Z' : C} (q : Z ⟶ Z')
(ht : CategoryTheory.Limits.IsColimit t) (k : t.pt ⟶ Z),
↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp k q)) =
CategoryTheory.CategoryStruct.comp (↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k)) q
This theorem states that the bijection of `Cotrident.IsColimit.homIso` is natural in `Z`. In the context of category theory, this means that for any type `J`, category `C`, objects `X`, `Y`, `Z`, and `Z'` in `C`, a morphism `f` from `J` to `X ⟶ Y`, a cotrident `t` on `f`, a morphism `q` from `Z` to `Z'`, and a morphism `k` from the point of `t` to `Z`, the homomorphism corresponding to the composition of `k` and `q` under `homIso` is equal to the composition of the homomorphism corresponding to `k` under `homIso` and `q`. This is assuming that `t` is a colimit in the category, and `J` is not empty.
More concisely: Given a cotrident (a colimit cone) `t` in a category `C` with non-empty index category `J`, and morphisms `q: Z → Z'`, `k: J → Z`, the naturality of `Cotrident.IsColimit.homIso` implies that `homIso.toFun(k) ∘ q = homIso.toFun(k ∘ f)`, where `f` is a morphism from `J` to `X ⟶ Y`.
|