SimplicialObject.Splitting.ι_desc
theorem SimplicialObject.Splitting.ι_desc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X) {Z : C} (Δ : SimplexCategoryᵒᵖ)
(F : (A : SimplicialObject.Splitting.IndexSet Δ) → s.N A.fst.unop.len ⟶ Z)
(A : SimplicialObject.Splitting.IndexSet Δ),
CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (s.desc Δ F) = F A
This theorem, `SimplicialObject.Splitting.ι_desc`, states that for a given category `C`, a simplicial object `X` in `C`, a splitting `s` of `X`, an object `Z` in `C`, a contravariant object `Δ` in `SimplexCategory` and a function `F` mapping from the `IndexSet` of the splitting to a morphism from `s.N (SimplexCategory.len A.fst.unop)` to `Z`, the composition of the cofan injection of the splitting with respect to `A` and the description of the splitting equals to the function `F` evaluated at `A`. In other words, it describes how the function `F` relates to the structure of the simplicial object.
More concisely: For any simplicial object X in category C, splitting s, object Z in C, contravariant Δ in SimplexCategory, and function F from the splitting's index set to morphisms from s.N to Z, the composition of the coface injection of s with respect to A and the description of the splitting equals F evaluated at A.
|
SimplicialObject.Splitting.cofan_inj_eq
theorem SimplicialObject.Splitting.cofan_inj_eq :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X) {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ),
(s.cofan Δ).inj A = CategoryTheory.CategoryStruct.comp (s.ι A.fst.unop.len) (X.map A.e.op)
The theorem `SimplicialObject.Splitting.cofan_inj_eq` states that for any category `C`, any simplicial object `X` in `C`, any splitting `s` of `X`, any `Δ` in the opposite simplex category, and any index set `A` associated to `Δ`, the injection from the `A`th object of `Δ` into the cofan of `s` at `Δ` is equal to the composition of the `ι` component of `s` applied to the length of the first component of `A` with the mapping of the simplicial object `X` applied to the epimorphism associated to `A`. This theorem relates the structure of the cofan to the structure of the splitting in the category of simplicial objects.
More concisely: For any simplicial object X in a category C, any splitting s of X, and any epimorphism A in the opposite simplex category with domain Δ and image the i-th object of Δ, the injection from the image of A under the cofan of s at Δ is equal to the composition of s(i) with the mapping of X from the source of A.
|