CategoryTheory.Limits.Multifork.condition
theorem CategoryTheory.Limits.Multifork.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C}
(K : CategoryTheory.Limits.Multifork I) (b : I.R),
CategoryTheory.CategoryStruct.comp (K.ι (I.fstTo b)) (I.fst b) =
CategoryTheory.CategoryStruct.comp (K.ι (I.sndTo b)) (I.snd b)
The theorem `CategoryTheory.Limits.Multifork.condition` states that for any category `C`, multispan index `I`, and a multifork `K` of `I`, for any object `b` in the right index `I.R` of `I`, the composition of the morphism `I.fst b` after the morphism from the point of `K` to the left object `I.fstTo b` is equal to the composition of the morphism `I.snd b` after the morphism from the point of `K` to the left object `I.sndTo b`. In other words, both paths from the cone point of the multifork to the object `b` in the category `C` through the multispan index `I` are equal.
More concisely: For any category C, multispan index I, object b in I.R, and multifork K of I, the composition of I.fst b with the morphism from the point of K to I.fstTo b equals the composition of I.snd b with the morphism from the point of K to I.sndTo b.
|
CategoryTheory.Limits.Multicofork.fst_app_right
theorem CategoryTheory.Limits.Multicofork.fst_app_right :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C}
(K : CategoryTheory.Limits.Multicofork I) (a : I.L),
K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) =
CategoryTheory.CategoryStruct.comp (I.fst a) (K.π (I.fstFrom a))
This theorem states that for any category `C`, any multispan index `I` in `C`, any multicofork `K` over `I`, and any object `a` from the left side of `I`, the application of the natural transformation `ι` of `K` to the morphism `WalkingMultispan.left a` is equal to the composition of the first morphism from `a` and the morphism from `I.fstFrom a` to the vertex of `K`. This is a condition for `K` to be a multicofork, which is a type of cocone in category theory. Here, `WalkingMultispan.left a` represents a morphism in the multispan, `I.fst a` represents the first morphism from `a`, and `CategoryTheory.Limits.Multicofork.π K (I.fstFrom a)` represents the morphism from the right side of the multispan to the vertex of the multicofork.
More concisely: For any multicofork $K$ over index $I$ in category $C$ and object $a$ in $C$, the following diagram commutes:
$$
\xymatrix{
a \ar[rr]^{\text{WalkingMultispan.left } a} \ar[rd]_{I.fst a} & & K.dom \\
& I.fstFrom a \ar[ur]_{\pi_K (I.fst a)}
}
$$
where $\pi_K$ is the natural transformation of $K$.
|
CategoryTheory.Limits.Multicofork.condition
theorem CategoryTheory.Limits.Multicofork.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C}
(K : CategoryTheory.Limits.Multicofork I) (a : I.L),
CategoryTheory.CategoryStruct.comp (I.fst a) (K.π (I.fstFrom a)) =
CategoryTheory.CategoryStruct.comp (I.snd a) (K.π (I.sndFrom a))
The theorem `CategoryTheory.Limits.Multicofork.condition` states that for any type `C` with an instance of a category structure, for any multispan index `I` of this category, and for any multicofork `K` of this multispan index, every object `a` on the left of the index satisfies a certain condition. The condition is that the composition of the first morphism from `a` and the morphism from the target of the first morphism to the point of the cocone is equal to the composition of the second morphism from `a` and the morphism from the target of the second morphism to the point of the cocone. In simpler terms, this means that the two possible paths from `a` to the cocone point through the multispan give the same result.
More concisely: For any category `C` with a multispan index `I` and multicofork `K`, the composition of the first morphism from an object `a` in `C` with the morphism from the target of the first morphism to the cocone point equals the composition of the second morphism from `a` with the morphism from the target of the second morphism to the cocone point, for all cocones over `K` in `C`.
|
CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst
theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C}
(K : CategoryTheory.Limits.Multifork I) (b : I.R),
K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) =
CategoryTheory.CategoryStruct.comp (K.ι (I.fstTo b)) (I.fst b)
The theorem `CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst` states that in any category `C`, for any multicospan index `I` and any multifork `K` over `I`, for each object `b` from the right index set `I.R`, the morphism from the apex of the cone `K` to `b` is equal to the composition of the morphism from the apex of the cone to the left object associated to `b` via `I.fstTo`, and the morphism `I.fst b`. In other words, this theorem specifies a property of the diagram chasing in the multifork or multicone structure.
More concisely: For any category C, given a multicospan index I and a multifork K over I, the morphism from the apex of cone K to any right index object b is equal to the composition of the morphism from the apex to the left object linked to b via I.fstTo, and the morphism I.fst b.
|
CategoryTheory.Limits.Multicoequalizer.π_desc
theorem CategoryTheory.Limits.Multicoequalizer.π_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C)
[inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : I.R) → I.right b ⟶ W)
(h :
∀ (a : I.L),
CategoryTheory.CategoryStruct.comp (I.fst a) (k (I.fstFrom a)) =
CategoryTheory.CategoryStruct.comp (I.snd a) (k (I.sndFrom a)))
(b : I.R),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b)
(CategoryTheory.Limits.Multicoequalizer.desc I W k h) =
k b
This theorem, `CategoryTheory.Limits.Multicoequalizer.π_desc`, states that for any category `C`, given a `MultispanIndex` `I`, if `I` has a multicoequalizer, and given an object `W` in `C` and a function `k` which assigns a morphism from `I.right b` to `W` for each `b` in `I.R`, such that for each `a` in `I.L` the composition of `I.fst a` with `k` of `I.fstFrom a` equals the composition of `I.snd a` with `k` of `I.sndFrom a`, then for any `b` in `I.R`, the composition of the multicoequalizer canonical map (from `I.right b` to the multicoequalizer of `I`) with the multicoequalizer desc map (from the multicoequalizer to `W`) equals `k b`. This essentially describes the universal property of the multicoequalizer in a category.
More concisely: For any category `C`, given a multicoequalizer `(M, η, μ)` of a multispan `(I, L, R, fst, snd)` and a function `k : I.R → C` such that `k ∘ fst = k ∘ snd`, the diagram commutes: `η ∘ I.right → M ∣→ k = k`.
|