CategoryTheory.Limits.epi_of_isColimit_cofork
theorem CategoryTheory.Limits.epi_of_isColimit_cofork :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{c : CategoryTheory.Limits.Cofork f g}, CategoryTheory.Limits.IsColimit c → CategoryTheory.Epi c.π
The theorem `CategoryTheory.Limits.epi_of_isColimit_cofork` states that in any category `C`, for any two morphisms `f` and `g` from `X` to `Y`, if `c` is a cofork on `f` and `g`, and `c` is a colimit, then the coequalizer morphism of the cofork `c` is an epimorphism. Here, epimorphism is a categorical concept equivalent to surjectivity in the category of sets. In other words, if we have a situation where any morphism `f` and `g` are coequalized at a specific cofork `c`, which is a colimit, then the coequalizer morphism of this cofork will always be an epimorphism, i.e., every element in the codomain is the image of some element in the domain.
More concisely: In a category C, if morphisms f and g have cofork c as their coequalizer and c is a colimit, then the coequalizer morphism of c is an epimorphism.
|
CategoryTheory.Limits.eq_of_mono_coequalizer
theorem CategoryTheory.Limits.eq_of_mono_coequalizer :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasCoequalizer f g]
[inst_2 : CategoryTheory.Mono (CategoryTheory.Limits.coequalizer.π f g)], f = g
This theorem states that in any category, if two morphisms `f` and `g` from an object `X` to an object `Y` have a coequalizer and the coequalizer projection is a monomorphism (an injective morphism), then the two morphisms `f` and `g` are equal. A coequalizer in category theory is a universal way to make two morphisms equal, and a monomorphism is a morphism that can't be factored through another morphism.
More concisely: In any category, if two morphisms from an object to another have a coequalizer with monomorphic projection, they are equal.
|
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left
theorem CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
(s : CategoryTheory.Limits.Fork f g),
s.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp s.ι f
The theorem `CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left` states that, for any category `C`, any objects `X` and `Y` in `C`, and any morphisms `f` and `g` from `X` to `Y`, if `s` is a fork on `f` and `g`, then the application of the projection function `s.π.app` at `CategoryTheory.Limits.WalkingParallelPair.one` is the same as the composition of the inclusion morphism `CategoryTheory.Limits.Fork.ι s` and the morphism `f`. In other words, in the context of category theory, this theorem relates the projection from a fork to a certain composition of morphisms in the category.
More concisely: For any category C, given objects X and Y, morphisms f and g from X to Y, and a fork s on f and g, the projection function s.π.app at CategoryTheory.Limits.WalkingParallelPair.one equals the composition of the inclusion morphism ιs and f.
|
CategoryTheory.Limits.Cofork.IsColimit.hom_ext
theorem CategoryTheory.Limits.Cofork.IsColimit.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g},
CategoryTheory.Limits.IsColimit s →
∀ {W : C} {k l : s.pt ⟶ W},
CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l → k = l
This theorem is stating that in any category `C`, given two morphisms `f` and `g` from `X` to `Y`, and a cofork `s` on `f` and `g`, if `s` is a colimit, then for any object `W` in the category, and any two morphisms `k` and `l` from the point of `s` to `W`, if the composition of the projection of `s` and `k` is equal to the composition of the projection of `s` and `l`, then `k` and `l` must be the same morphism. In other words, this is a uniqueness condition on morphisms from the tip of a cofork that is a colimit.
More concisely: Given any category `C`, if morphisms `f` and `g` from object `X` to object `Y` have a cofork `s` that is a colimit, then any two morphisms `k` and `l` from the object at the tip of `s` to any object `W` with `proj(s) ∘ k = proj(s) ∘ l` imply `k = l`.
|
CategoryTheory.Limits.ι_comp_coequalizerComparison
theorem CategoryTheory.Limits.ι_comp_coequalizerComparison :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
[inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
[inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g))
(CategoryTheory.Limits.coequalizerComparison f g G) =
G.map (CategoryTheory.Limits.coequalizer.π f g)
This theorem states that, given a category `C` and two morphisms `f` and `g` from `X` to `Y` in `C`, along with a functor `G` mapping `C` to another category `D`, if `f` and `g` have a coequalizer in `C` and the functors `G.map f` and `G.map g` have a coequalizer in `D`, then the composition of the coequalizer projection of `G.map f` and `G.map g` in `D` followed by the coequalizer comparison of `f` and `g` under `G` equals the `G`-mapping of the coequalizer projection of `f` and `g` in `C`. In mathematical terms, we have the following equality of morphisms in the category `D`: `(coequalizer.π (G.map f) (G.map g)) ≫ (coequalizerComparison f g G) = (G.map (coequalizer.π f g))`.
More concisely: Given a category `C`, a functor `G` from `C` to another category `D`, and morphisms `f` and `g` in `C` with coequalizers, if `G.map f` and `G.map g` have a coequalizer in `D`, then the projection of the coequalizer of `G.map f` and `G.map g` in `D` equals the `G`-map of the coequalizer projection of `f` and `g` in `C`.
|
CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair
theorem CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : ∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g)],
CategoryTheory.Limits.HasCoequalizers C
The theorem `CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair` states that if a category `C` has all colimits of diagrams formed by a parallel pair of morphisms `f` and `g` (i.e., two morphisms from the same source object `X` to the same target object `Y`), then `C` has all coequalizers. Here, coequalizers are a specific type of colimit, representing an object that is the "best" way to map two parallel morphisms to a single morphism.
More concisely: If a category has all colimits of parallel morphism pairs, then it has all coequalizers.
|
CategoryTheory.Limits.equalizer.ι_of_eq
theorem CategoryTheory.Limits.equalizer.ι_of_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasEqualizer f g],
f = g → CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.ι f g)
This theorem states that in a category `C`, given two morphisms `f` and `g` from object `X` to object `Y` with an equalizer, if `f` equals `g`, then the inclusion from the equalizer of `f` and `g` to `X` is an isomorphism. In simpler words, when the two morphisms are the same, the mapping from the equalizer object to `X` can be reversed without loss of information.
More concisely: Given two equalizing morphisms `f` and `g` from object `X` to object `Y` in a category `C`, if `f` equals `g`, then the equalizer inclusion morphism from the equalizer of `f` and `g` to `X` is an isomorphism.
|
CategoryTheory.Limits.Fork.equalizer_ext
theorem CategoryTheory.Limits.Fork.equalizer_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
(s : CategoryTheory.Limits.Fork f g) {W : C} {k l : W ⟶ s.pt},
CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι →
∀ (j : CategoryTheory.Limits.WalkingParallelPair),
CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
This theorem states that in any category `C`, given two morphisms `f` and `g` from `X` to `Y`, and a fork `s` on `f` and `g`, if two morphisms `k` and `l` from some object `W` to the tip of the fork `s` make the same composite with the injection of the fork, then they make the same composite with the legs of the cone of the fork. It's essentially saying that to check if two maps are equal when composed with both maps of a fork, it's enough to check it for the first map.
More concisely: In any category `C`, if morphisms `f`, `g` : `X` -> `Y`, fork `s` : {f, g} -> `Z`, and `k`, `l` : `W` -> `Z` satisfy `k * f = l * g` through the injection of the fork, then `k = l * h` for some `h` : `W` -> `X`.
|
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left
theorem CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
(s : CategoryTheory.Limits.Cofork f g),
s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.CategoryStruct.comp f s.π
This theorem states that for any category `C`, any two objects `X` and `Y` in `C`, and any two morphisms `f` and `g` from `X` to `Y`, if `s` is a cofork on `f` and `g`, then applying the cocone morphism `s.ι` to the initial object `CategoryTheory.Limits.WalkingParallelPair.zero` is equivalent to composing `f` with the projection morphism `CategoryTheory.Limits.Cofork.π s`. Here, the cofork is a particular kind of cocone over the parallel pair constructed from `f` and `g`, and the projection morphism is a morphism from the cofork to `Y`.
More concisely: For any category `C`, given objects `X`, `Y`, morphisms `f`, `g : X → Y`, and a cofork `s` on `f` and `g`, the following commutative diagram holds:
```
⋢───⌣─── s.ι ≫ CategoryTheory.Limits.WalkingParallelPair.zero
| |
v v
X Y
| |
↙─── f ───⟩ g ───────────────────────────────────────────────π_s
```
Therefore, `s.ι ∘ CategoryTheory.Limits.WalkingParallelPair.zero = π_s ∘ f`.
|
CategoryTheory.Limits.eq_of_mono_cofork_π
theorem CategoryTheory.Limits.eq_of_mono_cofork_π :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
(t : CategoryTheory.Limits.Cofork f g) [inst_1 : CategoryTheory.Mono t.π], f = g
This theorem states that in any category `C`, for any two objects `X` and `Y` and two morphisms `f` and `g` from `X` to `Y`, if there exists a cofork on `f` and `g` such that its projection `π` is a monomorphism (injective homomorphism), then `f` and `g` are equal. In other words, in the context of category theory, if two morphisms are related by a mono cofork, they must be identical.
More concisely: In any category C, if morphisms f and g from object X to object Y have a cofork with a monic (monomorphism) projection, then f and g are equal.
|
CategoryTheory.Limits.eq_of_epi_equalizer
theorem CategoryTheory.Limits.eq_of_epi_equalizer :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasEqualizer f g]
[inst_2 : CategoryTheory.Epi (CategoryTheory.Limits.equalizer.ι f g)], f = g
This theorem, `CategoryTheory.Limits.eq_of_epi_equalizer`, states that in any category `C`, for any objects `X` and `Y` and morphisms `f` and `g` from `X` to `Y`, if the equalizer of `f` and `g` exists and the inclusion morphism from the equalizer to `X` is an epimorphism (i.e., it is "surjective" in the categorical sense), then `f` and `g` must be equal.
In other words, if "everything" in `X` that comes from the equalizer (via the inclusion morphism) also comes from both `f` and `g` (since the equalizer "equalizes" `f` and `g`), and this situation "covers" all of `X` (since the inclusion morphism is an epimorphism), then `f` and `g` must be the same.
More concisely: If in a category `C`, the equalizer of morphisms `f` and `g` from object `X` to object `Y` exists and the inclusion morphism from the equalizer to `X` is an epimorphism, then `f` and `g` are equal.
|
CategoryTheory.Limits.equalizer.hom_ext
theorem CategoryTheory.Limits.equalizer.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} {k l : W ⟶ CategoryTheory.Limits.equalizer f g},
CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.equalizer.ι f g) =
CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) →
k = l
The theorem `CategoryTheory.Limits.equalizer.hom_ext` states that in a category `C`, for any two objects `X` and `Y` with morphisms `f` and `g` from `X` to `Y` and an equalizer of `f` and `g`, if there is a third object `W` and two morphisms `k` and `l` from `W` to the equalizer, then `k` and `l` are equal if they yield the same result when composed with the morphism from the equalizer to `X` (i.e., the equalizer map). In mathematical terms, this can be expressed as: if `k` composed with the equalizer map equals `l` composed with the equalizer map (k ∘ equalizer.ι f g = l ∘ equalizer.ι f g), then `k` equals `l` (k = l).
More concisely: If two morphisms from a third object to the equalizer of two given morphisms have equal compositions with the equalizer map, then they are equal.
|
CategoryTheory.Limits.mono_of_isLimit_fork
theorem CategoryTheory.Limits.mono_of_isLimit_fork :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{c : CategoryTheory.Limits.Fork f g}, CategoryTheory.Limits.IsLimit c → CategoryTheory.Mono c.ι
This theorem states that in any category `C`, for any two morphisms `f` and `g` from object `X` to object `Y`, if `c` is a fork on `f` and `g` that is also a limit cone, then the fork's natural morphism, often termed the equalizer morphism, is a monomorphism. In category theory, a monomorphism is a morphism (or arrow) that is left-cancelable, meaning that if two morphisms are post-composed with the monomorphism, their equality implies that they were equal to start with.
More concisely: In any category C, given morphisms f and g from object X to object Y, if c is a fork on f and g that is also a limit cone, then the equalizer morphism of c is a monomorphism.
|
CategoryTheory.Limits.equalizer.condition
theorem CategoryTheory.Limits.equalizer.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasEqualizer f g],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) g
This theorem states that in any category `C`, for any two morphisms `f` and `g` from `X` to `Y`, if `f` and `g` have an equalizer, then the composition of the equalizer's inclusion morphism (`equalizer.ι f g`) with `f` is equal to the composition of the equalizer's inclusion morphism with `g`. In other words, following the equalizer into `X` and then following `f` to `Y` is the same as following the equalizer into `X` and then following `g` to `Y`. This is the defining property of an equalizer in category theory.
More concisely: In any category, for all morphisms f and g from X to Y with an equalizer, the diagram commutes: i.e., equalizer.ι (f ∘ i) = equalizer.ι (g ∘ i).
|
CategoryTheory.Limits.parallelPair_functor_obj
theorem CategoryTheory.Limits.parallelPair_functor_obj :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
(j : CategoryTheory.Limits.WalkingParallelPair),
(CategoryTheory.Limits.parallelPair (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
(F.map CategoryTheory.Limits.WalkingParallelPairHom.right)).obj
j =
F.obj j
This theorem states that for any category `C`, and any functor `F` from the category of a walking parallel pair to `C`, the object obtained by applying the functor `F` to a walking parallel pair is identical to the object obtained by the `parallelPair` operation to the morphisms `WalkingParallelPairHom.left` and `WalkingParallelPairHom.right` in the category `C`. The `parallelPair` operation creates a parallel pair of morphisms between two objects in a category.
More concisely: For any category `C` and functor `F` from the category of walking parallel pairs, `F(WalkingParallelPair(x, y))` is isomorphic to `parallelPair(F(x) ↔[F(f)] F(y))` in `C`, where `x ↔[f] y` is a walking parallel pair in `C`.
|
CategoryTheory.Limits.Fork.IsLimit.homIso_natural
theorem CategoryTheory.Limits.Fork.IsLimit.homIso_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{t : CategoryTheory.Limits.Fork f g} (ht : CategoryTheory.Limits.IsLimit t) {Z Z' : C} (q : Z' ⟶ Z)
(k : Z ⟶ t.pt),
↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) =
CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z) k)
The theorem `CategoryTheory.Limits.Fork.IsLimit.homIso_natural` states that for any category `C`, given two morphisms `f` and `g` from `X` to `Y`, a fork `t` on `f` and `g`, where `t` is a limit cone, and two objects `Z` and `Z'` in `C` with a morphism `q : Z' ⟶ Z` and a morphism `k : Z ⟶ t.pt`, the isomorphism obtained from the `homIso` function applied to the limit `ht`, the object `Z'`, and the composition of `q` and `k`, is equal to the composition of `q` and the isomorphism obtained from the `homIso` function applied to `ht`, `Z`, and `k`. This expresses the naturality condition in the context of Category Theory, meaning that the isomorphism respects the structure of the category.
More concisely: For any limit cone `t` on morphisms `f` and `g` from object `X` to object `Y` in category `C`, and morphisms `q : Z' ⟶ Z` and `k : Z ⟶ t.pt`, the isomorphism obtained from applying `homIso` to `ht`, `Z'`, and `q ∘ k` is equal to the composition of `q` and the isomorphism obtained from applying `homIso` to `ht`, `Z`, and `k`.
|
CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self
theorem CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
{c : CategoryTheory.Limits.Cofork f f}, CategoryTheory.Limits.IsColimit c → CategoryTheory.IsIso c.π
This theorem states that in any category 'C', for any two objects 'X' and 'Y', and for any morphism 'f' from 'X' to 'Y', if there exists a `Cofork` 'c' on 'f' and 'f' which is a colimit, then the canonical projection (π) of the `Cofork` 'c' is an isomorphism. In other words, every coequalizer of a pair of identical morphisms is an isomorphism in the category.
More concisely: In any category, if a cofork of two identical morphisms is a colimit, then the canonical projection of the cofork is an isomorphism.
|
CategoryTheory.Limits.coequalizer.hom_ext
theorem CategoryTheory.Limits.coequalizer.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {W : C} {k l : CategoryTheory.Limits.coequalizer f g ⟶ W},
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) k =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) l →
k = l
The theorem `CategoryTheory.Limits.coequalizer.hom_ext` states that within a category `C`, for any objects `X`, `Y`, and `W`, and morphisms `f` and `g` from `X` to `Y`, given that `f` and `g` have a coequalizer, if there exist two morphisms `k` and `l` from the coequalizer of `f` and `g` to `W` such that composing the projection from `Y` to the coequalizer with `k` is equal to composing the same projection with `l`, then `k` and `l` are equal. In other words, in the context of category theory, it asserts the uniqueness property for morphisms out of the coequalizer.
More concisely: In a category, if two morphisms have a coequalizer and there exists a morphism from the coequalizer to another object that equals the composition of the projection from the coequalizer to the coequalizer with each of the original morphisms, then these two morphisms from the original object to the coequalizer are equal.
|
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq
theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y},
f = g → ∀ {c : CategoryTheory.Limits.Fork f g}, CategoryTheory.Limits.IsLimit c → CategoryTheory.IsIso c.ι
The theorem `CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq` states that in any category `C`, given objects `X` and `Y` and morphisms `f` and `g` from `X` to `Y`, if `f` equals `g`, then for any fork `c` on `f` and `g` (i.e., a cone over the parallel pair of `f` and `g`), if `c` is a limit cone, then the natural inclusion of `c` (denoted `CategoryTheory.Limits.Fork.ι c`) is an isomorphism. In other words, if `f` and `g` are the same morphism, then every limit of the fork on `f` and `g` is isomorphic to the initial object of the category.
More concisely: In a category, if two morphisms from one object to another are equal and have a limit cone, then the inclusion of that cone is an isomorphism.
|
CategoryTheory.Limits.eq_of_epi_fork_ι
theorem CategoryTheory.Limits.eq_of_epi_fork_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g) [inst_1 : CategoryTheory.Epi t.ι], f = g
This theorem states that for any category 'C', and any objects 'X' and 'Y' within 'C', if there exist two morphisms 'f' and 'g' from 'X' to 'Y', and a fork on 'f' and 'g' such that the inclusion of the fork is an epimorphism (a morphism which is "onto" or surjective), then the two morphisms 'f' and 'g' are equal.
More concisely: In any category, if two morphisms from one object to another have a common epimorphic fork, then they are equal.
|
CategoryTheory.Limits.Cofork.IsColimit.homIso_natural
theorem CategoryTheory.Limits.Cofork.IsColimit.homIso_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{t : CategoryTheory.Limits.Cofork f g} {Z Z' : C} (q : Z ⟶ Z') (ht : CategoryTheory.Limits.IsColimit t)
(k : t.pt ⟶ Z),
↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp k q)) =
CategoryTheory.CategoryStruct.comp (↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z) k)) q
The theorem `CategoryTheory.Limits.Cofork.IsColimit.homIso_natural` states that for any category `C`, objects `X`, `Y`, `Z`, `Z'` in `C`, morphisms `f` and `g` from `X` to `Y`, a cofork `t` on `f` and `g`, a morphism `q` from `Z` to `Z'`, and a morphism `k` from the point of `t` to `Z`, if `t` is a colimit, then the homomorphism given by the bijection `CategoryTheory.Limits.Cofork.IsColimit.homIso` applied to `Z'` and the composition of `k` and `q` is equal to the composition of the homomorphism given by the bijection applied to `Z` and `k`, and `q`. This expresses the naturality of the bijection in the object `Z`.
More concisely: Given categories `C`, objects `X`, `Y`, `Z`, `Z'`, morphisms `f` and `g` from `X` to `Y`, a cofork `t` on `f` and `g`, and morphisms `k` from the point of `t` to `Z` and `q` from `Z` to `Z'` in `C`, if `t` is a colimit, then the homomorphism induced by `q` and `k` via the bijection `CategoryTheory.Limits.Cofork.IsColimit.homIso is equal to the composition of the homomorphism induced by `q` and `k` via `CategoryTheory.Limits.Cofork.IsColimit.homIso for Z` and the homomorphism induced by `k` and `f` via `CategoryTheory.Limits.Cofork.IsColimit.homIso for X`.
|
CategoryTheory.Limits.Fork.condition
theorem CategoryTheory.Limits.Fork.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
(t : CategoryTheory.Limits.Fork f g),
CategoryTheory.CategoryStruct.comp t.ι f = CategoryTheory.CategoryStruct.comp t.ι g
The theorem `CategoryTheory.Limits.Fork.condition` states that for any category `C`, any objects `X` and `Y` in `C`, and any morphisms `f` and `g` from `X` to `Y`, if we have a fork `t` on `f` and `g`, then the composition of the morphism from the apex of the fork `t` with `f` is equal to the composition of the morphism from the apex of the fork `t` with `g`. In other words, in the diagrammatic representation of the fork, the two possible paths from the apex of the fork to `Y` via `f` and `g` respectively are equal.
More concisely: Given a category `C`, objects `X`, `Y`, morphisms `f`, `g`, and a fork `t` on `f` and `g` at `Y`, the composition of `t` with `f` equals the composition of `t` with `g`.
|
CategoryTheory.Limits.coequalizer.π_of_eq
theorem CategoryTheory.Limits.coequalizer.π_of_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasCoequalizer f g],
f = g → CategoryTheory.IsIso (CategoryTheory.Limits.coequalizer.π f g)
The theorem `CategoryTheory.Limits.coequalizer.π_of_eq` states that in any category `C`, for any two objects `X` and `Y` and any two morphisms `f` and `g` from `X` to `Y` that have a coequalizer, if `f` is equal to `g`, then the coequalizer projection of `f` and `g` is an isomorphism. In other words, when the two morphisms in a pair for which a coequalizer exists are the same, then the projection from the common codomain to the coequalizer is an isomorphism.
More concisely: In any category, if two morphisms from one object to another have a coequalizer and are equal, then their coequalizer projection is an isomorphism.
|
CategoryTheory.Limits.Cofork.IsColimit.π_desc
theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{s t : CategoryTheory.Limits.Cofork f g} (hs : CategoryTheory.Limits.IsColimit s),
CategoryTheory.CategoryStruct.comp s.π (hs.desc t) = t.π
This theorem, `CategoryTheory.Limits.Cofork.IsColimit.π_desc`, states that for any category `C` with objects `X` and `Y`, and for any pair of morphisms `f` and `g` from `X` to `Y`, if we have two coforks `s` and `t` over the pair `(f, g)`, and if `s` is a colimit, then composing the projection from `s` to `Y` with the unique morphism from `s` to `t` that makes the triangle commute (given by `hs.desc t`), gives us the projection from `t` to `Y`. This essentially states a property of the universal property of colimits in the context of coforks.
More concisely: Given a category `C` with objects `X` and `Y`, and morphisms `f`, `g` from `X` to `Y`, if `s` is a colimit cofork over `(f, g)` and there is a morphism `h` from `s` to `t` making the triangle commute, then the composite of the projection from `s` to `Y` and `h` equals the projection from `t` to `Y`.
|
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi
theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{c : CategoryTheory.Limits.Fork f g},
CategoryTheory.Limits.IsLimit c → ∀ [inst_1 : CategoryTheory.Epi c.ι], CategoryTheory.IsIso c.ι
This theorem states that in any category `C`, for any objects `X` and `Y`, and for any morphisms `f` and `g` from `X` to `Y`, if `c` is a fork on `f` and `g` that forms a limit, and the morphism from `c` to `X` is an epimorphism, then this morphism is also an isomorphism. In other words, if an equalizer of two morphisms is also an epimorphism, then it is an isomorphism.
More concisely: In any category, if an equalizer of two morphisms is an epimorphism, then it is an isomorphism.
|
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self
theorem CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.Fork f f},
CategoryTheory.Limits.IsLimit c → CategoryTheory.IsIso c.ι
This theorem states that, in any category `C`, for any objects `X` and `Y` in `C` and any morphism `f` from `X` to `Y`, if `c` is a fork on `f` and `f` and `c` is a limit, then the morphism `ι` from `c` is an isomorphism. In other words, every equalizer of a pair of identical morphisms is an isomorphism. This is a property of how limits interact with equalizers in category theory.
More concisely: In any category, if a morphism has a limit and a fork, then the morphism from the fork to the limit is an isomorphism. (Every equalizer of a pair of identical morphisms is an isomorphism.)
|
CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi
theorem CategoryTheory.Limits.isIso_limit_cocone_parallelPair_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{c : CategoryTheory.Limits.Cofork f g},
CategoryTheory.Limits.IsColimit c → ∀ [inst_1 : CategoryTheory.Mono c.π], CategoryTheory.IsIso c.π
This theorem states that in any category `C`, for any two morphisms `f` and `g` from `X` to `Y`, and for any cofork `c` on `f` and `g`, if `c` is a colimit (meaning it is the coequalizer for the parallel pair `f` and `g`) and the arrow `c.π` is a monomorphism (i.e., a one-to-one or injective morphism), then `c.π` is also an isomorphism (a morphism that has an inverse).
More concisely: In any category `C`, if a cofork `c` of morphisms `f` and `g` from `X` to `Y` is both a colimit and a monomorphism, then `c.π` is an isomorphism.
|
CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq
theorem CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y},
f = g → ∀ {c : CategoryTheory.Limits.Cofork f g}, CategoryTheory.Limits.IsColimit c → CategoryTheory.IsIso c.π
This theorem states that in any category `C`, for any two morphisms `f` and `g` from `X` to `Y`, if `f` and `g` are the same, then for any cofork `c` of `f` and `g`, if `c` is a colimit, then the arrow (`π`) from the apex of the cofork to `Y` is an isomorphism. In simpler terms, it says that every coequalizer of a pair of identical morphisms in a category is an isomorphism.
More concisely: In any category, if two morphisms have the same source and target and are equal, then their coequalizer is an isomorphism.
|
CategoryTheory.Limits.coequalizer.condition
theorem CategoryTheory.Limits.coequalizer.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasCoequalizer f g],
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.coequalizer.π f g) =
CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.coequalizer.π f g)
The theorem `CategoryTheory.Limits.coequalizer.condition` states that for any category `C` and any two morphisms `f` and `g` from object `X` to `Y` in `C` such that `f` and `g` have a coequalizer, the composition of `f` with the coequalizer projection (denoted `CategoryTheory.Limits.coequalizer.π f g`) is equal to the composition of `g` with the coequalizer projection. In other words, the diagram involving `f`, `g`, and the coequalizer projection commutes. This is a fundamental property of coequalizers in category theory.
More concisely: For any category `C`, given morphisms `f` and `g` from object `X` to `Y` with coequalizer `h : Y -> Z`, we have `f ∘ h = g ∘ h`.
|
CategoryTheory.Limits.Fork.IsLimit.hom_ext
theorem CategoryTheory.Limits.Fork.IsLimit.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{s : CategoryTheory.Limits.Fork f g},
CategoryTheory.Limits.IsLimit s →
∀ {W : C} {k l : W ⟶ s.pt},
CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι → k = l
This theorem, `CategoryTheory.Limits.Fork.IsLimit.hom_ext`, states that in a category `C`, for any two morphisms `f` and `g` from object `X` to object `Y`, given a fork `s` on `f` and `g` that is a limit, for any object `W` and any two morphisms `k` and `l` from `W` to the fork's point `s.pt`, if the composite of `k` and the injection `CategoryTheory.Limits.Fork.ι s` is equal to the composite of `l` and the injection `CategoryTheory.Limits.Fork.ι s`, then `k` and `l` are the same morphism. This theorem embodies the uniqueness part of the universal property of limits in category theory.
More concisely: In a category, if two morphisms to a limit have equal compositions with the injections from the limit's point to each morphism, then they are equal.
|
CategoryTheory.Limits.Cofork.IsColimit.π_desc'
theorem CategoryTheory.Limits.Cofork.IsColimit.π_desc' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{s : CategoryTheory.Limits.Cofork f g} (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k),
CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.Limits.Cofork.IsColimit.desc hs k h) = k
This theorem in the Category Theory context asserts that for any category `C`, objects `X` and `Y` in `C`, and morphisms `f` and `g` from `X` to `Y`, given a cofork `s` on `f` and `g` that is a colimit in the category, and any object `W` in `C` with a morphism `k` from `Y` to `W` such that the composition `f ≫ k` equals `g ≫ k`, the composition of the projection from the cofork (denoted by `CategoryTheory.Limits.Cofork.π s`) and the descent from the colimit to `W` (denoted by `CategoryTheory.Limits.Cofork.IsColimit.desc hs k h`) is equal to the morphism `k`. This theorem captures a key property of colimits in category theory.
More concisely: Given any category `C`, objects `X`, `Y`, morphisms `f`, `g` from `X` to `Y`, a cofork `s` on `f` and `g` that is a colimit in `C`, and a morphism `k` from `Y` to an object `W` such that `f ≫ k = g ≫ k`, the projection from the cofork and the descent to `W` are equal to `k`.
|
CategoryTheory.Limits.Cofork.coequalizer_ext
theorem CategoryTheory.Limits.Cofork.coequalizer_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
(s : CategoryTheory.Limits.Cofork f g) {W : C} {k l : s.pt ⟶ W},
CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l →
∀ (j : CategoryTheory.Limits.WalkingParallelPair),
CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l
This theorem states that in a category 'C', for any two morphisms 'f' and 'g' from 'X' to 'Y', and a cofork 's' on 'f' and 'g', if we have two other morphisms 'k' and 'l' from the target object of the cofork to some object 'W' such that the composition of 's.π' (the co-cone morphism of the co-fork) with 'k' is equal to the composition of 's.π' with 'l', then for any object 'j' in the index category of the cofork, the composition of the cofork's component at 'j' with 'k' is also equal to the composition of the cofork's component at 'j' with 'l'. In other words, to verify that two maps are coequalized (made equal) by both maps of a cofork, it's sufficient to check this condition for the second map. This theorem is a part of the categorical concept of limit and co-limit.
More concisely: In a category 'C', if cofork morphisms 's.π' of two morphisms 'f' and 'g' from 'X' to 'Y' have the same composition with morphisms 'k' and 'l' from the target object of the cofork to an object 'W', then the components of the cofork at any index object 'j' have equal compositions with 'k' and 'l'.
|
CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair
theorem CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : ∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)],
CategoryTheory.Limits.HasEqualizers C
The theorem `CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair` states that for any category `C`, if `C` has all limits of diagrams defined by a pair of parallel morphisms `f` and `g` from `X` to `Y`, then `C` also has all equalizers. In mathematical terms, an equalizer is a specific limit for a pair of morphisms, so if a category has all general limits for such pairs, it necessarily has all equalizers.
More concisely: In any category with all limits of pairs of parallel morphisms, equalizers exist.
|
CategoryTheory.Limits.Fork.IsLimit.lift_ι
theorem CategoryTheory.Limits.Fork.IsLimit.lift_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
{s t : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s),
CategoryTheory.CategoryStruct.comp (hs.lift t) s.ι = t.ι
The theorem `CategoryTheory.Limits.Fork.IsLimit.lift_ι` states that for any category `C` with objects `X` and `Y`, and morphisms `f` and `g` between `X` and `Y`, given any two forks `s` and `t` on `f` and `g`, if `s` is a limit, then the composition of the lift of `t` with respect to `s` and the projection (`ι`) of `s` is equal to the projection of `t`. In simpler terms, if we have a limit structure on a fork, we can lift any other fork to it in a way that preserves the fork structure.
More concisely: If $s$ and $t$ are forks on morphisms $f$ and $g$ in a category $C$ with limit $s$, then the projection of $t$ is equal to the composition of the lift of $t$ with respect to $s$ and the projection of $s$.
|
CategoryTheory.Limits.coequalizer.π_desc
theorem CategoryTheory.Limits.coequalizer.π_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {W : C} (k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g)
(CategoryTheory.Limits.coequalizer.desc k h) =
k
The theorem `CategoryTheory.Limits.coequalizer.π_desc` states that in any category `C`, for any objects `X`, `Y`, and `W` in `C`, and for any morphisms `f`, `g` from `X` to `Y`, and `k` from `Y` to `W` such that the composition of `f` and `k` is equal to the composition of `g` and `k`, if `f` and `g` have a coequalizer, then the composition of the projection from the coequalizer of `f` and `g` and the descendent of `k` with respect to the coequalizer is equal to `k`. This property encapsulates the universal property of the coequalizer in the language of category theory.
More concisely: If in a category `C` objects `X`, `Y`, `W`, morphisms `f: X → Y`, `g: X → Y`, and `k: Y → W` satisfy `f ∘ k = g ∘ k`, and `f` and `g` have a coequalizer, then the composition of the coequalizer's projection and `k`'s descent is equal to `k`.
|
CategoryTheory.Limits.Cofork.condition
theorem CategoryTheory.Limits.Cofork.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
(t : CategoryTheory.Limits.Cofork f g),
CategoryTheory.CategoryStruct.comp f t.π = CategoryTheory.CategoryStruct.comp g t.π
This theorem, called `CategoryTheory.Limits.Cofork.condition`, states that for any category `C` and for any objects `X` and `Y` in this category, given two morphisms `f` and `g` from `X` to `Y` and a cofork `t` on `f` and `g`, the composition of the morphism `f` with the projection function of the cofork (`CategoryTheory.Limits.Cofork.π t`) is equal to the composition of the morphism `g` with the same projection function. In other words, the diagram formed by `f`, `g`, and the cofork projection commutes.
More concisely: For any category C, objects X and Y, morphisms f and g from X to Y, and cofork t on f and g, the diagram commutes: f · CategoryTheory.Limits.Cofork.π t = g · CategoryTheory.Limits.Cofork.π t.
|
Mathlib.CategoryTheory.Limits.Shapes.Equalizers._auxLemma.1
theorem Mathlib.CategoryTheory.Limits.Shapes.Equalizers._auxLemma.1 :
∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h
This theorem from Category Theory in mathematics, states that for any objects `W, X, Y, Z` in a category, and morphisms `f : W ⟶ X`, `g : X ⟶ Y`, `h : Y ⟶ Z`, the composition of the morphisms is associative. In other words, composing `f` with the result of composing `g` and `h` is the same as composing the result of composing `f` and `g` with `h`. This is written in mathematical notation as `(f ∘ (g ∘ h)) = ((f ∘ g) ∘ h)`, where `∘` represents the composition of morphisms.
More concisely: In any category, the order of composing morphisms does not matter, that is, `(f ∘ g) ∘ h = f ∘ (g ∘ h)` for morphisms `f : W ⟶ X`, `g : X ⟶ Y`, and `h : Y ⟶ Z`.
|